Nontriviality of the equivariant prism genericity polynomials

The finite perturbation theorem applies only after every determinant polynomial in the combined family is known to be nonzero. The essential point is that the scalar orbit parameters occurring at the vertices of one refined prism simplex are independent: two local scalar sites can represent the same diagonal prime orbit only when both the local vertex and the coordinate label agree.

Once this local independence is exposed, an arbitrary collection of vectors can be prescribed at the vertices of one fixed prism simplex. For a facet determinant we prescribe a triangular augmented-deviation matrix with diagonal one. For a codimension-two minor we prescribe the identity deviation matrix. Evaluation at the corresponding assignments proves that the two polynomial families, and hence the combined family, are nonzero.

Injectivity of the affine subdivision charts

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.affineSubdivMap_injective (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) : Function.Injective (SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n pi)

One barycentric-subdivision affine map is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.affineCompMap_injective (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) : Function.Injective ⇑(SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N rho)

Every iterated barycentric-subdivision affine composite is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.simplex_realizationPoint_injective {p d : ℕ} (s : Simplex p d) : Function.Injective s.realizationPoint

The affine realization chart of a strict order-complex simplex is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.refined_chart_injective {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) : Function.Injective ⇑(RefinedAffineMap.chart hp N q)

A refined spatial chart is injective.

The staircase map is an affine isomorphism onto the selected prism simplex. The following coordinate proof recovers every barycentric coefficient from the spatial aggregate and interval coordinate.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.spatialIndex {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : Fin (p - 1 + 1)

Transport a spatial label to the maximal-simplex indexing type.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.spatialIndex hp i = Fin.cast ⋯ i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.spatialWeight_eq_of_lt {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) (i : Fin p) (hi : ↑i < ↑k) : SubdivisionPrismCharts.spatialWeight hp k w (spatialIndex hp i) = ↑w i.castSucc

Spatial weights away from the doubled staircase vertex recover a unique domain coordinate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.spatialWeight_eq_of_gt {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) (i : Fin p) (hi : ↑k < ↑i) : SubdivisionPrismCharts.spatialWeight hp k w (spatialIndex hp i) = ↑w ⟨↑i + 1, ⋯⟩

Spatial weights above the doubled staircase vertex recover the successor domain coordinate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.spatialWeight_pivot {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) : SubdivisionPrismCharts.spatialWeight hp k w (spatialIndex hp k) = ↑w k.castSucc + ↑w k.succ

The doubled spatial coordinate is the sum of the two staircase coordinates.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.intervalWeight_eq_sum_gt {p : ℕ} (k : Fin p) (w : StandardSimplex p) : SubdivisionPrismCharts.intervalWeight k w = ∑ j : Fin (p + 1), if ↑k < ↑j then ↑w j else 0

The interval coordinate is the sum of all domain coordinates strictly above the staircase cut.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.intervalWeight_eq_pivot_add_spatial_tail {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) : SubdivisionPrismCharts.intervalWeight k w = ↑w k.succ + ∑ i : Fin p, if ↑k < ↑i then ↑(SubdivisionPrismCharts.spatialPoint hp k w) (spatialIndex hp i) else 0

The interval coordinate splits into the upper pivot coordinate and the spatial tail.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.staircasePoint_injective {p : ℕ} (hp : Nat.Prime p) (k : Fin p) : Function.Injective (SubdivisionPrismCharts.staircasePoint hp k)

The staircase chart is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.prism_chart_injective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) : Function.Injective ⇑(SubdivisionPrismCharts.chart hp N L q)

Every refined prism chart is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.prism_vertex_injective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) : Function.Injective (SubdivisionPrismCharts.vertex hp N L q)

The vertices of one refined prism simplex are pairwise distinct.

Separation under the prime action

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.realizationPoint_orbit_separated (p : ℕ) {d : ℕ} (s : Simplex p d) (w v : StandardSimplex d) (g : ↥(PrimeSymmetry p)) (h : g • s.realizationPoint w = s.realizationPoint v) : g = 1

A prime translate of a point in one strict simplex can lie in that same simplex only for the identity group element.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.prism_vertex_orbit_injective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (g : ↥(PrimeSymmetry p)) (i j : Fin (p + 1)) (h : g • EquivariantPrismVertexParameters.CylinderPoint.ofProd (SubdivisionPrismCharts.vertex hp N L q i) = EquivariantPrismVertexParameters.CylinderPoint.ofProd (SubdivisionPrismCharts.vertex hp N L q j)) : g = 1 ∧ i = j

No two different vertices of one refined prism simplex lie in the same prime orbit.

Local scalar-site independence and assignment realization

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localParameter {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) (j : Fin p) : EquivariantPrismVertexParameters.Parameter hp N L

