Geometric Route B inputs for the affine-pullback full collar

This module proves the frozen positive-support certificate by following the actual three-region Step 4 decomposition. The lower iterated endpoint stack is lower-support safe, its composition with the middle region remains lower-support safe, and the reversed upper stack is upper-support safe. The final half-cylinder composition therefore satisfies Route B's exact frozen-parameter condition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.lowerCollar_lowerPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : RouteBFrozenSupportGeometry.LowerPositiveSupportRaySafe hp (StableFullCollarConstructionAffinePullback.lowerCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.lowerAssignment hp A0 A1 L)

The transported lower stack is lower-support safe.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.upperCollar_upperPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : RouteBFrozenSupportGeometry.UpperPositiveSupportRaySafe hp (StableFullCollarConstructionAffinePullback.upperCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.upperAssignment hp A0 A1 L)

The transported reversed upper stack is upper-support safe.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.lowerMiddleCollar_lowerPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : RouteBFrozenSupportGeometry.LowerPositiveSupportRaySafe hp (StableFullCollarConstructionAffinePullback.lowerMiddleCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.lowerMiddleAssignment hp F0 F1 H A0 A1 L)

The lower two regions remain lower-support safe.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.fullCollar_frozenPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (StableFullCollarConstructionAffinePullback.fullCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.fullAssignment hp F0 F1 H A0 A1 L)

The complete three-region assignment is frozen-support safe.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.fineFullCollarData_frozenPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (StableFullCollarConstructionAffinePullback.fineFullCollarData hp F0 F1 H A0 A1).collar.cells (StableFullCollarConstructionAffinePullback.fineFullCollarData hp F0 F1 H A0 A1).assignment

The concrete Step 4 assignment satisfies Route B's support-level frozen safety condition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBGeometry.baseData_frozenPositiveSupportRaySafe {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment

Frozen-support safety for the concrete quantitative Step 5 data.