Composition with described internal endpoints

The fully refined middle prism has canonical lower and upper endpoint facets, exact endpoint chain pairings, and representative geometry. What is not available is a standalone theorem saying that every horizontal quotient facet is one of those canonical facets. That stronger exhaustiveness property is unnecessary for an internal collar region.

This module separates the data used for seam cancellation from the external-facet exhaustiveness needed by EndpointIdentifiedRelativeAffineCollar. Two endpoint-described collars compose, and the result can be packaged as endpoint-identified whenever the left input has exhaustive lower facets and the right input has exhaustive upper facets. Thus a refined middle prism can be placed between two genuine endpoint stacks without assuming an unproved middle-prism exhaustiveness lemma.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M L : ℕ) extends NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L : Type 1

Endpoint data sufficient for chain-level seam cancellation. Unlike EndpointIdentifiedRelativeAffineCollar, no exhaustiveness is requested for either horizontal quotient-facet family.

• cells : RelativeAffineCellSystem hp N₀ N₁ M L
• lowerBoundaryCoefficient : self.cells.Facet → ZMod p
• upperBoundaryCoefficient : self.cells.Facet → ZMod p
• lower_zero_of_not_lower (s : self.cells.Facet) : ¬self.cells.IsLowerFacet s → self.lowerBoundaryCoefficient s = 0
• upper_zero_of_not_upper (s : self.cells.Facet) : ¬self.cells.IsUpperFacet s → self.upperBoundaryCoefficient s = 0
• incidence_eq_boundary (s : self.cells.Facet) : self.cells.facetIncidence s = self.upperBoundaryCoefficient s - self.lowerBoundaryCoefficient s
• lowerFacet : RefinedAffineMap.TopCell hp N₀ → self.cells.Facet

  The lower endpoint top cell's described boundary facet.

• upperFacet : RefinedAffineMap.TopCell hp N₁ → self.cells.Facet

  The upper endpoint top cell's described boundary facet.

• lowerFacet_isLower (q : RefinedAffineMap.TopCell hp N₀) : self.cells.IsLowerFacet (self.lowerFacet q)
• upperFacet_isUpper (q : RefinedAffineMap.TopCell hp N₁) : self.cells.IsUpperFacet (self.upperFacet q)
• lowerBoundaryPairing_eq (W : self.cells.Facet → ZMod p) : ∑ s : self.cells.Facet, self.lowerBoundaryCoefficient s * W s = ∑ q : RefinedAffineMap.TopCell hp N₀, RefinedAffineMap.coefficient hp N₀ q * W (self.lowerFacet q)
• upperBoundaryPairing_eq (W : self.cells.Facet → ZMod p) : ∑ s : self.cells.Facet, self.upperBoundaryCoefficient s * W s = ∑ q : RefinedAffineMap.TopCell hp N₁, RefinedAffineMap.coefficient hp N₁ q * W (self.upperFacet q)
• lowerFacetOccurrenceVertex_eq (q : RefinedAffineMap.TopCell hp N₀) (o : self.cells.FacetOccurrence) : self.cells.facetClass o = self.lowerFacet q → ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), self.cells.facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N₀ q (Fin.cast ⋯ i))
• upperFacetOccurrenceVertex_eq (q : RefinedAffineMap.TopCell hp N₁) (o : self.cells.FacetOccurrence) : self.cells.facetClass o = self.upperFacet q → ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), self.cells.facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp N₁ q (Fin.cast ⋯ i))

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.EndpointDescribedRelativeAffineCollar.ofEndpointIdentified {p N₀ N₁ M₀ L₀ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M₀ L₀) : EndpointDescribedRelativeAffineCollar hp N₀ N₁ M₀ L₀

Forget only endpoint-facet exhaustiveness.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.internalFacet_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp Nmid) : ExplicitAffineRelativeCollarCompose.Combined.leftFacet C.cells D.cells (C.upperFacet q) = ExplicitAffineRelativeCollarCompose.Combined.rightFacet C.cells D.cells (D.lowerFacet q)

The two described copies of every common endpoint top cell determine the same combined quotient facet.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerBoundaryCoefficient {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) : ZMod p

External lower coefficient inherited from the left collar.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperBoundaryCoefficient {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) : ZMod p

External upper coefficient inherited from the right collar.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.internalPairings_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) : ∑ t : C.cells.Facet, C.upperBoundaryCoefficient t * ExplicitAffineRelativeCollarCompose.Combined.leftIndicator C.cells D.cells s t = ∑ t : D.cells.Facet, D.lowerBoundaryCoefficient t * ExplicitAffineRelativeCollarCompose.Combined.rightIndicator C.cells D.cells s t

