Canonical horizontal facets of the common-level middle prism

This module constructs the lower and upper horizontal quotient facets attached to every top cell at combined refinement level N + L. It also records the exact factorization of subdivision signs under the split refinement word. These are the endpoint maps needed by the chain-level collar interface; no choice of a unique quotient-facet representative is made.

@[instance_reducible]

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.facetFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (RelativeCollarMiddlePrism.cellSystem hp N L).Facet

Enumerate the facets of the refined middle-prism cell system.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.splitTopCellEquiv {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : RefinedAffineMap.TopCell hp (N + L) ≃ RefinedAffineMap.TopCell hp N × RefinementWord p L

Split a combined-level top cell into its level-N prefix and length-L refinement tail.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.subdivisionSign_appendRefinementWord {p : ℕ} (N L : ℕ) (rho : RefinementWord p N) (eta : RefinementWord p L) : RefinedAffineMap.subdivisionSign (N + L) (EndpointFaceRefinement.appendRefinementWord N L rho eta) = RefinedAffineMap.subdivisionSign N rho * RefinedAffineMap.subdivisionSign L eta

The subdivision sign of a concatenated word factors into the two subdivision signs.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.iteratedSign_eq_subdivisionSign {p : ℕ} (hp : Nat.Prime p) (L : ℕ) (eta : RefinementWord p L) : EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod p) L (EquivariantPrismHorizontalEndpointIdentification.endpointRefinementWord hp L eta) = RefinedAffineMap.subdivisionSign L eta

The transported generic iterated-subdivision sign is the Fox--Neuwirth subdivision sign.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.coefficient_endpointTopCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : RefinedAffineMap.coefficient hp (N + L) (EndpointFaceRefinement.endpointTopCell hp N L q eta) = RefinedAffineMap.coefficient hp N q * RefinedAffineMap.subdivisionSign L eta

Coefficients factor under the prefix-tail endpoint decomposition.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerFacet {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet

Canonical lower quotient facet of a combined-level top cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperFacet {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet

Canonical upper quotient facet of a combined-level top cell.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerFacet_isLower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) : (RelativeCollarMiddlePrism.cellSystem hp N L).IsLowerFacet (lowerFacet hp N L q)

Every canonical lower endpoint facet belongs to the lower horizontal boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperFacet_isUpper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) : (RelativeCollarMiddlePrism.cellSystem hp N L).IsUpperFacet (upperFacet hp N L q)

Every canonical upper endpoint facet belongs to the upper horizontal boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.facetOrbitIndicator_lowerEndpointMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : RelativeCollarMiddlePrismBoundary.facetOrbitIndicator hp N L s (EquivariantPrismNonhorizontalCancellation.lowerEndpointMap (EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta)) = if lowerFacet hp N L (EndpointFaceRefinement.endpointTopCell hp N L q eta) = s then 1 else 0

Canonical lower endpoint map evaluated on its actual occurrence is the Kronecker weight of the corresponding quotient facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.facetOrbitIndicator_upperEndpointMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : RelativeCollarMiddlePrismBoundary.facetOrbitIndicator hp N L s (EquivariantPrismNonhorizontalCancellation.upperEndpointMap (EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta)) = if upperFacet hp N L (EndpointFaceRefinement.endpointTopCell hp N L q eta) = s then 1 else 0

Upper endpoint analogue of facetOrbitIndicator_lowerEndpointMap.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerBoundaryPairing_eq_split {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet → ZMod p) : ∑ s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet, RelativeCollarMiddlePrismBoundary.lowerBoundaryCoefficient hp N L s * W s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * ∑ eta : RefinementWord p L, RefinedAffineMap.subdivisionSign L eta * W (lowerFacet hp N L (EndpointFaceRefinement.endpointTopCell hp N L q eta))

Pairing the lower boundary coefficients against an arbitrary quotient-facet weight gives the split refined Fox--Neuwirth endpoint chain.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperBoundaryPairing_eq_split {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet → ZMod p) : ∑ s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet, RelativeCollarMiddlePrismBoundary.upperBoundaryCoefficient hp N L s * W s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * ∑ eta : RefinementWord p L, RefinedAffineMap.subdivisionSign L eta * W (upperFacet hp N L (EndpointFaceRefinement.endpointTopCell hp N L q eta))

