Finite affine zero counts on Fox--Neuwirth incidence cycles

This module implements the algebraic finite-zero-count layer. The correct modulo-prime invariant counts symmetry orbits of transverse zeros, rather than all zeros in the covering order complex. Accordingly the main object is a finite incidence cycle: a finite set of top cells, a finite set of facets, an incidence matrix, and a coefficient vector whose boundary vanishes.

The zero count is the pairing of the cycle coefficients with a local-index function. An admissible affine homotopy supplies a facet transgression whose incidence coboundary is the difference of the endpoint local indices. Finite Stokes algebra then proves invariance of the zero count. No general PL topology is used in this layer.

For the order complex itself, the file defines the explicit alternating incidence matrix and shows that an ordinary simplicial cycle produces a finite incidence cycle. The later orbit reduction can instantiate the same interface with orbit representatives and quotient incidences.

structure NRR.FiniteIncidenceCycle (R : Type u_2) [CommRing R] : Type (max (max u_2 (u_3 + 1)) (u_4 + 1))

A finite chain-level incidence cycle. This is the exact algebraic structure required by the zero-count argument, and it applies equally to an ordinary finite simplicial cycle or to its finite symmetry-orbit quotient.

• TopCell : Type u_3

  The finite type of top-dimensional cells in the incidence cycle.

• Facet : Type u_4

  The finite type of codimension-one facets in the incidence cycle.

• topCellFintype : Fintype self.TopCell
• topCellDecidableEq : DecidableEq self.TopCell
• facetFintype : Fintype self.Facet
• facetDecidableEq : DecidableEq self.Facet
• incidence : self.Facet → self.TopCell → R

  The signed incidence coefficient of a facet in a top cell.

• coefficient : self.TopCell → R

  The coefficient of each top cell in the cycle.

• boundary_zero (f : self.Facet) : ∑ c : self.TopCell, self.incidence f c * self.coefficient c = 0

