Base-facet chain of the one-step subdivision cylinder

Every recursive cylinder cell is a cone. Its facet opposite the cone apex belongs to the triangulated boundary of Delta (p - 1) x I. This module separates the lower and upper endpoint parts of that base-facet chain from the recursive spatial-side part and proves that the endpoint part is exactly

sd^(N+1)(orbitCycle) - sd^N(orbitCycle).

The radial-facet cancellation and the recursive-side vanishing over the Fox--Neuwirth orbit cycle are proved in the boundary-cancellation module.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.baseOccurrence {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RelativeSubdivisionOneStepCells.Cell hp N) : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence

The base facet occurrence of a coned top cell.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.baseOccurrence hp N q = (q, 0)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.basePairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ZMod p

Pairing of all cone-base facets against an arbitrary quotient-facet weight.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.IsEndpointCell {p : ℕ} (hp : Nat.Prime p) (q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) : Prop

A local base cell belongs to one of the two external horizontal boundaries.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.isEndpointCellDecidable {p : ℕ} (hp : Nat.Prime p) (q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) : Decidable (IsEndpointCell hp q)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.endpointBasePairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ZMod p

Endpoint part of the cone-base pairing.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.sideBasePairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ZMod p

Recursive spatial-side part of the cone-base pairing.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.basePairing_eq_endpoint_add_side {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : basePairing hp N W = endpointBasePairing hp N W + sideBasePairing hp N W

The base pairing is the sum of its endpoint and recursive-side parts.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.lowerEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ZMod p

The lower endpoint contribution of the cone-base chain.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.upperEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ZMod p

The upper endpoint contribution of the cone-base chain.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.endpoint_local_sum {p : ℕ} (hp : Nat.Prime p) (f : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1) → ZMod p) : (∑ q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1), if IsEndpointCell hp q then f q else 0) = f (RelativeSubdivisionCylinderCombinatorics.lowerCell (p - 1)) + ∑ pi : Equiv.Perm (Fin p), f (RelativeSubdivisionCylinderCombinatorics.upperCell (p - 1) (⋯.mpr pi))

Endpoint cells in the local recursive cylinder are precisely the one lower cell and all upper barycentric cells.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.endpointBasePairing_eq_upper_sub_lower {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : endpointBasePairing hp N W = upperEndpointPairing hp N W - lowerEndpointPairing hp N W

The endpoint part of the base chain is the refined upper chain minus the coarse lower chain.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepBoundaryBase.basePairing_eq_upper_sub_lower_add_side {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : basePairing hp N W = upperEndpointPairing hp N W - lowerEndpointPairing hp N W + sideBasePairing hp N W

Exact decomposition of all cone-base facets into the two external endpoint chains and the recursive spatial-side chain.