Stable refined S6 obstruction

This is the S6 endpoint. Endpoint counts are taken only from StableRegularApproximations, so a positive-ray intersection cannot be lost on a triangulation face. The finite relative-collar theorem supplies stable homotopy invariance. The positive reference endpoint is discharged explicitly at level zero by the reference-map skeleton transversality theorem.

noncomputable def NRR.AAK.stableRefinedChildObstructionValue {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((FoxNeuwirthOrderComplex.orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) : ZMod p

Stable obstruction value of the frozen child map.

Equations

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

theorem NRR.AAK.stableRefinedChildObstructionValue_locally_constant {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((FoxNeuwirthOrderComplex.orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) : ∃ (U : Set (BodySpace K A × ↑SignedInterval)) (hUout : U ⊆ ((FoxNeuwirthOrderComplex.orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ), IsOpen U ∧ z ∈ U ∧ ∀ (w : BodySpace K A × ↑SignedInterval) (hw : w ∈ U), stableRefinedChildObstructionValue hp hA phi w ⋯ = stableRefinedChildObstructionValue hp hA phi z hz

The stable child obstruction is locally constant on the complement.

theorem NRR.AAK.stableRefinedChildObstructionValue_left_eq_zero {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : stableRefinedChildObstructionValue hp hA phi (C, SignedInterval.left) ⋯ = 0

The stable obstruction vanishes on the lower endpoint.

theorem NRR.AAK.stableRefinedChildObstructionValue_right_ne_zero {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : stableRefinedChildObstructionValue hp hA phi (C, SignedInterval.right) ⋯ ≠ 0

The stable obstruction is nonzero on the upper endpoint.

noncomputable def NRR.AAK.stableRefinedComplementObstructionValue {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) : ComplementObstructionValue (BodySpace K A) ((FoxNeuwirthOrderComplex.orderComplexModel hp).projectedAllChildrenZeroSet hA phi) (ZMod p)

The stable finite-PL theorem produces the exact complement obstruction needed by the simplest route.

Equations

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

theorem NRR.AAK.stableRefinedPL_implies_simplestRouteObstruction (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) : SimplestRouteObstructionTheorem

Stable homotopy invariance implies the simplest-route obstruction statement.

theorem NRR.AAK.avvakumov_akopyan_karasev_of_stableRefinedPL (HPL : FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Conditional arbitrary-n AAK endpoint. This statement does not assume equality of counts for arbitrary raw regular approximations.

theorem NRR.AAK.avvakumov_akopyan_karasev_of_relativeStableCollar (HC : FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarExistenceTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Relative stable-collar existence supplies the stable homotopy-invariance input used to prove the arbitrary-n AAK endpoint.

theorem NRR.AAK.avvakumov_akopyan_karasev_of_relativeStableCollarConstruction (HC : FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarConstructionTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Fully geometric S6 reduction. It is enough to construct the endpoint-identified collar, prove that its endpoint-adjusted affine cells avoid the origin, provide nonhorizontal facet/minor witnesses, and identify purely horizontal codimension-two faces with the supplied stable endpoint skeletons. Compactness, horizontal facet regularity, polynomial nontriviality, relative perturbation, and finite Stokes are then automatic.