Concrete fine full-collar construction by affine pullback

This module closes Step 4. The collar is assembled from three regions:

1. an iterated affine-pullback stack from the lower endpoint level to a common refined level;
2. a sufficiently fine staircase prism sampling the PL-ended compatible chart homotopy; and
3. the reversal of an iterated affine-pullback stack from the upper endpoint level to the same common refined level.

All three assignments use the original endpoint PL chart maps as their seam invariants. The carrier theorem therefore gives literal equality on both composition seams. Endpoint stacks avoid the origin exactly, while the middle prism avoids it by the compactness/oscillation estimate. The external horizontal values are the supplied stable approximation samples.

The endpoint stacks are produced at the level A.level + (k + 1) while the middle prism lives at baseLevel A0 A1 + L. These two natural numbers are equal but not definitionally equal, so the stacks are transported with castEndpointCollar; castEndpoint_property moves every property of a collar together with its assignment across such a transport.

Transport of collar data along equal spatial levels

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpointCollar {p : ℕ} {hp : Nat.Prime p} {N₀ N₀' N₁ N₁' M T : ℕ} (h₀ : N₀ = N₀') (h₁ : N₁ = N₁') (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M T) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀' N₁' M T

Transport an endpoint-identified collar along equalities of its two endpoint levels.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpointCollar h₀ h₁ C = h₀ ▸ h₁ ▸ C

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpointCollar_rfl {p : ℕ} {hp : Nat.Prime p} {N₀ N₁ M T : ℕ} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M T) : castEndpointCollar ⋯ ⋯ C = C

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpointAssignment {p : ℕ} {hp : Nat.Prime p} {N₀ N₀' N₁ N₁' M T : ℕ} (h₀ : N₀ = N₀') (h₁ : N₁ = N₁') (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M T) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C.cells) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (castEndpointCollar h₀ h₁ C).cells

Transport an assignment along the same equalities of endpoint levels.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpointAssignment h₀ h₁ C a = h₀ ▸ h₁ ▸ a

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.castEndpoint_property {p : ℕ} {hp : Nat.Prime p} {N₀ N₀' N₁ N₁' M T : ℕ} (P : (A B : ℕ) → (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A B M T) → ExplicitAffineRelativeCollar.Parameters.Assignment hp D.cells → Prop) (h₀ : N₀ = N₀') (h₁ : N₁ = N₁') (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M T) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C.cells) (h : P N₀ N₁ C a) : P N₀' N₁' (castEndpointCollar h₀ h₁ C) (castEndpointAssignment h₀ h₁ C a)

Every property of a collar together with its assignment survives the level transport.

Prism boundary representation at a transported level

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lower_boundary_represents_base_cast {p : ℕ} (hp : Nat.Prime p) {N0 d M : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N0) (h : N0 + d = M) {K1 : CompatibleRefinedChartHomotopy.ChartMap hp M} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp M (CompatibleRefinedChartHomotopy.ChartMap.castLevel h (K.refine d)) K1) (L : ℕ) : ChartMapCollarRepresentation.RepresentsAtTime (RelativeCollarMiddlePrism.cellSystem hp M L) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp M L) (CompatibleRefinedChartHomotopyPrism.assignment hp J L)) 0

Lower prism boundary representation when the homotopy is stated at a level equal, but not definitionally equal, to the refined endpoint level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upper_boundary_represents_base_cast {p : ℕ} (hp : Nat.Prime p) {N0 d M : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N0) (h : N0 + d = M) {K0 : CompatibleRefinedChartHomotopy.ChartMap hp M} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp M K0 (CompatibleRefinedChartHomotopy.ChartMap.castLevel h (K.refine d))) (L : ℕ) : ChartMapCollarRepresentation.RepresentsAtTime (RelativeCollarMiddlePrism.cellSystem hp M L) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp M L) (CompatibleRefinedChartHomotopyPrism.assignment hp J L)) 1

Upper prism boundary representation when the homotopy is stated at a level equal, but not definitionally equal, to the refined endpoint level.

The three collar regions

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.baseLevel {p : ℕ} {hp : Nat.Prime p} {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) : ℕ

