Prime-refinement separator certificates

This module isolates the exact output required from the mod-p Fox--Neuwirth argument. A certificate consists of a top--bottom separator over the parent-body hyperspace and a lifting property: every point of the separator is represented by a prime configuration for which all canonical equal-area children are zeros of the input nice multivalued function.

The definition contains no orbit-count or transversality axiom. Those belong to the geometric prime-refinement theorem that constructs such a certificate. Once a certificate is available, the conversion to a new nice multivalued function is formal and is proved here directly.

structure NRR.PrimeRefinementSeparator {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Type

The proof-carrying separator produced by one prime-refinement step.

For every carrier point (C,y), lifts supplies a configuration parameter whose canonical p-piece equal-area partition of C consists entirely of zeros of φ at the common parameter y.

• separator : TopBottomSeparator (BodySpace K A)

  The separator in the parent-body/parameter cylinder.

• lifts (C : BodySpace K A) (y : ↑SignedInterval) : (C, y) ∈ self.separator.carrier → ∃ (x : M.Point), ((C, x), y) ∈ M.allChildrenZeroSet hA φ

  Every point of the separator lifts to a simultaneous child zero.

noncomputable def NRR.PrimeRefinementSeparator.toNiceMV {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {M : PrimeConfigurationModel hp} {hA : 0 < A} {φ : NiceMV (BodySpace K (A / ↑p))} (S : PrimeRefinementSeparator M hA φ) [Nonempty (BodySpace K A)] : NiceMV (BodySpace K A)

The output nice multivalued function associated with the separator.

Equations

• S.toNiceMV = S.separator.toNiceMV

theorem NRR.PrimeRefinementSeparator.zero_toNiceMV_iff {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {M : PrimeConfigurationModel hp} {hA : 0 < A} {φ : NiceMV (BodySpace K (A / ↑p))} (S : PrimeRefinementSeparator M hA φ) [Nonempty (BodySpace K A)] (C : BodySpace K A) (y : ↑SignedInterval) : S.toNiceMV.Zero C y ↔ (C, y) ∈ S.separator.carrier

A zero of the output function is exactly a point of the separator carrier.

theorem NRR.PrimeRefinementSeparator.zero_lifts_to_all_children {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {M : PrimeConfigurationModel hp} {hA : 0 < A} {φ : NiceMV (BodySpace K (A / ↑p))} (S : PrimeRefinementSeparator M hA φ) [Nonempty (BodySpace K A)] {C : BodySpace K A} {y : ↑SignedInterval} (hy : S.toNiceMV.Zero C y) : ∃ (x : M.Point), ∀ (i : Fin p), φ.Zero (EMP.VariableBody.child M.sites hA ⋯ (C, x) i) y

Every zero of the output nice multivalued function lifts to a configuration at which all canonical equal-area children are zeros of the input function.

theorem NRR.PrimeRefinementSeparator.zero_lifts_to_partition_witness {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {M : PrimeConfigurationModel hp} {hA : 0 < A} {φ : NiceMV (BodySpace K (A / ↑p))} (S : PrimeRefinementSeparator M hA φ) [Nonempty (BodySpace K A)] {C : BodySpace K A} {y : ↑SignedInterval} (hy : S.toNiceMV.Zero C y) : ∃ (x : M.Point) (W : EMP.VariableBody.Witness M.sites hA ⋯ (C, x)), ∀ (i : Fin p), φ.Zero (W.child i) y

The stronger witness form of zero_lifts_to_all_children, retaining the canonical power partition and its cover/null-overlap/equal-area proofs.

theorem NRR.PrimeRefinementSeparator.exists_zero_with_partition_witness {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {M : PrimeConfigurationModel hp} {hA : 0 < A} {φ : NiceMV (BodySpace K (A / ↑p))} (S : PrimeRefinementSeparator M hA φ) [Nonempty (BodySpace K A)] (C : BodySpace K A) : ∃ (y : ↑SignedInterval), S.toNiceMV.Zero C y ∧ ∃ (x : M.Point) (W : EMP.VariableBody.Witness M.sites hA ⋯ (C, x)), ∀ (i : Fin p), φ.Zero (W.child i) y

Every parent body has at least one parameter value on the refined zero set, and that value comes with a simultaneous child-zero configuration.