The common-level staircase prism as an explicit relative-collar cell system

This module turns the already formalized fully refined staircase prism into the concrete cell-system interface used by the endpoint-identified relative collar. The cells are prime-orbit representatives; equivariant values on all translates are reconstructed later by the decorated vertex-parameter quotient.

The horizontal boundary of this cell system is at the combined spatial level N + L. A later module identifies its horizontal facet quotient with RefinedAffineMap.TopCell hp (N + L) and packages the exact signed incidence formula.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.selectedTopOrbit {p : ℕ} (hp : Nat.Prime p) : PrimeOrbitCycle.TopOrbit hp

A selected top orbit used only to witness that the finite middle-prism cell type is nonempty.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.defaultTopCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : RefinedAffineMap.TopCell hp N

A canonical refined spatial cell at any level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.defaultPrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : SubdivisionPrismCharts.PrismCell hp N L

A canonical fully refined prism cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.vertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : EquivariantPrismVertexParameters.CylinderPoint p

The geometric cylinder vertex of one fully refined middle-prism cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.chart {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : EquivariantPrismVertexParameters.CylinderPoint p

The geometric affine chart of one fully refined middle-prism cell.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.chart_vertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : chart hp N L q (SphereOddDegree.FiniteSimplex.vertex i) = vertex hp N L q i

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.cellSystem {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp (N + L) (N + L) (N + L) L

The existing refined staircase prism supplies a genuine explicit finite cell system whose two horizontal triangulations both have combined level N + L.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrism.middleGlobalVertexAction {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : MulAction (↥(PrimeSymmetry p)) (ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (cellSystem hp N L))

The generic quotient action specialized to the explicit middle-prism carrier.

Equations

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