Signed boundary of a thin-time stack

A thin stack is a disjoint union of unrefined staircase prisms whose geometric copies meet along successive time slices. This file proves its pointwise signed boundary formula without classifying all quotient facets. For one quotient facet s, pull its characteristic function back to every slab and apply the arbitrary prime-invariant weighted boundary theorem for the ordinary staircase prism. The upper endpoint term of slab r is literally the lower endpoint term of slab r+1, so the finite sum telescopes. Only time zero and time one remain.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.BaseCells {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp (N + 0) (N + 0) (N + 0) 0

The unrefined staircase-prism cell system used in every slab.

Equations

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

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.StackCells {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N N N m

The complete m-slab cell system.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)

Apply the affine time rescaling of slab r to an arbitrary facet map.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap_fst {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) : (slabFacetMap m hm r tau x).1 = (tau x).1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap_time {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) : ↑(slabFacetMap m hm r tau x).2 = (↑↑r + ↑(tau x).2) / ↑m

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap_translate (p m : ℕ) (hm : 0 < m) (r : Fin m) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : slabFacetMap m hm r (EquivariantPrismNonhorizontalCancellation.translateFacetMap p g tau) = EquivariantPrismNonhorizontalCancellation.translateFacetMap p g (slabFacetMap m hm r tau)

Slab rescaling commutes with simultaneous prime translation.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.stackOccurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) (o : (BaseCells hp N).FacetOccurrence) : (StackCells hp N m hm).FacetOccurrence

Embed one base-prism facet occurrence into slab r.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.stackOccurrence hp N m hm r o = ((r, o.1), o.2)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.facetSignature_stackOccurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) (o : (BaseCells hp N).FacetOccurrence) : (StackCells hp N m hm).facetSignature (stackOccurrence hp N m hm r o) = fun (i : Fin p) => RelativeCollarThinSlabs.slabPoint m hm r ((BaseCells hp N).facetSignature o i)

Ordered geometric vertices of an embedded occurrence are the rescaled base vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.mapVertexSignature_slabOccurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) (o : (BaseCells hp N).FacetOccurrence) : EquivariantPrismNonhorizontalCancellation.mapVertexSignature (slabFacetMap m hm r (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N 0 o)) = (StackCells hp N m hm).facetSignature (stackOccurrence hp N m hm r o)