Pairing the upper boundary coefficients against an arbitrary quotient-facet weight gives the split refined Fox--Neuwirth endpoint chain.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet → ZMod p) : ∑ s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet, RelativeCollarMiddlePrismBoundary.lowerBoundaryCoefficient hp N L s * W s = ∑ q : RefinedAffineMap.TopCell hp (N + L), RefinedAffineMap.coefficient hp (N + L) q * W (lowerFacet hp N L q)

Chain-level lower endpoint identification at the combined subdivision level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet → ZMod p) : ∑ s : (RelativeCollarMiddlePrism.cellSystem hp N L).Facet, RelativeCollarMiddlePrismBoundary.upperBoundaryCoefficient hp N L s * W s = ∑ q : RefinedAffineMap.TopCell hp (N + L), RefinedAffineMap.coefficient hp (N + L) q * W (upperFacet hp N L q)

Chain-level upper endpoint identification at the combined subdivision level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) (o : (RelativeCollarMiddlePrism.cellSystem hp N L).FacetOccurrence) (ho : (RelativeCollarMiddlePrism.cellSystem hp N L).facetClass o = lowerFacet hp N L q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeCollarMiddlePrism.cellSystem hp N L).facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp (N + L) q (Fin.cast ⋯ i))

Every representative of a canonical lower quotient facet has the prescribed endpoint vertices, up to one simultaneous prime relabelling.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) (o : (RelativeCollarMiddlePrism.cellSystem hp N L).FacetOccurrence) (ho : (RelativeCollarMiddlePrism.cellSystem hp N L).facetClass o = upperFacet hp N L q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeCollarMiddlePrism.cellSystem hp N L).facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + L) q (Fin.cast ⋯ i))

Every representative of a canonical upper quotient facet has the prescribed endpoint vertices, up to one simultaneous prime relabelling.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.emptyEndpointRefinementWord (p : ℕ) : RefinementWord p 0

The unique empty endpoint refinement word.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.emptyEndpointRefinementWord p i = i.elim0

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.lowerOccurrence_classification_zero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (o : (RelativeCollarMiddlePrism.cellSystem hp N 0).FacetOccurrence) (ho : (RelativeCollarMiddlePrism.cellSystem hp N 0).IsLowerFacetOccurrence o) : ∃ (q : RefinedAffineMap.TopCell hp N), (RelativeCollarMiddlePrism.cellSystem hp N 0).facetClass o = (RelativeCollarMiddlePrism.cellSystem hp N 0).facetClass (RelativeCollarMiddlePrismEndpointsCore.lowerOccurrence hp N 0 q (emptyEndpointRefinementWord p))

At prism refinement level zero, every lower horizontal occurrence is the canonical lower occurrence of its spatial top cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.upperOccurrence_classification_zero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (o : (RelativeCollarMiddlePrism.cellSystem hp N 0).FacetOccurrence) (ho : (RelativeCollarMiddlePrism.cellSystem hp N 0).IsUpperFacetOccurrence o) : ∃ (q : RefinedAffineMap.TopCell hp N), (RelativeCollarMiddlePrism.cellSystem hp N 0).facetClass o = (RelativeCollarMiddlePrism.cellSystem hp N 0).facetClass (RelativeCollarMiddlePrismEndpointsCore.upperOccurrence hp N 0 q (emptyEndpointRefinementWord p))

At prism refinement level zero, every upper horizontal occurrence is the canonical upper occurrence of its spatial top cell.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.HorizontalFacetExhaustive {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Prop

The one remaining combinatorial condition needed to package the common-level middle prism as an endpoint-identified collar: every geometric horizontal facet must occur in the corresponding refined endpoint chain.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.horizontalFacetExhaustive_zero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : HorizontalFacetExhaustive hp N 0

Horizontal-facet exhaustiveness is completely explicit before any additional prism barycentric subdivision.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.endpointIdentifiedCollar {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (hexhaustive : HorizontalFacetExhaustive hp N L) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp (N + L) (N + L) (N + L) L

Horizontal-facet exhaustiveness makes the common-level middle prism a genuine endpoint-identified relative affine collar. All incidence, chain-pairing, and endpoint-geometry fields are already proved above.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpoints.endpointIdentifiedCollarZero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N N N 0

The unrefined common-level staircase prism is therefore already a complete endpoint-identified collar.

Equations

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