Prime-refinement separator interface and consequences

PrimeRefinementTheorem states the separator property for the concrete Fox--Neuwirth model. This file derives the functional prime-refinement consequences from that proposition.

def NRR.PrimeRefinementTheorem : Prop

For every prime and every nice multivalued function on the child-body hyperspace, the concrete Fox--Neuwirth model produces a top--bottom separator whose points lift to simultaneous child zeros.

Equations

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

theorem NRR.PrimeRefinementTheorem.toFlexible (H : PrimeRefinementTheorem) : FlexiblePrimeRefinementTheorem

A separator for the fixed Fox--Neuwirth model is a model-independent refinement step.

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

A prime-refinement separator witness yields the refined nice multivalued function together with its complete child-partition lifting property.

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

Fiberwise existence form: for every parent body, a separator witness supplies a common parameter and a canonical equal-area p-partition whose children are all input zeros.