Horizontal endpoint identification for the refined equivariant prism

The global prism boundary has already been split into lower-horizontal, upper-horizontal, and nonhorizontal contributions, and the nonhorizontal term has been shown to vanish. This file reindexes each horizontal contribution as the positive-ray count on the corresponding endpoint triangulation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointRefinementWord {p : ℕ} (hp : Nat.Prime p) (L : ℕ) (eta : RefinementWord p L) : Fin L → Equiv.Perm (Fin (p - 1 + 1))

Interpret a spatial refinement word on the definitionally different simplex-index type.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointRefinementWord hp L eta = ⋯.mpr eta

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

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointTopMap {p : ℕ} (hp : Nat.Prime p) {X : Type} (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p) → X) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1 + 1)) → X

Transport an endpoint top simplex to the cardinality expected by the boundary theorem.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointTopMap hp sigma = ⋯.mpr sigma

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointIteratedFacetMap {p : ℕ} (hp : Nat.Prime p) {X : Type} (L : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p) → X) (rho : Fin L → Equiv.Perm (Fin (p + 1))) (k : Fin (p + 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → X

Transported endpoint facet map with the natural Fin (p+1) indexing.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointIteratedBoundaryMap {p : ℕ} (hp : Nat.Prime p) {X : Type} (L : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p) → X) (j : Fin (p + 1)) (eta : RefinementWord p L) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → X

Transported endpoint boundary map with the natural endpoint indexing.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointFaceSign {p : ℕ} (hp : Nat.Prime p) (j : Fin (p + 1)) : ZMod p

Endpoint face sign with the natural Fin (p+1) indexing.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpoint_iterated_weighted_boundary {p : ℕ} {X : Type} (hp : Nat.Prime p) (L : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p) → X) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → X) → ZMod p) : ∑ rho : Fin L → Equiv.Perm (Fin (p + 1)), EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod p) L rho * ∑ k : Fin (p + 1), endpointFaceSign hp k * W (endpointIteratedFacetMap hp L sigma rho k) = ∑ j : Fin (p + 1), endpointFaceSign hp j * ∑ eta : RefinementWord p L, RefinedAffineMap.subdivisionSign L eta * W (endpointIteratedBoundaryMap hp L sigma j eta)

Endpoint-index form of the iterated weighted-boundary theorem. This packages the single Fin p versus Fin (p - 1 + 1) transport used by every horizontal endpoint calculation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p

The spatial simplex obtained by applying the final L barycentric refinements to an already level-N refined top cell.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap_succ {p : ℕ} (hp : Nat.Prime (p + 1)) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord (p + 1) L) : endpointSpatialMap hp N L q eta = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) => (RefinedAffineMap.chart hp N q) ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L eta) x)

In successor dimension the transported endpoint spatial map is the original refinement word applied in the original chart.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Positive-ray count represented by the lower horizontal boundary of a compatible prism assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.upperEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Positive-ray count represented by the upper horizontal boundary of a compatible prism assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerHorizontalMapWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Weight which retains only lower-horizontal realized facets.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.upperHorizontalMapWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Weight which retains only upper-horizontal realized facets.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerHorizontalContribution_eq_occurrence_sum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.lowerHorizontalContribution hp N L a = ∑ o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L, EquivariantPrismGlobalCancellation.occurrenceCoefficient hp N L o * lowerHorizontalMapWeight hp N L a (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L o)

Occurrence expansion of the lower-horizontal signature contribution.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.upperHorizontalContribution_eq_occurrence_sum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.upperHorizontalContribution hp N L a = ∑ o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L, EquivariantPrismGlobalCancellation.occurrenceCoefficient hp N L o * upperHorizontalMapWeight hp N L a (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L o)

Occurrence expansion of the upper-horizontal signature contribution.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerEndpointMap_horizontal {p : ℕ} (hp : Nat.Prime p) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : EquivariantPrismNonhorizontalCancellation.MapIsLowerHorizontal (EquivariantPrismNonhorizontalCancellation.lowerEndpointMap sigma) ∧ ¬EquivariantPrismNonhorizontalCancellation.MapIsUpperHorizontal (EquivariantPrismNonhorizontalCancellation.lowerEndpointMap sigma)

Lower endpoint maps are lower-horizontal and not upper-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.upperEndpointMap_horizontal {p : ℕ} (hp : Nat.Prime p) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : EquivariantPrismNonhorizontalCancellation.MapIsUpperHorizontal (EquivariantPrismNonhorizontalCancellation.upperEndpointMap sigma) ∧ ¬EquivariantPrismNonhorizontalCancellation.MapIsLowerHorizontal (EquivariantPrismNonhorizontalCancellation.upperEndpointMap sigma)

