Pointwise boundary of the one-step relative subdivision cylinder

This module lifts the arbitrary-weight boundary theorem for the recursive standard-simplex cylinder over every refined Fox--Neuwirth top cell. A characteristic weight of one ordered prime-orbit facet converts that weighted identity into the pointwise facet-incidence formula.

The only global term not already contained in the local cylinder theorem is the recursively triangulated spatial-side chain. It vanishes after summing over the refined Fox--Neuwirth orbit cycle: iterated barycentric-subdivision boundary moves it to the original orbit-cycle boundary, and prime invariance of the quotient-facet characteristic weight lets orbit_boundary_pairing_eq_zero apply.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.liftTuple {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (v : Fin (p - 1 + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) × ↑(Set.Icc 0 1)) : Fin p → EquivariantPrismVertexParameters.CylinderPoint p

Lift an ordered local-cylinder tuple through one refined Fox--Neuwirth chart.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetOrbitIndicator {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (v : Fin p → EquivariantPrismVertexParameters.CylinderPoint p) : ZMod p

Characteristic weight of one ordered prime-orbit facet, evaluated on an arbitrary geometric vertex tuple. The existential formulation makes it available to the local arbitrary-weight boundary theorem without choosing a quotient representative.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetOrbitIndicator_smul {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (g : ↥(PrimeSymmetry p)) (v : Fin p → EquivariantPrismVertexParameters.CylinderPoint p) : (facetOrbitIndicator hp N s fun (i : Fin p) => g • v i) = facetOrbitIndicator hp N s v

Simultaneous prime translation does not change the quotient-facet characteristic weight.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.fullFacetIndexEquiv {p : ℕ} (hp : Nat.Prime p) : Fin (p + 1) ≃ Fin (p - 1 + 2)

Identify global facet indices with the dimension-normalized local cylinder indices.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.fullFacetIndexEquiv hp = finCongr ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.liftTuple_facetTuple {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (j : Fin (p + 1)) : liftTuple hp N q (RelativeSubdivisionCylinderBoundary.facetTuple (p - 1) r ((fullFacetIndexEquiv hp) j)) = (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature ((q, r), j)

A local cylinder facet lifted through a refined top chart is exactly the corresponding global facet occurrence signature.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetOrbitIndicator_occurrence {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (o : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence) : facetOrbitIndicator hp N s ((RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature o) = if (RelativeSubdivisionOneStepCells.cellSystem hp N).facetClass o = s then 1 else 0

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.localTupleWeight {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (q : RefinedAffineMap.TopCell hp N) (v : Fin (p - 1 + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) × ↑(Set.Icc 0 1)) : ZMod p

Local tuple weight induced by one global quotient-facet class.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetIncidence_eq_localFullBoundary {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetIncidence s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * RelativeSubdivisionCylinderBoundary.fullBoundaryPairing (ZMod p) (p - 1) (localTupleWeight hp N s q)

The explicit global incidence is the sum of the local full-boundary pairings over refined Fox--Neuwirth top cells.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetIncidence_eq_localBase {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetIncidence s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * RelativeSubdivisionCylinderBoundary.basePairing (ZMod p) (p - 1) (localTupleWeight hp N s q)

After applying the local recursive-cylinder theorem, global incidence is the pairing with all cone-base facets.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.quotientIndicator {p N : ℕ} {hp : Nat.Prime p} (s t : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : ZMod p

Quotient-facet Kronecker delta.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.quotientIndicator s t = if t = s then 1 else 0

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.localBase_eq_globalBase {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * RelativeSubdivisionCylinderBoundary.basePairing (ZMod p) (p - 1) (localTupleWeight hp N s q) = RelativeSubdivisionOneStepBoundaryBase.basePairing hp N (quotientIndicator s)

The local cone-base sum is exactly the previously defined global cone-base pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.facetIncidence_eq_basePairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetIncidence s = RelativeSubdivisionOneStepBoundaryBase.basePairing hp N (quotientIndicator s)

Pointwise incidence is the global cone-base pairing.

Cancellation of the recursive spatial-side chain

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideCylinderTuple {p : ℕ} (hp : Nat.Prime p) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 2)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2)) → Realization p) : Fin p → EquivariantPrismVertexParameters.CylinderPoint p

Geometric tuple obtained by attaching the time coordinates of one lower-dimensional local cylinder cell to an arbitrary spatial facet map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideMapWeight {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 2)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2)) → Realization p) : ZMod p

Quotient-facet weight induced on a spatial facet map by one recursive side-cylinder cell.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideMapWeight_smul {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 2)) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2)) → Realization p) : (sideMapWeight hp N s r fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2))) => g • tau x) = sideMapWeight hp N s r tau

The side-map weight is invariant under prime relabelling.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideDimension_eq {p : ℕ} (hp : Nat.Prime p) : p - 2 + 1 = p - 1

The recursive side simplex has the same dimension as the parent boundary.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideDomainCast {p : ℕ} (hp : Nat.Prime p) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2 + 1)) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))

Identify the side simplex dimension with the parent boundary dimension.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideDomainCast hp x = ⋯ ▸ x

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideRefinementCast {p : ℕ} (hp : Nat.Prime p) (rho : Equiv.Perm (Fin p)) : Equiv.Perm (Fin (p - 2 + 2))

Transport a parent refinement permutation to the side-cylinder index type.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideRefinementCast hp rho = (Equiv.cast ⋯).trans (Equiv.trans rho (Equiv.cast ⋯).symm)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.fixedSideCell_sum_eq_zero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 2)) : ∑ c : PrimeOrbitCycle.TopOrbit hp, (PrimeOrbitCycle.orbitCycle hp).coefficient c * ∑ rho : RefinementWord p N, RefinedAffineMap.subdivisionSign N rho * ∑ k : Fin p, SimplicialChain.faceSign (EquivariantPrismNonhorizontalCancellation.orbitFacetIndex hp k) * sideMapWeight hp N s r (EquivariantPrismNonhorizontalCancellation.iteratedFacetMap (p - 2) N (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 2 + 1))) => (ReferenceAffineOrbitCount.topRepr hp c).realizationContinuousMap (sideDomainCast hp x)) (fun (i : Fin N) => sideRefinementCast hp (rho i)) (EquivariantPrismNonhorizontalCancellation.orbitFacetIndex hp k)) = 0

For one fixed recursive side cell, the signed side contribution of the refined orbit cycle vanishes.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.sideBasePairing_eq_zero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : RelativeSubdivisionOneStepBoundaryBase.sideBasePairing hp N (quotientIndicator s) = 0

The complete recursive spatial-side part of the one-step cone-base chain vanishes.

Pointwise collar boundary

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.lowerBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : ZMod p

Lower boundary coefficient of one quotient facet.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.upperBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : ZMod p

Upper boundary coefficient of one quotient facet.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundary.incidence_eq_boundary {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetIncidence s = upperBoundaryCoefficient hp N s - lowerBoundaryCoefficient hp N s

Exact pointwise boundary formula for the one-step relative subdivision cylinder.