python/cartan_dna_bridge.py:
- Constructs 8×8 Cartan crossing matrix (block diagonal: 4×2 pairs)
- Each 2×2 block [273 256; 256 273] has eigenvalues {529, 17}
- σ = 273/1792 = 39/256 (normalized diagonal weight)
- τ = 256/1792 = 1/7 (normalized adjacent weight)
- ∆ = (273-256)/1792 = 17/1792 (difference)
- The min nonzero eigenvalue 17 IS the gap numerator
docs/cartan_dna_derivation.md:
- Step-by-step spec for modifying dna_codec.py
- Replace thermodynamic weights with Cartan weights
- Expected output and verification
All derived values match the Lean reference exactly.
The DNA encoder can now witness the spectral gap chain.
Test harnesses added for all remaining AVM ISA ports:
- C (9 tests): arithmetic, saturation, comparison, overflow, control flow, locals
- C++ (9 tests): same test suite with std::optional-based error handling
- Scala (9 tests): functional style with Option return
- Fortran (4 tests): add, div, saturation, control flow (minimal Fortran test)
- Octave/MATLAB (4 tests): basic operations test
Milestone: 10/12 ports have test harnesses. Coq still pending.