Upper endpoint maps are upper-horizontal and not lower-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.affineSubdivMap_pos_of_forall_pos (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) (hx : ∀ (i : Fin (n + 1)), 0 < x i) (j : Fin (n + 1)) : 0 < (SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n pi x) j

An affine barycentric-subdivision chart sends a strictly positive simplex point to a strictly positive simplex point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.affineCompMap_pos_of_forall_pos (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) (hx : ∀ (i : Fin (n + 1)), 0 < x i) (j : Fin (n + 1)) : 0 < ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N rho) x) j

Iterated affine barycentric-subdivision charts preserve strict positivity.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.affineCompMap_succ_last_vertex_pos (n N : ℕ) (rho : Fin (N + 1) → Equiv.Perm (Fin (n + 1))) (j : Fin (n + 1)) : 0 < ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n (N + 1) rho) (SphereOddDegree.FiniteSimplex.vertex (Fin.last n))) j

After at least one refinement, the last domain vertex maps to a strictly positive point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.genericStaircaseIntervalPoint_pos_lt_one (n : ℕ) (k : Fin (n + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) (hw : ∀ (i : Fin (n + 1 + 1)), 0 < w i) : 0 < ↑(EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint n k w) ∧ ↑(EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint n k w) < 1

A strictly positive barycentric point has strictly interior staircase time.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.deltaCast_pos_of_forall_pos {m n : ℕ} (e : m = n) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta m)) (hx : ∀ (i : Fin (m + 1)), 0 < x i) (j : Fin (n + 1)) : 0 < (EquivariantPrismNonhorizontalCancellation.deltaCast e x) j

Transporting a strictly positive simplex point preserves strict positivity.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.refinedSidePrismMap_not_lowerHorizontal {p : ℕ} (hp : Nat.Prime (p + 1)) (N : ℕ) (orbit : RefinedAffineMap.TopCell hp N) (r : Fin (p + 1)) (h : Fin p) (L : ℕ) (eta : Fin L → Equiv.Perm (Fin (p + 1))) : ¬EquivariantPrismNonhorizontalCancellation.MapIsLowerHorizontal fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p + 1 - 1))) => EquivariantPrismNonhorizontalCancellation.sidePrismMap p (⇑(RefinedAffineMap.chart hp N orbit)) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L eta) x)

A refined staircase side map is never lower-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.refinedSidePrismMap_not_upperHorizontal {p : ℕ} (hp : Nat.Prime (p + 1)) (N : ℕ) (orbit : RefinedAffineMap.TopCell hp N) (r : Fin (p + 1)) (h : Fin p) (L : ℕ) (eta : Fin L → Equiv.Perm (Fin (p + 1))) : ¬EquivariantPrismNonhorizontalCancellation.MapIsUpperHorizontal fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p + 1 - 1))) => EquivariantPrismNonhorizontalCancellation.sidePrismMap p (⇑(RefinedAffineMap.chart hp N orbit)) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L eta) x)

A refined staircase side map is never upper-horizontal.

Endpoint pairing for an arbitrary affine-facet weight

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedLowerMapWeight {p : ℕ} (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Restrict an arbitrary facet-map weight to the lower horizontal faces.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedUpperMapWeight {p : ℕ} (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Restrict an arbitrary facet-map weight to the upper horizontal faces.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedOccurrencePairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

The occurrence sum of an arbitrary facet-map weight.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedLowerEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

The lower endpoint pairing of an arbitrary facet-map weight.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedUpperEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

The upper endpoint pairing of an arbitrary facet-map weight.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedOccurrencePairing_lower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : weightedOccurrencePairing hp N L (weightedLowerMapWeight W) = -weightedLowerEndpointPairing hp N L W

The lower occurrence sum of any weight is its negative lower endpoint pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.weightedOccurrencePairing_upper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : weightedOccurrencePairing hp N L (weightedUpperMapWeight W) = weightedUpperEndpointPairing hp N L W

The upper occurrence sum of any weight is its upper endpoint pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerHorizontalContribution_eq_neg_lowerEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.lowerHorizontalContribution hp N L a = -lowerEndpointRefinedCount hp N L a

The lower horizontal contribution is the negative of the refined lower endpoint count.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.upperHorizontalContribution_eq_upperEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.upperHorizontalContribution hp N L a = upperEndpointRefinedCount hp N L a

The upper horizontal contribution is the refined upper endpoint count.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.lowerEndpointRefinedCount_eq_upperEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : lowerEndpointRefinedCount hp N L a = upperEndpointRefinedCount hp N L a

Horizontal balance identifies the two refined endpoint counts represented by any compatible assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismHorizontalEndpointIdentification.Result.lowerEndpointRefinedCount_eq_upperEndpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : lowerEndpointRefinedCount hp N L R.assignment = upperEndpointRefinedCount hp N L R.assignment

Endpoint-count equality specialized to the compatible generic perturbation.