Parameter represented by one scalar coordinate at one local prism vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localParameter hp N L q i j = ⟦(NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.sampleVertex hp N L (q, i), j)⟧

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localParameter_injective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) : Function.Injective fun (z : Fin (p + 1) × Fin p) => localParameter hp N L q z.1 z.2

Scalar sites at the vertices of one fixed refined prism simplex give distinct orbit parameters.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localRealizingAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (target : Fin (p + 1) → Fin p → ℝ) : EquivariantPrismVertexParameters.Assignment hp N L

Assignment obtained by prescribing arbitrary full coordinate vectors at the vertices of one fixed refined prism simplex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localRealizingAssignment_apply {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (target : Fin (p + 1) → Fin p → ℝ) (i : Fin (p + 1)) (j : Fin p) : localRealizingAssignment hp N L q target (localParameter hp N L q i j) = target i j

The local realizing assignment takes the prescribed scalar values.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.localVertexValue_localRealizingAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (target : Fin (p + 1) → Fin p → ℝ) (i : Fin (p + 1)) : EquivariantPrismVertexParameters.localVertexValue hp N L (localRealizingAssignment hp N L q target) q i = target i

The prescribed vectors are reconstructed at every vertex of the selected local simplex.

Explicit witnesses for the two determinant families

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.coordinateLabel_injective {p : ℕ} (hp : Nat.Prime p) : Function.Injective (ReferenceAffineOrbitCount.coordinateLabel hp)

The fixed difference-coordinate labels are injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.coordinateLabel_ne_last {p : ℕ} (hp : Nat.Prime p) (r : Fin (p - 1)) : ReferenceAffineOrbitCount.coordinateLabel hp r ≠ ReferenceAffineOrbitCount.lastLabel hp

No fixed difference-coordinate label is the omitted label.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.facetWitnessTarget {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : Fin (p + 1) → Fin p → ℝ

Target values making the selected facet matrix lower triangular with diagonal one.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.facetWitnessTarget_succAbove {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (c j : Fin p) : facetWitnessTarget hp k (k.succAbove c) j = Fin.lastCases 0 (fun (r : Fin (p - 1)) => if j = ReferenceAffineOrbitCount.coordinateLabel hp r then 1 else 0) ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) c)

Values of the facet witness on retained vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.facetMatrix_witness {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetMatrix hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L (localRealizingAssignment hp N L q (facetWitnessTarget hp k)) q) k = fun (r c : Fin p) => Fin.lastCases 1 (fun (s : Fin (p - 1)) => Fin.lastCases 0 (fun (t : Fin (p - 1)) => if s = t then 1 else 0) ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) c)) ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) r)

The real facet matrix produced by the witness assignment is triangular with diagonal one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.facetDeterminant_witness {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L (localRealizingAssignment hp N L q (facetWitnessTarget hp k)) q) k = 1

The explicit facet witness has determinant one.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.codimTwoWitnessTarget {p : ℕ} (hp : Nat.Prime p) (f : EquivariantPrismGenericityPolynomials.CodimTwoFace p) : Fin (p + 1) → Fin p → ℝ

Target values making a selected codimension-two deviation matrix the identity.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.codimTwoWitnessTarget_vertex {p : ℕ} (hp : Nat.Prime p) (f : EquivariantPrismGenericityPolynomials.CodimTwoFace p) (i : Fin (p - 1)) (j : Fin p) : codimTwoWitnessTarget hp f (EquivariantPrismGenericityPolynomials.codimTwoVertex hp f i) j = if j = ReferenceAffineOrbitCount.coordinateLabel hp i then 1 else 0

Values of the codimension-two witness on retained vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.codimTwoDeviationMatrix_witness {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : EquivariantPrismGenericityPolynomials.CodimTwoFace p) : EquivariantPrismGenericityPolynomials.codimTwoDeviationMatrix hp N L (localRealizingAssignment hp N L q (codimTwoWitnessTarget hp f)) q f = 1

The codimension-two witness evaluates to the identity deviation matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.facetDeterminantPolynomial_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : EquivariantPrismGenericityPolynomials.facetDeterminantPolynomial hp N L q k ≠ 0

Every facet determinant polynomial is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.codimTwoMinorPolynomial_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : EquivariantPrismGenericityPolynomials.CodimTwoFace p) : EquivariantPrismGenericityPolynomials.codimTwoMinorPolynomial hp N L q f ≠ 0

Every codimension-two minor polynomial is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityNonzero.genericityPolynomial_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (i : EquivariantPrismGenericityPolynomials.GenericityIndex hp N L) : EquivariantPrismGenericityPolynomials.genericityPolynomial hp N L i ≠ 0

Every polynomial in the combined finite prism-genericity family is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityPolynomial_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (i : GenericityIndex hp N L) : genericityPolynomial hp N L i ≠ 0

Public nontriviality theorem for the combined finite genericity family.