Relative subdivision collars for arbitrary endpoint levels

The explicit one-step collar is iterated by the abstract collar-composition operation. Reversing one such stack supplies a collar from a common refinement down to the independently prescribed upper endpoint. Composing the lower stack with that reversed upper stack gives a genuine endpoint-identified affine collar for any two subdivision levels.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.Witness {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ : ℕ) : Type 1

Existential bookkeeping wrapper for the common and time-refinement levels of a collar.

• commonLevel : ℕ

  The common spatial subdivision level of the endpoint collar.

• timeLevel : ℕ

  The time-refinement level of the endpoint collar.

• collar : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ self.commonLevel self.timeLevel

  The endpoint-identified relative affine collar at the chosen levels.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.identityWitness {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Witness hp N N

Equal-level identity collar, represented by one unrefined thin slab.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.oneStepWitness {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Witness hp N (N + 1)

One-step subdivision witness.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.reverseWitness {p : ℕ} {hp : Nat.Prime p} {N₀ N₁ : ℕ} (C : Witness hp N₀ N₁) : Witness hp N₁ N₀

Reverse an existential collar witness.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.composeWitness {p : ℕ} {hp : Nat.Prime p} {N₀ Nmid N₁ : ℕ} (C : Witness hp N₀ Nmid) (D : Witness hp Nmid N₁) : Witness hp N₀ N₁

Compose two existential collar witnesses.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.forwardWitness {p : ℕ} (hp : Nat.Prime p) (N k : ℕ) : Witness hp N (N + k)

Iterate the one-step cylinder k times.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.orderedWitness {p : ℕ} (hp : Nat.Prime p) (N M : ℕ) (hNM : N ≤ M) : Witness hp N M

A forward subdivision collar between any ordered pair of levels.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.endpointWitnessAt {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M : ℕ) (h₀ : N₀ ≤ M) (h₁ : N₁ ≤ M) : Witness hp N₀ N₁

Relative subdivision collar through any preselected common refinement level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.endpointWitness {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ : ℕ) : Witness hp N₀ N₁

Relative subdivision collar for arbitrary independent endpoint levels.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionEndpointCollar.relativeAffineCollarExists {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ : ℕ) : ∃ (M : ℕ) (L : ℕ), ExplicitAffineRelativeCollar.RelativeAffineCollarExists hp N₀ N₁ M L

Existence of a genuine endpoint-identified relative affine collar for arbitrary levels.