Thin-time stacks of unrefined Fox--Neuwirth staircase prisms

The fully barycentrically refined middle prism changes the horizontal spatial triangulation from level N to level N + L. For a boundary-relative comparison this is undesirable: the supplied stable endpoint approximation must remain fixed on its exact level.

This module refines only the interval direction. A thin stack with m > 0 consists of m copies of the unrefined (L = 0) staircase prism. Copy r : Fin m is embedded in the time slab [r/m, (r+1)/m]. Spatial coordinates and all prime-orbit data are unchanged.

The construction below supplies the genuine affine-cell system. The subsequent boundary module collects quotient-facet incidences: side facets cancel inside each slab, adjacent horizontal facets cancel between consecutive slabs, and only the first lower and final upper boundary remain.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabTime (m : ℕ) (hm : 0 < m) (r : Fin m) (t : ↑(Set.Icc 0 1)) : ↑(Set.Icc 0 1)

Affine rescaling of the unit interval onto slab r of a positive m-slab partition.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabTime m hm r t = ⟨(↑↑r + ↑t) / ↑m, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabTime_val (m : ℕ) (hm : 0 < m) (r : Fin m) (t : ↑(Set.Icc 0 1)) : ↑(slabTime m hm r t) = (↑↑r + ↑t) / ↑m

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabPoint {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (z : EquivariantPrismVertexParameters.CylinderPoint p) : EquivariantPrismVertexParameters.CylinderPoint p

Embed one cylinder point into a specified thin time slab.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabPoint_spatial {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (z : EquivariantPrismVertexParameters.CylinderPoint p) : (slabPoint m hm r z).spatial = z.spatial

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabPoint_time {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (z : EquivariantPrismVertexParameters.CylinderPoint p) : ↑(slabPoint m hm r z).time = (↑↑r + ↑z.time) / ↑m

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabPoint_smul {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (g : ↥(PrimeSymmetry p)) (z : EquivariantPrismVertexParameters.CylinderPoint p) : slabPoint m hm r (g • z) = g • slabPoint m hm r z

Time rescaling commutes with prime symmetry.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.slabPoint_injective {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) : Function.Injective (slabPoint m hm r)

Rescaling into one fixed positive slab is injective.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.Cell {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) : Type

One top-cell representative in a thin stack.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.cellFintype {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) : Fintype (Cell hp N m)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.cellFintype hp N m = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.cellDecidableEq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) : DecidableEq (Cell hp N m)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.cellDecidableEq hp N m = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.defaultCell {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) : Cell hp N m

A canonical cell witnessing nonemptiness of a positive thin stack.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.vertex {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : Cell hp N m) (i : Fin (p + 1)) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric vertex of a thin-stack cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.chart {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : Cell hp N m) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : EquivariantPrismVertexParameters.CylinderPoint p

Affine chart of a thin-stack cell.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.chart_vertex {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : Cell hp N m) (i : Fin (p + 1)) : chart hp N m hm q (SphereOddDegree.FiniteSimplex.vertex i) = vertex hp N m hm q i

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabs.cellSystem {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N N N m

The thin stack is a genuine affine cell system with unchanged spatial endpoint level N.

Equations

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