The transformed old occurrence map and the explicit stack occurrence have the same ordered geometric vertex tuple.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.stackFacetOrbitIndicator {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Characteristic weight of one ordered prime-orbit facet of the complete thin stack.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.stackFacetOrbitIndicator_translate {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : stackFacetOrbitIndicator hp N m hm s (EquivariantPrismNonhorizontalCancellation.translateFacetMap p g tau) = stackFacetOrbitIndicator hp N m hm s tau

The stack characteristic weight is invariant under simultaneous prime translation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetOrbitIndicator {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (r : Fin m) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Pull the stack-facet characteristic weight back to the ordinary prism maps in slab r.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetOrbitIndicator_translate {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (r : Fin m) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : slabFacetOrbitIndicator hp N m hm s r (EquivariantPrismNonhorizontalCancellation.translateFacetMap p g tau) = slabFacetOrbitIndicator hp N m hm s r tau

The pulled-back characteristic weight is prime invariant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.stackFacetOrbitIndicator_occurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (o : (StackCells hp N m hm).FacetOccurrence) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) (htau : EquivariantPrismNonhorizontalCancellation.mapVertexSignature tau = (StackCells hp N m hm).facetSignature o) : stackFacetOrbitIndicator hp N m hm s tau = if (StackCells hp N m hm).facetClass o = s then 1 else 0

On an actual stack occurrence, the characteristic weight is the Kronecker delta of its quotient-facet class.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetOrbitIndicator_occurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (r : Fin m) (o : (BaseCells hp N).FacetOccurrence) : slabFacetOrbitIndicator hp N m hm s r (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N 0 o) = if (StackCells hp N m hm).facetClass (stackOccurrence hp N m hm r o) = s then 1 else 0

On an actual base occurrence embedded in slab r, the pulled-back weight is the Kronecker weight of its stack quotient facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.facetIncidence_eq_sum_slabOccurrencePairing {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) : (StackCells hp N m hm).facetIncidence s = ∑ r : Fin m, RelativeCollarMiddlePrismBoundary.occurrencePairing hp N 0 (slabFacetOrbitIndicator hp N m hm s r)

The signed incidence of a stack quotient facet is the sum of the ordinary staircase occurrence pairings pulled back from each slab.

Mesh endpoint terms and telescoping

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.meshTime (m : ℕ) (hm : 0 < m) (k : Fin (m + 1)) : ↑(Set.Icc 0 1)

The k-th time node of the uniform m-slab mesh.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.meshTime m hm k = ⟨↑↑k / ↑m, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.meshTime_val (m : ℕ) (hm : 0 < m) (k : Fin (m + 1)) : ↑(meshTime m hm k) = ↑↑k / ↑m

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.meshEndpointMap {p : ℕ} (m : ℕ) (hm : 0 < m) (k : Fin (m + 1)) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)

Place a spatial facet map on one node of the uniform time mesh.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap_lowerEndpointMap {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : slabFacetMap m hm r (EquivariantPrismNonhorizontalCancellation.lowerEndpointMap sigma) = meshEndpointMap m hm r.castSucc sigma

The lower face of slab r is mesh node r.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.slabFacetMap_upperEndpointMap {p : ℕ} (m : ℕ) (hm : 0 < m) (r : Fin m) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : slabFacetMap m hm r (EquivariantPrismNonhorizontalCancellation.upperEndpointMap sigma) = meshEndpointMap m hm r.succ sigma

The upper face of slab r is mesh node r+1.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.meshEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (k : Fin (m + 1)) : ZMod p

Pair the spatial Fox--Neuwirth chain at level N with one stack quotient facet on a fixed mesh node.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.lowerEndpointPairing_slab_eq_mesh {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (r : Fin m) : RelativeCollarMiddlePrismBoundary.lowerEndpointPairing hp N 0 (slabFacetOrbitIndicator hp N m hm s r) = meshEndpointPairing hp N m hm s r.castSucc

At refinement length zero, a slab's lower endpoint pairing is its lower mesh-node pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.upperEndpointPairing_slab_eq_mesh {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (r : Fin m) : RelativeCollarMiddlePrismBoundary.upperEndpointPairing hp N 0 (slabFacetOrbitIndicator hp N m hm s r) = meshEndpointPairing hp N m hm s r.succ

At refinement length zero, a slab's upper endpoint pairing is its upper mesh-node pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.sum_fin_succ_sub {R : Type} [AddCommGroup R] (m : ℕ) (a : Fin (m + 1) → R) : ∑ r : Fin m, (a r.succ - a r.castSucc) = a (Fin.last m) - a 0

Finite telescoping identity in the indexing form used by a uniform slab stack.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.facetIncidence_eq_last_sub_first_mesh {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) : (StackCells hp N m hm).facetIncidence s = meshEndpointPairing hp N m hm s (Fin.last m) - meshEndpointPairing hp N m hm s 0

Pointwise boundary formula for the complete thin stack: all internal time nodes telescope.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.lowerBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) : ZMod p

External lower boundary coefficient of a thin stack.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.upperBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) : ZMod p

External upper boundary coefficient of a thin stack.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.isLowerFacet_of_meshFirstIndicator_ne_zero {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) (h : stackFacetOrbitIndicator hp N m hm s (meshEndpointMap m hm 0 sigma) ≠ 0) : (StackCells hp N m hm).IsLowerFacet s

A nonzero lower external coefficient forces the represented stack facet to lie at time zero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.isUpperFacet_of_meshLastIndicator_ne_zero {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) (h : stackFacetOrbitIndicator hp N m hm s (meshEndpointMap m hm (Fin.last m) sigma) ≠ 0) : (StackCells hp N m hm).IsUpperFacet s

A nonzero upper external coefficient forces the represented stack facet to lie at time one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.lowerBoundaryCoefficient_zero_of_not_lower {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (hs : ¬(StackCells hp N m hm).IsLowerFacet s) : lowerBoundaryCoefficient hp N m hm s = 0

Lower coefficients vanish away from the external lower boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.upperBoundaryCoefficient_zero_of_not_upper {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (StackCells hp N m hm).Facet) (hs : ¬(StackCells hp N m hm).IsUpperFacet s) : upperBoundaryCoefficient hp N m hm s = 0

Upper coefficients vanish away from the external upper boundary.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsBoundary.collar {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N N N m

The complete thin-time stack as a pointwise Fox--Neuwirth relative affine collar.

Equations

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