Model-independent prime-refinement steps

The geometric obstruction may be represented by any compact prime-equivariant configuration model. The recursive partition construction uses only that model's site family and the separator lifting property, independently of a particular top-cell atlas.

structure NRR.FlexiblePrimeRefinementStep {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) : Type 1

One prime-refinement step together with the concrete configuration model that realizes it.

• model : PrimeConfigurationModel hp

  The prime configuration model selected for the refinement step.

• certificate : PrimeRefinementSeparator self.model hA phi

  The separator certificate for the selected model and multivalued observable.

def NRR.FlexiblePrimeRefinementTheorem : Prop

Model-independent prime-refinement theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.FlexiblePrimeRefinementTheorem.refinedNiceMV (H : FlexiblePrimeRefinementTheorem) (p : ℕ) (hp : Nat.Prime p) (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) (hA : 0 < A) [Nonempty (BodySpace K A)] (phi : NiceMV (BodySpace K (A / ↑p))) : ∃ (psi : NiceMV (BodySpace K A)), ∀ (C : BodySpace K A) (y : ↑SignedInterval), psi.Zero C y → ∃ (M : PrimeConfigurationModel hp) (x : M.Point) (W : EMP.VariableBody.Witness M.sites hA ⋯ (C, x)), ∀ (i : Fin p), phi.Zero (W.child i) y

A flexible step yields the next nice multivalued function and its complete partition decoder.