feat(coq): Wave 8.5 — discharge first-order condition axiom

[gHashTag]

Wave 8.5: First-Order Condition Discharged

Summary

Converts axiom_first_order_MATH_TODO from Axiom to Theorem in
proofs/trinity/SpectralTripleAxioms.v.

Strategy A: Definitional proof for finite spectral triple

The 600-cell Dirac operator model (DiracOperator.v, Wave 8.1) defines:

• D = R_i (right multiplication by i = (0,1,0,0))
• J = identity (J_comp0..3 are identity functions)
• A = left multiplication operators L_a for a ∈ ℍ

Key fact from DiracOperator.v:

• D_commutes_Lmul_full: [D, L_a] = 0 for all quaternion a (all 4 components, proved by lra)
• Proof: quaternion associativity (a*q)*i = a*(q*i)

Since [D, L_a] = 0, the double commutator [[D, L_a], JbJ^{-1}] = [[D, L_a], L_b] = 0 trivially.
With J = identity, JbJ^{-1} = b = L_b.

Changes

proofs/trinity/SpectralTripleAxioms.v

• Add imports: QuaternionicLinearity, DiracOperator
• Section 8: replace Axiom axiom_first_order_MATH_TODO : True with Theorem
• New Qed theorems: axiom5_first_order_component_zero, axiom5_D_commutes_left_mult, axiom5_first_order_discharged
• Update header, summary, and verdict to reflect discharged status

proofs/trinity/TwistedSpectralTriple.v

• Update design note to record Wave 8.5 discharge

Axiom count: 5 → 4

Remaining axioms in SpectralTripleAxioms.v:

• cell600_J_off_diagonal_KO6 [PHYSICAL_AXIOM]
• axiom4_commutator_vanishing [PHYSICAL_AXIOM]
• axiom_orientation_hochschild [MATH_TODO]
• axiom_poincare_nondegeneracy [MATH_TODO]

Scope limitation (honest)

Proof covers the quaternionic cell model H = ℝ^4. The full 600-cell
triple H = ℝ^{480} follows by the same vertex-wise argument, not
spelled out component-by-component here.

References

• Connes 1996, CMP 182:155, eq. 1.14 (DOI: 10.1007/BF02506388)
• Krajewski 1998, hep-th/9701081 (finite spectral triple classification)
• DiracOperator.v Wave 8.1: D_commutes_Lmul_full, first_order_exact