Facet-polynomial nontriviality for the affine-pullback full collar

The lower endpoint stack carries lower-relative facet targets by induction. Reversal gives the upper-relative targets. The middle prism is strictly internal in the final three-region collar, so universal triangular targets suffice there. The two composition steps therefore yield exact frozen-relative targets for every final cell and facet.

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

Every iterated lower endpoint stack admits boundary-respecting regular facet targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.lowerCollar_lowerFacetTargets {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : RouteBEndpointFacetTargets.LowerFacetTargets hp (StableFullCollarConstructionAffinePullback.lowerCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.lowerAssignment hp A0 A1 L)

The transported lower stack carries lower-relative facet targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.upperCollar_upperFacetTargets {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : RouteBFacetTargetComposition.UpperFacetTargets hp (StableFullCollarConstructionAffinePullback.upperCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.upperAssignment hp A0 A1 L)

The transported reversed upper stack carries upper-relative facet targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.lowerMiddleCollar_lowerFacetTargets {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 : ℕ) : RouteBEndpointFacetTargets.LowerFacetTargets hp (StableFullCollarConstructionAffinePullback.lowerMiddleCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.lowerMiddleAssignment hp F0 F1 H A0 A1 L)

The lower two regions keep lower-relative facet targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.fullCollar_frozenFacetTargets {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 : ℕ) : RouteBFacetTargetComposition.FrozenFacetTargets hp (StableFullCollarConstructionAffinePullback.fullCollar hp A0 A1 L).cells (StableFullCollarConstructionAffinePullback.fullAssignment hp F0 F1 H A0 A1 L)

The complete three-region collar carries frozen-relative facet targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.fineFullCollarData_frozenFacetTargets {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) : RouteBFacetTargetComposition.FrozenFacetTargets hp (StableFullCollarConstructionAffinePullback.fineFullCollarData hp F0 F1 H A0 A1).collar.cells (StableFullCollarConstructionAffinePullback.fineFullCollarData hp F0 F1 H A0 A1).assignment

The concrete Step 4 collar has a frozen-relative regular target for every local facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.baseData_allFacetRegularityWitnesses {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.AllFacetRegularityWitnesses hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment

Pointwise regularity witnesses for every boundary-restricted facet polynomial.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBFacetGeometry.baseData_allRestrictedFacetPolynomialsNonzero {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.AllRestrictedFacetPolynomialsNonzero hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment

Every restricted facet determinant polynomial for the concrete collar is nonzero.