The explicit reference affine orbit count

This is Step S5 of the simplest AAK route. On a non-top Fox--Neuwirth vertex we use the first-coordinate reference vector: the block-index vector modulo the diagonal. At a top-cell vertex this vector is zero, so we perturb it in a rank-dependent direction. The adjacent gaps of the perturbation direction are 1, 2, ..., p - 1.

For a maximal flag, positive barycentric coefficients force the bottom rank to agree with the final top rank. Comparing adjacent labels then forces the bars to be removed in the identity order. Thus one maximal flag is selected for every top Fox--Neuwirth cell. The selected flags form one prime-symmetry orbit for p = 2 and two equally oriented orbits for odd primes.

At perturbation parameter zero the augmented affine determinant is the oriented maximal-flag coefficient, up to the constant sign (-1)^(p-1). Since there are finitely many maximal flags, a single sufficiently small positive perturbation preserves all determinant signs. This gives a regular affine reference map whose orbit zero count is the previously computed nonzero value FoxNeuwirth.referenceSignedOrbitCount p.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.stageIndex_val {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 1 + 1)) : ↑(MaximalFlagCode.stageIndex hp i) = ↑i

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lastLabel {p : ℕ} (hp : Nat.Prime p) : Fin p

The fixed label omitted from the difference-coordinate model of the diagonal quotient.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lastLabel hp = ⟨p - 1, ⋯⟩

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.coordinateLabel {p : ℕ} (hp : Nat.Prime p) (r : Fin (p - 1)) : Fin p

Embed a target coordinate into the label set.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.coordinateLabel hp r = ⟨↑r, ⋯⟩

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular (n : ℕ) : ℕ

Triangular numbers. Their consecutive gaps are 1,2,....

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular n = n * (n + 1) / 2

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular_two_mul (n : ℕ) : 2 * triangular n = n * (n + 1)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular_succ_sub (n : ℕ) : ↑(triangular (n + 1)) - ↑(triangular n) = ↑n + 1

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular_strictMono : StrictMono triangular

Triangular numbers are strictly increasing.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.triangular_injective : Function.Injective triangular