def NRR.FiniteIncidenceCycle.coboundary {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (h : C.Facet → R) : C.TopCell → R

Incidence coboundary of a facet function.

Equations

• C.coboundary h c = ∑ f : C.Facet, C.incidence f c * h f

def NRR.FiniteIncidenceCycle.zeroCount {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (index : C.TopCell → R) : R

Pairing of the cycle coefficient vector with a local-index function.

Equations

• C.zeroCount index = ∑ c : C.TopCell, C.coefficient c * index c

@[simp]

theorem NRR.FiniteIncidenceCycle.zeroCount_zero {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) : C.zeroCount 0 = 0

@[simp]

theorem NRR.FiniteIncidenceCycle.zeroCount_add {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (a b : C.TopCell → R) : C.zeroCount (a + b) = C.zeroCount a + C.zeroCount b

@[simp]

theorem NRR.FiniteIncidenceCycle.zeroCount_sub {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (a b : C.TopCell → R) : C.zeroCount (a - b) = C.zeroCount a - C.zeroCount b

theorem NRR.FiniteIncidenceCycle.zeroCount_coboundary_eq_zero {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (h : C.Facet → R) : C.zeroCount (C.coboundary h) = 0

Finite Stokes theorem: the pairing of a cycle with an incidence coboundary vanishes.

structure NRR.FiniteIncidenceCycle.IndexHomotopy {R : Type u_1} [CommRing R] (C : FiniteIncidenceCycle R) (index₀ index₁ : C.TopCell → R) : Type (max u_1 u_3)

A chain-level admissible homotopy. The transgression is the finite signed zero set in the prism facets, and index_difference is the local finite Stokes relation.

• transgression : C.Facet → R

  The facet cochain whose coboundary relates the two index functions.

• index_difference : index₁ - index₀ = C.coboundary self.transgression

theorem NRR.FiniteIncidenceCycle.IndexHomotopy.zeroCount_eq {R : Type u_1} [CommRing R] {C : FiniteIncidenceCycle R} {index₀ index₁ : C.TopCell → R} (H : C.IndexHomotopy index₀ index₁) : C.zeroCount index₀ = C.zeroCount index₁

Zero-count invariance under an admissible finite homotopy.

theorem NRR.FiniteIncidenceCycle.IndexHomotopy.zeroCount_ne_zero {R : Type u_1} [CommRing R] {C : FiniteIncidenceCycle R} {index₀ index₁ : C.TopCell → R} (H : C.IndexHomotopy index₀ index₁) (h₀ : C.zeroCount index₀ ≠ 0) : C.zeroCount index₁ ≠ 0

Nonvanishing transports across an admissible finite homotopy.

noncomputable def NRR.FoxNeuwirthOrderComplex.SimplicialIncidence.incidence {R : Type u_1} [CommRing R] {p d : ℕ} (target : Simplex p d) (source : Simplex p (d + 1)) : R

Alternating incidence coefficient between a simplex and one of its codimension-one faces.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.SimplicialIncidence.boundary_apply_eq_incidence {R : Type u_1} [CommRing R] {p d : ℕ} (chain : SimplicialChain R p (d + 1)) (target : Simplex p d) : chain.boundary target = ∑ source : Simplex p (d + 1), incidence target source * chain source

The ordinary simplicial boundary coefficient is matrix multiplication by the alternating incidence matrix.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.SimplicialIncidence.ofCycle {R : Type u_1} [CommRing R] {p d : ℕ} (chain : SimplicialChain R p (d + 1)) (hcycle : chain.boundary = 0) : FiniteIncidenceCycle R

An ordinary simplicial cycle as a finite incidence cycle.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.AffineVertexMap (p d : ℕ) : Type

Vertex data for a map that is affine on every simplex of the order complex. The target is an explicit d-dimensional real coordinate space.

• vertexValue : BarredPermutation p → Fin d → ℝ

  The coordinate vector assigned to each barred-permutation vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.value {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) (w : StandardSimplex d) : Fin d → ℝ

Affine extension of vertex values over one order-complex simplex.

Equations

• f.value s w r = ∑ i : Fin (d + 1), ↑w i * f.vertexValue (↑s i) r

def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.augmentedMatrix {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ

Augmented affine matrix. Its columns are the target values of the simplex vertices and its last row consists of ones.

Equations

• f.augmentedMatrix s r i = Fin.lastCases 1 (fun (q : Fin d) => f.vertexValue (↑s i) q) r

noncomputable def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.determinant {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) : ℝ

Determinant controlling regularity and the local orientation of the affine map.

Equations

• f.determinant s = (f.augmentedMatrix s).det

def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.HasInteriorZero {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) : Prop

The affine restriction has a zero in the relative interior of the simplex.

Equations

• f.HasInteriorZero s = ∃ (w : NRR.StandardSimplex d), w.IsInterior ∧ ∀ (r : Fin d), f.value s w r = 0

def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.IsRegularOn {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) : Prop

The restriction is regular when its augmented affine matrix is nonsingular.

Equations

• f.IsRegularOn s = (f.determinant s ≠ 0)

def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.IsRegular {p d : ℕ} (f : AffineVertexMap p d) : Prop

Global finite regularity on all top-dimensional simplices.

Equations

• f.IsRegular = ∀ (s : NRR.FoxNeuwirthOrderComplex.Simplex p d), f.IsRegularOn s

noncomputable def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.determinantIndex {p : ℕ} (x : ℝ) : ZMod p

Sign of a real determinant, reduced to the coefficient field ZMod p.

Equations

• NRR.FoxNeuwirthOrderComplex.AffineVertexMap.determinantIndex x = if 0 < x then 1 else if x < 0 then -1 else 0

noncomputable def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.localZeroIndex {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) : ZMod p

Local signed zero index of one affine simplex.

Equations

• f.localZeroIndex s = if f.HasInteriorZero s then NRR.FoxNeuwirthOrderComplex.AffineVertexMap.determinantIndex (f.determinant s) else 0

noncomputable def NRR.FoxNeuwirthOrderComplex.AffineVertexMap.localIndexCochain {p d : ℕ} (f : AffineVertexMap p d) : Simplex p d → ZMod p

Local-index function used in the finite cycle pairing.

Equations

• f.localIndexCochain s = f.localZeroIndex s

noncomputable def NRR.FoxNeuwirthOrderComplex.simplicialAffineZeroCount {p d : ℕ} (chain : SimplicialChain (ZMod p) p d) (f : AffineVertexMap p d) : ZMod p

Concrete finite affine zero count on an ordinary simplicial chain. The orbit-count version uses the same FiniteIncidenceCycle.zeroCount operation after replacing top simplices by their prime-symmetry orbit cells.

Equations

• NRR.FoxNeuwirthOrderComplex.simplicialAffineZeroCount chain f = ∑ s : NRR.FoxNeuwirthOrderComplex.Simplex p d, chain s * f.localZeroIndex s

structure NRR.FiniteOrbitZeroCountModel {p : ℕ} (hp : Nat.Prime p) : Type 1

Proof-carrying finite orbit model for the finite zero count. The top and facet types are intended to be prime-symmetry orbits of transverse simplices and prism facets.

• cycle : FiniteIncidenceCycle (ZMod p)

  The finite incidence cycle on which zero indices are counted.

• topSimplex : self.cycle.TopCell → FoxNeuwirthOrderComplex.Simplex p (p - 1)

  The order-complex simplex representing each top cell of the cycle.

• referenceMap : FoxNeuwirthOrderComplex.AffineVertexMap p (p - 1)

  The regular reference affine map used to normalize the zero count.

• referenceRegular : self.referenceMap.IsRegular
• referenceIndex : self.cycle.TopCell → ZMod p

  The local zero index of the reference map on each top cell.

• referenceIndex_eq (c : self.cycle.TopCell) : self.referenceIndex c = self.referenceMap.localZeroIndex (self.topSimplex c)
• referenceCount_eq : self.cycle.zeroCount self.referenceIndex = FoxNeuwirth.referenceSignedOrbitCount p

theorem NRR.FiniteOrbitZeroCountModel.referenceCount_ne_zero {p : ℕ} {hp : Nat.Prime p} (M : FiniteOrbitZeroCountModel hp) : M.cycle.zeroCount M.referenceIndex ≠ 0

The reference orbit count of the finite affine model is nonzero modulo the prime.

structure NRR.FiniteOrbitZeroCountModel.EndpointData {p : ℕ} {hp : Nat.Prime p} (M : FiniteOrbitZeroCountModel hp) : Type

Endpoint data for an affine family: its local-index function is related to the reference function by a finite incidence transgression.

• map : FoxNeuwirthOrderComplex.AffineVertexMap p (p - 1)

  The regular affine map at the endpoint of the index comparison.

• regular : self.map.IsRegular
• homotopy : M.cycle.IndexHomotopy M.referenceIndex fun (c : M.cycle.TopCell) => self.map.localZeroIndex (M.topSimplex c)

  The finite incidence transgression connecting reference and endpoint indices.

noncomputable def NRR.FiniteOrbitZeroCountModel.EndpointData.index {p : ℕ} {hp : Nat.Prime p} {M : FiniteOrbitZeroCountModel hp} (D : M.EndpointData) : M.cycle.TopCell → ZMod p

Local-index function of an affine endpoint on the orbit representatives.

Equations

• D.index c = D.map.localZeroIndex (M.topSimplex c)

theorem NRR.FiniteOrbitZeroCountModel.EndpointData.zeroCount_ne_zero {p : ℕ} {hp : Nat.Prime p} {M : FiniteOrbitZeroCountModel hp} (D : M.EndpointData) : M.cycle.zeroCount D.index ≠ 0

Every regular affine endpoint connected to the reference index by an admissible finite homotopy has nonzero orbit zero count.

theorem NRR.FiniteIncidenceCycle.exists_index_ne_zero_of_zeroCount_ne_zero {R : Type u_1} [CommRing R] {C : FiniteIncidenceCycle R} {index : C.TopCell → R} (hcount : C.zeroCount index ≠ 0) : ∃ (c : C.TopCell), index c ≠ 0

A nonzero cycle pairing has at least one top cell with nonzero local index.

theorem NRR.FoxNeuwirthOrderComplex.AffineVertexMap.hasInteriorZero_of_localZeroIndex_ne_zero {p d : ℕ} (f : AffineVertexMap p d) (s : Simplex p d) (hindex : f.localZeroIndex s ≠ 0) : f.HasInteriorZero s

A nonzero local affine index certifies a relative-interior zero.

theorem NRR.FiniteOrbitZeroCountModel.EndpointData.exists_topCell_hasInteriorZero {p : ℕ} {hp : Nat.Prime p} {M : FiniteOrbitZeroCountModel hp} (D : M.EndpointData) : ∃ (c : M.cycle.TopCell), D.map.HasInteriorZero (M.topSimplex c)

A nonzero finite orbit count produces an orbit representative simplex containing a relative-interior zero of the affine endpoint map.