Step 2: the maximal-flag determinant sign

For an explicitly coded maximal flag, the successive bar-removal matrix is the permutation matrix of the inverse removal permutation. Its determinant is therefore the sign of the removal permutation. Together with the bottom-cell permutation orientation, this identifies the subdivision coefficient with MaximalFlagCode.coefficient.

Combining this identity with the bijection proved in Step 1 constructs CompleteEncoding, closes the rank-two cancellation theorem, and proves that the top-flag subdivision chain is a genuine mod-p simplicial cycle.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageIndex_castSucc_val {p : ℕ} (hp : Nat.Prime p) (k : Fin (p - 1)) : ↑(stageIndex hp k.castSucc) = ↑k

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageIndex_succ_val {p : ℕ} (hp : Nat.Prime p) (k : Fin (p - 1)) : ↑(stageIndex hp k.succ) = ↑k + 1

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.barDifferenceMatrix_toSimplex_apply {p : ℕ} (hp : Nat.Prime p) (z : Code p) (r k : Fin (p - 1)) : TopFlagSubdivision.barDifferenceMatrix (toSimplex hp z) r k = Equiv.Perm.permMatrix ℤ (Equiv.symm z.removal) r k

One successive bar difference is the Kronecker coefficient recording the removed bar.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.barDifferenceMatrix_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : Code p) : TopFlagSubdivision.barDifferenceMatrix (toSimplex hp z) = Equiv.Perm.permMatrix ℤ (Equiv.symm z.removal)

The complete bar-removal matrix is the inverse-removal permutation matrix.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.barRemovalDeterminant_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : Code p) : TopFlagSubdivision.barRemovalDeterminant (toSimplex hp z) = permSignInt z.removal

The bar-removal determinant is the sign of the removal permutation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.integralCoefficient_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : Code p) : TopFlagSubdivision.integralCoefficient (toSimplex hp z) = coefficient z

The determinant subdivision coefficient agrees with the explicit code coefficient.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.completeEncoding {p : ℕ} (hp : Nat.Prime p) : CompleteEncoding hp

Step 1 plus the determinant calculation gives the complete maximal-flag encoding.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.rankTwoCancellation : TopFlagSubdivision.RankTwoCancellationTheorem

The internal rank-two source sums vanish for the actual simplicial chain.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.topFlagCycle {p : ℕ} (hp : Nat.Prime p) : TopFlagSubdivision.boundary hp = 0

The top-flag subdivision is an unconditional mod-p simplicial cycle.

theorem NRR.AAK.simplestRoute_topFlagCycle_complete {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.TopFlagSubdivision.boundary hp = 0

The best next move after maximal-flag classification: identify the determinant sign and close all finite-combinatorial S3 obligations.