Frozen positive-support safety for endpoint stacks and composed collars

The Route B frozen-support condition is proved one-sidedly. A lower endpoint stack is safe when all positive barycentric support lies at time zero; reversal gives the corresponding upper safety. Collar composition then converts those two one-sided statements into the global frozen-parameter condition because the two half-cylinder embeddings have no other horizontal points.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.LowerPositiveSupportRaySafe {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) : Prop

Lower one-sided version of frozen positive-support safety.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.UpperPositiveSupportRaySafe {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) : Prop

Upper one-sided version of frozen positive-support safety.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.exists_positive_coordinate {p : ℕ} (w : StandardSimplex p) : ∃ (k : Fin (p + 1)), 0 < ↑w k

Every simplex weight has a positive coordinate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.lowerSpatialWeight_not_interior (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (i j : Fin (d + 2)) (hij : i ≠ j) (hzeros : w i = 0 ∧ w j = 0) (hsupport : ∀ (k : Fin (d + 2)), 0 < w k → ↑(RelativeSubdivisionCylinderCombinatorics.vertex d q k).2 = 0) : ¬(StandardSimplex.ofDelta (RelativeSubdivisionCylinderCombinatorics.spatialPoint d q w)).IsInterior

In one local subdivision cylinder, positive support at time zero together with two vanishing source coordinates maps to a proper face of the coarse lower simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.oneStep_lowerPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) : LowerPositiveSupportRaySafe hp (RelativeSubdivisionOneStepCells.cellSystem hp A.level) (CompatibleChartMapOneStep.assignment hp (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A.toRegularApproximation))

The first affine-pullback endpoint layer is lower-support safe.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.lowerSafe_combined_left {p N₀ N₁ : ℕ} (hp : Nat.Prime p) {Nmid M₀ L₀ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hC : LowerPositiveSupportRaySafe hp C a) : LowerPositiveSupportRaySafe hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)

Lower safety is inherited by a composition from its left component.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.upperSafe_reverse {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (hC : LowerPositiveSupportRaySafe hp C a) : UpperPositiveSupportRaySafe hp (ExplicitAffineRelativeCollarReverse.reverseCells C) (ExplicitAffineRelativeCollarAssignmentReverse.reverseAssignment C a)

Reversal converts lower-support safety into upper-support safety.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.frozenSafe_combined {p N₀ N₁ : ℕ} (hp : Nat.Prime p) {Nmid M₀ L₀ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hC : LowerPositiveSupportRaySafe hp C a) (hD : UpperPositiveSupportRaySafe hp D b) : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)

Composing a lower-safe left collar and an upper-safe right collar gives the exact frozen positive-support condition used by Route B.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFrozenSupportGeometry.build_lowerPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (k : ℕ) : LowerPositiveSupportRaySafe hp (EndpointStackIteratedAffinePullback.positiveWitness hp A.level k).collar.cells (EndpointStackIteratedAffinePullback.build hp A.toRegularApproximation k).assignment

Every iterated positive endpoint stack is lower-support safe.