The described common endpoint pairings cancel pointwise.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.incidence_eq_boundary {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).facetIncidence s = upperBoundaryCoefficient C D s - lowerBoundaryCoefficient C D s

Pointwise boundary formula for composition with described internal endpoints.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerFacet_isLower {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₀) : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsLowerFacet (ExplicitAffineRelativeCollarCompose.Combined.leftFacet C.cells D.cells (C.lowerFacet q))

Canonical external lower facets remain lower-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperFacet_isUpper {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₁) : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsUpperFacet (ExplicitAffineRelativeCollarCompose.Combined.rightFacet C.cells D.cells (D.upperFacet q))

Canonical external upper facets remain upper-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerBoundaryCoefficient_zero_of_not_lower {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) (hs : ¬(ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsLowerFacet s) : lowerBoundaryCoefficient C D s = 0

External lower coefficients vanish away from time zero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperBoundaryCoefficient_zero_of_not_upper {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) (hs : ¬(ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsUpperFacet s) : upperBoundaryCoefficient C D s = 0

External upper coefficients vanish away from time one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerBoundaryPairing_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (W : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet → ZMod p) : ∑ s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet, lowerBoundaryCoefficient C D s * W s = ∑ q : RefinedAffineMap.TopCell hp N₀, RefinedAffineMap.coefficient hp N₀ q * W (ExplicitAffineRelativeCollarCompose.Combined.leftFacet C.cells D.cells (C.lowerFacet q))

Lower endpoint chain pairing of the described composition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperBoundaryPairing_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (W : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet → ZMod p) : ∑ s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet, upperBoundaryCoefficient C D s * W s = ∑ q : RefinedAffineMap.TopCell hp N₁, RefinedAffineMap.coefficient hp N₁ q * W (ExplicitAffineRelativeCollarCompose.Combined.rightFacet C.cells D.cells (D.upperFacet q))

Upper endpoint chain pairing of the described composition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerFacetOccurrenceVertex_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₀) (o : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).FacetOccurrence) (ho : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).facetClass o = ExplicitAffineRelativeCollarCompose.Combined.leftFacet C.cells D.cells (C.lowerFacet q)) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N₀ q (Fin.cast ⋯ i))

Representatives of external lower facets retain the prescribed endpoint geometry.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperFacetOccurrenceVertex_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₁) (o : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).FacetOccurrence) (ho : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).facetClass o = ExplicitAffineRelativeCollarCompose.Combined.rightFacet C.cells D.cells (D.upperFacet q)) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp N₁ q (Fin.cast ⋯ i))

Representatives of external upper facets retain the prescribed endpoint geometry.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.describedCollar {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) : EndpointDescribedRelativeAffineCollar hp N₀ N₁ (max M₀ M₁) (L₀ + L₁ + 1)

Composition preserving all endpoint data used by a later seam.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.lowerFacet_exhaustive_of_left {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (hC : ∀ (s : C.cells.Facet), C.cells.IsLowerFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₀), C.lowerFacet q = s) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) (hs : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsLowerFacet s) : ∃ (q : RefinedAffineMap.TopCell hp N₀), ExplicitAffineRelativeCollarCompose.Combined.leftFacet C.cells D.cells (C.lowerFacet q) = s

Lower-facet exhaustiveness propagates from the left external region; no endpoint exhaustiveness is required of the right internal region.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.upperFacet_exhaustive_of_right {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (hD : ∀ (s : D.cells.Facet), D.cells.IsUpperFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₁), D.upperFacet q = s) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).Facet) (hs : (ExplicitAffineRelativeCollarCompose.combinedCells C.cells D.cells).IsUpperFacet s) : ∃ (q : RefinedAffineMap.TopCell hp N₁), ExplicitAffineRelativeCollarCompose.Combined.rightFacet C.cells D.cells (D.upperFacet q) = s

Upper-facet exhaustiveness propagates from the right external region.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarComposeDescribed.endpointIdentifiedCollar {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : EndpointDescribedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : EndpointDescribedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (hC : ∀ (s : C.cells.Facet), C.cells.IsLowerFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₀), C.lowerFacet q = s) (hD : ∀ (s : D.cells.Facet), D.cells.IsUpperFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₁), D.upperFacet q = s) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ (max M₀ M₁) (L₀ + L₁ + 1)

Package a described composition as a genuine endpoint-identified collar when only the two external endpoint families are exhaustive.

Equations

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