Base level at which the PL-ended chart homotopy is defined.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.baseLevel A0 A1 = A0.level + A1.level + 1

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerStackIndex {p : ℕ} {hp : Nat.Prime p} {F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ℕ

Number of one-step layers below a middle prism with additional refinement L.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerStackIndex A1 L = A1.level + L

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperStackIndex {p : ℕ} {hp : Nat.Prime p} {F0 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (L : ℕ) : ℕ

Number of one-step layers above a middle prism with additional refinement L.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperStackIndex A0 L = A0.level + L

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerLevel_eq {p : ℕ} {hp : Nat.Prime p} {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : A0.level + (lowerStackIndex A1 L + 1) = baseLevel A0 A1 + L

The lower stack reaches exactly the middle prism level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperLevel_eq {p : ℕ} {hp : Nat.Prime p} {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : A1.level + (upperStackIndex A0 L + 1) = baseLevel A0 A1 + L

The upper stack reaches exactly the middle prism level.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleHomotopy {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) : CompatibleRefinedChartHomotopy.ChartHomotopy hp (CompatibleRefinedChartHomotopy.baseCommonLevel A0 A1) (CompatibleRefinedChartHomotopy.originalPLMap hp A0.toRegularApproximation (A1.level + 1)) (CompatibleRefinedChartHomotopy.ChartMap.castLevel ⋯ (CompatibleRefinedChartHomotopy.originalPLMap hp A1.toRegularApproximation (A0.level + 1)))

The PL-ended chart homotopy used in the middle region.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleRefinement {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) : ℕ

Chosen fine prism level for the middle region.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleRefinement hp F0 F1 H A0 A1 = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleRefinement_avoidsOrigin {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) (q : SubdivisionPrismCharts.PrismCell hp (baseLevel A0 A1) (middleRefinement hp F0 F1 H A0 A1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp (baseLevel A0 A1) (middleRefinement hp F0 F1 H A0 A1)) (CompatibleRefinedChartHomotopyPrism.assignment hp (middleHomotopy hp F0 F1 H A0 A1) (middleRefinement hp F0 F1 H A0 A1)) q).AvoidsOrigin

Origin avoidance for the chosen middle refinement.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerCollar {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A0.level (baseLevel A0 A1 + L) (EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).commonLevel (EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).timeLevel

Lower endpoint stack, transported to the common middle level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperCollar {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp (baseLevel A0 A1 + L) A1.level (EndpointStackIteratedAffinePullback.positiveWitness hp A1.level (upperStackIndex A0 L)).commonLevel (EndpointStackIteratedAffinePullback.positiveWitness hp A1.level (upperStackIndex A0 L)).timeLevel

Upper endpoint stack, reversed and transported from the common middle level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerAssignment {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (lowerCollar hp A0 A1 L).cells

The transported lower stack assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperAssignment {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (upperCollar hp A0 A1 L).cells

The transported reversed upper stack assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleCollar {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar hp (baseLevel A0 A1 + L) (baseLevel A0 A1 + L) (baseLevel A0 A1 + L) L

Fine common-level middle prism with all seam data, but without the unnecessary standalone horizontal-facet exhaustiveness requirement.

Equations

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

The assembled three-region collar

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middleAssignment {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.Parameters.Assignment hp (middleCollar hp A0 A1 L).cells

The middle prism assignment sampled from the PL-ended chart homotopy.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lower_represents {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ChartMapCollarRepresentation.Represents (lowerCollar hp A0 A1 L).cells (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A0.toRegularApproximation) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (lowerCollar hp A0 A1 L).cells (lowerAssignment hp A0 A1 L))

The lower stack represents the lower original PL chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upper_represents {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ChartMapCollarRepresentation.Represents (upperCollar hp A0 A1 L).cells (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A1.toRegularApproximation) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (upperCollar hp A0 A1 L).cells (upperAssignment hp A0 A1 L))

The reversed upper stack represents the upper original PL chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middle_represents_lower {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 : ℕ) : ChartMapCollarRepresentation.RepresentsAtTime (middleCollar hp A0 A1 L).cells (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A0.toRegularApproximation) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (middleCollar hp A0 A1 L).cells (middleAssignment hp F0 F1 H A0 A1 L)) 0

At time zero the middle prism represents the lower original PL chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.middle_represents_upper {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 : ℕ) : ChartMapCollarRepresentation.RepresentsAtTime (middleCollar hp A0 A1 L).cells (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A1.toRegularApproximation) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (middleCollar hp A0 A1 L).cells (middleAssignment hp F0 F1 H A0 A1 L)) 1

At time one the middle prism represents the upper original PL chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerSeam {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 : ℕ) : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible (lowerCollar hp A0 A1 L).cells (middleCollar hp A0 A1 L).cells (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (lowerCollar hp A0 A1 L).cells (lowerAssignment hp A0 A1 L)) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (middleCollar hp A0 A1 L).cells (middleAssignment hp F0 F1 H A0 A1 L))

The lower seam of the three-region decomposition.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerMiddleCollar {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar hp A0.level (baseLevel A0 A1 + L) (max (EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).commonLevel (baseLevel A0 A1 + L)) ((EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).timeLevel + L + 1)

The lower stack composed with the middle prism.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerMiddleAssignment {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.Parameters.Assignment hp (lowerMiddleCollar hp A0 A1 L).cells

The assignment of the lower two regions.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperSeam {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 : ℕ) : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible (lowerMiddleCollar hp A0 A1 L).cells (upperCollar hp A0 A1 L).cells (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (lowerMiddleCollar hp A0 A1 L).cells (lowerMiddleAssignment hp F0 F1 H A0 A1 L)) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (upperCollar hp A0 A1 L).cells (upperAssignment hp A0 A1 L))

The upper seam of the three-region decomposition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lowerMiddle_lowerFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (s : (lowerMiddleCollar hp A0 A1 L).cells.Facet) : (lowerMiddleCollar hp A0 A1 L).cells.IsLowerFacet s → ∃ (q : RefinedAffineMap.TopCell hp A0.level), (lowerMiddleCollar hp A0 A1 L).lowerFacet q = s

External lower facets of the composed lower region are exhaustive.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upperDescribed_upperFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (s : (ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar.ofEndpointIdentified (upperCollar hp A0 A1 L)).cells.Facet) : (ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar.ofEndpointIdentified (upperCollar hp A0 A1 L)).cells.IsUpperFacet s → ∃ (q : RefinedAffineMap.TopCell hp A1.level), (ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar.ofEndpointIdentified (upperCollar hp A0 A1 L)).upperFacet q = s

External upper facets of the upper region are exhaustive.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fullCollar {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A0.level A1.level (max (max (EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).commonLevel (baseLevel A0 A1 + L)) (EndpointStackIteratedAffinePullback.positiveWitness hp A1.level (upperStackIndex A0 L)).commonLevel) ((EndpointStackIteratedAffinePullback.positiveWitness hp A0.level (lowerStackIndex A1 L)).timeLevel + L + 1 + (EndpointStackIteratedAffinePullback.positiveWitness hp A1.level (upperStackIndex A0 L)).timeLevel + 1)

The complete three-region collar.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fullAssignment {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.Parameters.Assignment hp (fullCollar hp A0 A1 L).cells

The complete three-region assignment.

Equations

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

Origin avoidance and horizontal endpoint values

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lower_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (q : (lowerCollar hp A0 A1 L).cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (lowerCollar hp A0 A1 L).cells (lowerAssignment hp A0 A1 L) q).AvoidsOrigin

The lower stack avoids the origin cellwise.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upper_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (q : (upperCollar hp A0 A1 L).cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (upperCollar hp A0 A1 L).cells (upperAssignment hp A0 A1 L) q).AvoidsOrigin

The reversed upper stack avoids the origin cellwise.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.full_avoidsOrigin {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) (q : (fullCollar hp A0 A1 (middleRefinement hp F0 F1 H A0 A1)).cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (fullCollar hp A0 A1 (middleRefinement hp F0 F1 H A0 A1)).cells (fullAssignment hp F0 F1 H A0 A1 (middleRefinement hp F0 F1 H A0 A1)) q).AvoidsOrigin

The full collar avoids the origin cellwise.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.lower_lowerFixed {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (s : (lowerCollar hp A0 A1 L).cells.VertexSlot) : ↑((lowerCollar hp A0 A1 L).cells.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (lowerCollar hp A0 A1 L).cells (lowerAssignment hp A0 A1 L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (lowerCollar hp A0 A1 L).cells s) = A0.map ((lowerCollar hp A0 A1 L).cells.slotPoint s).spatial

Exact lower endpoint samples on the lower stack.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.upper_upperFixed {p : ℕ} (hp : Nat.Prime p) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (L : ℕ) (s : (upperCollar hp A0 A1 L).cells.VertexSlot) : ↑((upperCollar hp A0 A1 L).cells.slotPoint s).time = 1 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (upperCollar hp A0 A1 L).cells (upperAssignment hp A0 A1 L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (upperCollar hp A0 A1 L).cells s) = A1.map ((upperCollar hp A0 A1 L).cells.slotPoint s).spatial

Exact upper endpoint samples on the reversed upper stack.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.full_lowerFixed {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 : ℕ) (s : (fullCollar hp A0 A1 L).cells.VertexSlot) : ↑((fullCollar hp A0 A1 L).cells.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (fullCollar hp A0 A1 L).cells (fullAssignment hp F0 F1 H A0 A1 L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (fullCollar hp A0 A1 L).cells s) = A0.map ((fullCollar hp A0 A1 L).cells.slotPoint s).spatial

Exact lower endpoint samples on the full collar.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.full_upperFixed {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 : ℕ) (s : (fullCollar hp A0 A1 L).cells.VertexSlot) : ↑((fullCollar hp A0 A1 L).cells.slotPoint s).time = 1 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (fullCollar hp A0 A1 L).cells (fullAssignment hp F0 F1 H A0 A1 L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (fullCollar hp A0 A1 L).cells s) = A1.map ((fullCollar hp A0 A1 L).cells.slotPoint s).spatial

Exact upper endpoint samples on the full collar.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fineFullCollarData {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) : StableFullCollarOriginMargin.FineFullCollarData hp H A0 A1

Concrete full fine-collar data.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fineFullCollarData_collar {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) : (fineFullCollarData hp F0 F1 H A0 A1).collar = fullCollar hp A0 A1 (middleRefinement hp F0 F1 H A0 A1)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fineFullCollarData_assignment {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) : (fineFullCollarData hp F0 F1 H A0 A1).assignment = fullAssignment hp F0 F1 H A0 A1 (middleRefinement hp F0 F1 H A0 A1)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarConstructionAffinePullback.fineFullCollarConstruction_affinePullback : StableFullCollarOriginMargin.FineFullCollarConstructionTheorem

Step 4: the full fine collar exists for every supplied stable endpoint pair and zero-free homotopy.