Triangular numbers are injective.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.sum_if_one_zero_eq_card {X : Type u_1} {R : Type u_2} [Fintype X] [Semiring R] (P : X → Prop) [DecidablePred P] : (∑ x : X, if P x then 1 else 0) = ↑(Fintype.card { x : X // P x })

Sum of an indicator over a finite type is the cardinality of its support, cast to the ring.

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.blockDifference {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (r : Fin (p - 1)) : ℤ

Block-index vector modulo the diagonal, in the fixed difference coordinates.

Equations

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

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.topDirection {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (r : Fin (p - 1)) : ℤ

Generic direction at a top-cell vertex. In the final rank order its adjacent gaps are 1,2,...,p-1.

Equations

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

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.liftedVertexValue (p : ℕ) (epsilon : ℝ) (c : BarredPermutation p) (x : Fin p) : ℝ

Unquotiented scalar attached to one label. The actual target coordinates are its differences from lastLabel. Introducing this lift is essential when comparing two arbitrary labels: neither label has to be one of the fixed target-coordinate labels.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.mapAt {p : ℕ} (hp : Nat.Prime p) (epsilon : ℝ) : AffineVertexMap p (p - 1)

Piecewise-affine reference map with perturbation parameter epsilon.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.mapAt_vertexValue_eq_lifted_sub {p : ℕ} (hp : Nat.Prime p) (epsilon : ℝ) (c : BarredPermutation p) (r : Fin (p - 1)) : (mapAt hp epsilon).vertexValue c r = liftedVertexValue p epsilon c (coordinateLabel hp r) - liftedVertexValue p epsilon c (lastLabel hp)

Every target coordinate is the difference of the lifted values at its label and at the omitted label.

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedCode {p : ℕ} (sigma : Equiv.Perm (Fin p)) : MaximalFlagCode.Code p

The selected maximal flag over a top permutation: bottom and top ranks agree, and bars are removed in their natural order.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedCode sigma = { bottom := sigma, removal := 1, top := sigma }

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedSimplex {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : Simplex p (p - 1)

Selected maximal simplex over a top permutation.

Equations

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

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.IsSelected {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Prop

A maximal simplex is one of the selected reference simplices.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.IsSelected hp s = ∃ (sigma : Equiv.Perm (Fin p)), s = NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedSimplex hp sigma

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.isSelectedDecidable {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Decidable (IsSelected hp s)

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.isSelectedDecidable hp s = Classical.dec (NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.IsSelected hp s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedCode_bottom {p : ℕ} (sigma : Equiv.Perm (Fin p)) : (selectedCode sigma).bottom = sigma

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedCode_removal {p : ℕ} (sigma : Equiv.Perm (Fin p)) : (selectedCode sigma).removal = 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedCode_top {p : ℕ} (sigma : Equiv.Perm (Fin p)) : (selectedCode sigma).top = sigma

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.permSignInt_eq_one_or_neg_one {n : ℕ} (sigma : Equiv.Perm (Fin n)) : MaximalFlagCode.permSignInt sigma = 1 ∨ MaximalFlagCode.permSignInt sigma = -1

The integer sign of a permutation is always 1 or -1.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.toSimplex_isTop_iff_last {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (i : Fin (p - 1 + 1)) : (↑(MaximalFlagCode.toSimplex hp z) i).IsTop ↔ ↑i = p - 1

A coded maximal-flag stage is top-dimensional exactly at the final index.

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lowerCumulativeMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

Lower-unit cumulative matrix.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lowerCumulativeMatrix n = Matrix.of fun (i j : Fin n) => if ↑j ≤ ↑i then 1 else 0

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.det_lowerCumulativeMatrix (n : ℕ) : (lowerCumulativeMatrix n).det = 1

The lower cumulative matrix is triangular with diagonal one.

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.cumulativePermutationMatrix {n : ℕ} (rho : Equiv.Perm (Fin n)) : Matrix (Fin n) (Fin n) ℤ

Cumulative rows ordered by a permutation.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.cumulativePermutationMatrix rho = Matrix.of fun (k j : Fin n) => if ↑j ≤ ↑((Equiv.symm rho) k) then 1 else 0

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.det_cumulativePermutationMatrix {n : ℕ} (rho : Equiv.Perm (Fin n)) : (cumulativePermutationMatrix rho).det = MaximalFlagCode.permSignInt rho

The cumulative-permutation determinant is the permutation sign.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.coordinateLabel_range {p : ℕ} (hp : Nat.Prime p) : Set.range (coordinateLabel hp) = {x : Fin p | x ≠ lastLabel hp}

The fixed label-coordinate family enumerates every label except lastLabel.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.weighted_lifted_difference_eq_zero {p : ℕ} (hp : Nat.Prime p) (epsilon : ℝ) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (hzero : ∀ (r : Fin (p - 1)), (mapAt hp epsilon).value s w r = 0) (x y : Fin p) : ∑ i : Fin (p - 1 + 1), ↑w i * (liftedVertexValue p epsilon (↑s i) x - liftedVertexValue p epsilon (↑s i) y) = 0

Vanishing of all fixed difference coordinates implies vanishing of the weighted lifted difference for any two labels. This is the correct coordinate-free replacement for subtracting two target equations, and it also handles the omitted label.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.stageBlock_adjacent_sub {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (j : Fin p) (r : Fin (p - 1)) : ↑(MaximalFlagCode.stageBlock z j ((Equiv.symm z.bottom) (MaximalFlagCode.stageIndex hp r.succ))) - ↑(MaximalFlagCode.stageBlock z j ((Equiv.symm z.bottom) (MaximalFlagCode.stageIndex hp r.castSucc))) = if ↑j ≤ ↑((Equiv.symm z.removal) r) then 1 else 0

Adjacent bottom ranks differ by one block exactly while their separating bar is retained.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.sum_fin_le_indicator {n : ℕ} (r : Fin n) : (∑ j : Fin n, if j ≤ r then 1 else 0) = ↑(↑r + 1)

The number of indices in a finite ordinal not exceeding r.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selected_stageBlock_sum_rank {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) (x : Fin p) : ∑ j : Fin (p - 1), ↑(MaximalFlagCode.stageBlock (selectedCode sigma) (MaximalFlagCode.stageIndex hp j.castSucc) x) = ↑(triangular ↑(sigma x))

For a selected flag, the sum of the earlier-stage block numbers of a label is the triangular number of its rank. This is the discrete antiderivative of the adjacent retained-bar indicator.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.sum_blockDifference_selected {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) (r : Fin (p - 1)) : ∑ j : Fin (p - 1), blockDifference hp (↑(selectedSimplex hp sigma) j.castSucc) r = topDirection hp (↑(selectedSimplex hp sigma) (Fin.last (p - 1))) r

Summing the non-top vertices of a selected flag gives precisely its triangular top direction.

def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.cutBasisMatrix {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : Matrix (Fin (p - 1)) (Fin (p - 1)) ℤ

Type-A cut-basis matrix in the fixed diagonal-quotient coordinates.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.det_cutBasisMatrix {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : (cutBasisMatrix hp sigma).det = (-1) ^ (p - 1) * MaximalFlagCode.permSignInt sigma

Determinant of the standard type-A cut basis.

The proof augments the difference matrix by the constant column. Reindexing rows by sigma turns the augmented matrix into the lower cumulative matrix. Expansion along the omitted-label row gives the stated cofactor sign.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedSimplex_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (sigma : Equiv.Perm (Fin p)) : g • selectedSimplex hp sigma = selectedSimplex hp ((Equiv.symm ((PrimeSymmetry.toPerm p) g)).trans sigma)

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.isSelected_toSimplex_iff {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : IsSelected hp (MaximalFlagCode.toSimplex hp z) ↔ z.bottom = z.top ∧ z.removal = 1

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.mapAt_zero_value_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (i : Fin (p - 1 + 1)) (r : Fin (p - 1)) : (mapAt hp 0).vertexValue (↑(MaximalFlagCode.toSimplex hp z) i) r = if ↑i = p - 1 then 0 else ↑(blockDifference hp (↑(MaximalFlagCode.toSimplex hp z) i) r)

At parameter zero, the top vertex is zero and all earlier vertices are block-difference vectors.

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.blockVertexMatrix {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : Matrix (Fin (p - 1)) (Fin (p - 1)) ℤ

Matrix of the non-top block-difference vertices of a coded maximal flag.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.det_blockVertexMatrix {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : (blockVertexMatrix hp z).det = (-1) ^ (p - 1) * MaximalFlagCode.coefficient z

The block-vertex determinant is the code orientation, with the fixed difference-coordinate orientation factor. This is the integral braid-fan basis calculation.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.determinant_zero_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : (mapAt hp 0).determinant (MaximalFlagCode.toSimplex hp z) = ↑(blockVertexMatrix hp z).det

At parameter zero, expansion along the final vertex column identifies the affine augmented determinant with the real cast of the integral block-vertex determinant.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.determinant_zero_ne_zero {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (mapAt hp 0).determinant s ≠ 0

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.continuous_determinant_mapAt {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Continuous fun (epsilon : ℝ) => (mapAt hp epsilon).determinant s

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.exists_common_positive_sign_neighborhood {ι : Type u_1} [Finite ι] (f : ι → ℝ → ℝ) (hf : ∀ (i : ι), Continuous (f i)) (h0 : ∀ (i : ι), f i 0 ≠ 0) : ∃ (epsilon : ℝ), 0 < epsilon ∧ ∀ (i : ι), (0 < f i epsilon ↔ 0 < f i 0) ∧ (f i epsilon < 0 ↔ f i 0 < 0)

A finite family of continuous nonzero values at zero has a common positive neighborhood on which every sign is unchanged.

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.epsilon {p : ℕ} (hp : Nat.Prime p) : ℝ

A common positive perturbation scale preserving the signs of all reference determinants.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.epsilon hp = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.epsilon_pos {p : ℕ} (hp : Nat.Prime p) : 0 < epsilon hp

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.determinant_sign_preserved {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (0 < (mapAt hp (epsilon hp)).determinant s ↔ 0 < (mapAt hp 0).determinant s) ∧ ((mapAt hp (epsilon hp)).determinant s < 0 ↔ (mapAt hp 0).determinant s < 0)

Determinant signs are preserved by the chosen perturbation.

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceMap {p : ℕ} (hp : Nat.Prime p) : AffineVertexMap p (p - 1)

The chosen affine reference map is regular on every maximal simplex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceMap_regular {p : ℕ} (hp : Nat.Prime p) : (referenceMap hp).IsRegular

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.eq_zero_of_mulVec_eq_zero_of_det_ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hdet : A.det ≠ 0) {v : n → ℝ} (hmul : A.mulVec v = 0) : v = 0

A square real matrix with nonzero determinant has trivial mulVec kernel.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.zero_barycentric_unique {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (hw : ∀ (r : Fin (p - 1)), (referenceMap hp).value s w r = 0) (hv : ∀ (r : Fin (p - 1)), (referenceMap hp).value s v r = 0) : w = v

On a regular affine simplex, barycentric coordinates of a zero are unique, even before requiring positivity of every coordinate.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.perm_eq_one_of_strictMono {n : ℕ} (sigma : Equiv.Perm (Fin n)) (hmono : StrictMono ⇑sigma) : sigma = 1

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.top_weight_pos_of_zero {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) : 0 < ↑w (Fin.last (p - 1))

Any barycentric zero of the perturbed reference map has positive coefficient at the final top-cell vertex. If that coefficient vanished, the invertible block-vertex matrix would force all earlier coefficients to vanish as well, contradicting that barycentric coordinates sum to one.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.strictOrder_eq_of_top_weight_pos {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hwtop : 0 < ↑w (Fin.last (p - 1))) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) (label : Fin p) : z.bottom label = z.top label

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.strictOrder_eq_of_positive_blockCombination {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hwint : w.IsInterior) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) (label : Fin p) : z.bottom label = z.top label

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.removal_eq_identity_of_top_weight_pos {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hwtop : 0 < ↑w (Fin.last (p - 1))) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) (horder : z.bottom = z.top) (k : Fin (p - 1)) : z.removal k = k

Once the bottom and top orders agree, positivity of the final top weight makes the prefix sums strictly increasing, forcing the bar-removal schedule to be the identity.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.removal_eq_identity_of_triangular_gaps {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hwint : w.IsInterior) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) (horder : z.bottom = z.top) (k : Fin (p - 1)) : z.removal k = k

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.hasInteriorZero_toSimplex_iff {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : (referenceMap hp).HasInteriorZero (MaximalFlagCode.toSimplex hp z) ↔ z.bottom = z.top ∧ z.removal = 1

Positive barycentric solutions of the perturbed reference equation are exactly the selected maximal flags.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.zero_isInterior_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) (w : StandardSimplex (p - 1)) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value (MaximalFlagCode.toSimplex hp z) w r = 0) : w.IsInterior

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.zero_isInterior {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (hzero : ∀ (r : Fin (p - 1)), (referenceMap hp).value s w r = 0) : w.IsInterior

Every barycentric zero on an arbitrary maximal simplex is interior.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.hasInteriorZero_iff_selected {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (referenceMap hp).HasInteriorZero s ↔ IsSelected hp s

Relative-interior zero characterization for an arbitrary maximal simplex.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.determinantIndex_zero_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : AffineVertexMap.determinantIndex ((mapAt hp 0).determinant (MaximalFlagCode.toSimplex hp z)) = ↑((-1) ^ (p - 1) * MaximalFlagCode.coefficient z)

Determinant sign at zero in code coordinates.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.localZeroIndex_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : MaximalFlagCode.Code p) : (referenceMap hp).localZeroIndex (MaximalFlagCode.toSimplex hp z) = if z.bottom = z.top ∧ z.removal = 1 then ↑(MaximalFlagCode.coefficient z) else 0

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.coveringTopCell_eq {p : ℕ} (hp : Nat.Prime p) : (PrimeOrbitCycle.coveringCycle hp).TopCell = Simplex p (p - 1)

The covering top cell has dimension p - 1.

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.topRepr {p : ℕ} (hp : Nat.Prime p) (q : PrimeOrbitCycle.TopOrbit hp) : Simplex p (p - 1)

Canonical top-orbit representative, cast to the dimension p - 1 used by the reference map.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.topRepr hp q = ⋯ ▸ NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.topRepresentative hp q

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedFlagOfTopCell {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation.TopCell p) : Simplex p (p - 1)

The selected maximal flag associated with a top cell's label ordering.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedFlagOfTopCell hp c = NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedSimplex hp (↑c).rank

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedFlagOfTopCell_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (c : BarredPermutation.TopCell p) : selectedFlagOfTopCell hp (g • c) = g • selectedFlagOfTopCell hp c

Selected flags are equivariant.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.SelectedOrbit (p : ℕ) : Type

Quotient of the selected reference flags.

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.SelectedOrbit p = MulAction.orbitRel.Quotient (↥(NRR.PrimeSymmetry p)) (NRR.BarredPermutation.TopCell p)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedOrbitFintype (p : ℕ) : Fintype (SelectedOrbit p)

Equations

• NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedOrbitFintype p = Fintype.ofFinite (NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.SelectedOrbit p)

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.smul_castDim (p : ℕ) (g : ↥(PrimeSymmetry p)) {d d' : ℕ} (hd : d = d') (s : Simplex p d) : g • ⋯ ▸ s = ⋯ ▸ (g • s)

Relabelling commutes with a dimension recast of order-complex simplices.

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.selectedOrbitEquivTopSupport {p : ℕ} (hp : Nat.Prime p) : SelectedOrbit p ≃ { q : PrimeOrbitCycle.TopOrbit hp // IsSelected hp (topRepr hp q) }

Selected top-cell orbits and selected top-simplex orbits are canonically equivalent.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.card_selectedOrbit (p : ℕ) : Fintype.card (SelectedOrbit p) = FoxNeuwirth.referenceOrbitMultiplicity p

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceIndex {p : ℕ} (hp : Nat.Prime p) : PrimeOrbitCycle.TopOrbit hp → ZMod p

The local zero index of the reference map on each selected orbit representative.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.orbitCycle_coefficient_eq {p : ℕ} (hp : Nat.Prime p) (q : PrimeOrbitCycle.TopOrbit hp) : (PrimeOrbitCycle.orbitCycle hp).coefficient q = ↑(MaximalFlagCode.coefficient (MaximalFlagCode.simplexToCode hp (topRepr hp q)))

The quotient-cycle coefficient at a top orbit equals the code coefficient of the canonical representative flag, reduced to ZMod p.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.coefficient_mul_referenceIndex {p : ℕ} (hp : Nat.Prime p) (q : PrimeOrbitCycle.TopOrbit hp) : (PrimeOrbitCycle.orbitCycle hp).coefficient q * referenceIndex hp q = if IsSelected hp (topRepr hp q) then 1 else 0

On the selected support, cycle coefficient times local index is one; off the support it is zero.

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceZeroCount_eq {p : ℕ} (hp : Nat.Prime p) : (PrimeOrbitCycle.orbitCycle hp).zeroCount (referenceIndex hp) = FoxNeuwirth.referenceSignedOrbitCount p

noncomputable def NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.model {p : ℕ} (hp : Nat.Prime p) : FiniteOrbitZeroCountModel hp

The finite orbit zero-count model supplied by the reference affine construction.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceZeroCount_ne_zero {p : ℕ} (hp : Nat.Prime p) : (PrimeOrbitCycle.orbitCycle hp).zeroCount (referenceIndex hp) ≠ 0

The explicit reference orbit count is nonzero.

theorem NRR.AAK.simplestRoute_referenceAffineCount_complete {p : ℕ} (hp : Nat.Prime p) : Nonempty (FiniteOrbitZeroCountModel hp)

Step S5: the prime-orbit cycle carries an explicit regular affine reference map with nonzero signed orbit count.