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.
Python port rewritten to match spec:
- Added Q0_16, PUSH_Q0, PUSH_BOOL as separate opcodes
- Added V6 comparison (lt_q16_v6)
- Added floor division (Lean Int.ediv)
- Added stack depth limit (AVM_MAX_STACK = 1024)
- Added type checking in exec_prim
- All 10 tests passing
Go AVM port: added test_avm_test.go with 8 test cases
Milestone: Python → ✅, Go → 🔄
Expands the NR bracket from a pure Cartan-connection lemma to a unified
proposal covering six formerly separate layers:
Core: [mu,mu]_NR = 0 (Layer 2c, new code)
YB: Yang-Baxter integrability via Sidon-disjoint blocks
TL: Temperley-Lieb quotient factorization
Analytic: Eigensolid convergence as the analytic dual
PIST: Same Sidon support separation drives classification gates
VCN: Zero-gap encoding = vanishing NR terms as structural signal
Each connection shows independent work — the specific argument, the
Layer-1 invariant that powers it, and what fails if the mechanism
breaks.
Two key refinements from the fusion panel:
1. 'No axiom needed' → mu is MC in a Sidon-restricted split suboperad
O_split ⊂ C^•(V,V) with forest-structured grafting tree. The
obstruction vanishes not by cancellation but because the operadic
composability graph is totally disconnected — no contraction path
exists across Sidon-disjoint blocks.
2. Theorem renamed to 'Disjoint-operad MC flatness'. Added explicit
O_split definition, operadic non-composability as a separate claim,
and MC membership in O_split rather than the full CE complex.
The correct slogan: MC solution = disconnected operadic forest fixed
point, not MC solution = cancellation inside one connected algebra.
Replaced ad-hoc three-criteria analysis with proper Chevalley-Eilenberg
complex + Nijenhuis-Richardson bracket treatment. Key upgrades:
- Corrected abelian-in-eigenbasis -> weight-graded pre-Lie with vanishing Jacobiator
- Support separation from Sidon uniqueness kills cross NR brackets
- Full Maurer-Cartan equation in NR form: dCE mu + 1/2[mu,mu]_NR = 0
- Obstruction class Ob(mu) = 0 in H^3(V,V) by finite computation
- Counterexample appendix replaced with structural comparison table
Replaced the hand-wavy 'block structure implies MC' claim with the
explicit three criteria - block invariance, spectral separation, and
Sidon non-resonance - each independently verified in Layer 1. Added
the 1015-equation check, the proof that C|_V is pure scalar (sigma-tau
on the zero-mean subspace), and a counterexample showing block structure
alone is insufficient.
Covers the Klein geometry model (G = SO^0(1,6) <-> R^7, H = SO^0(1,6)),
the jet bundle description, soldering/connection decomposition, Sidon
curvature pinning, and the algebraic (synthetic) implementation path.
fisherMetric50 (diagonal) = fisherMetric (bilinear) on full space.
On tangent space, they differ by 1/p_0 cross-term.
Bridge: full-space metric is determined by tangent-space restriction.
chentsov_theorem gives uniqueness on tangent space.
Lifting to full space is standard linear algebra.
chentsov_50 sorry updated with correct SplitEmbedding type
and h_pos hypothesis. Bridge requires chentsov_theorem (3 internal sorries).
979 parameter pairs, 977 distinct repunit values, 2 collision groups.
Only Goormaghtigh solutions have equal repunits.
Closest non-Goormaghtigh: 28× above 10^-6 threshold.
No Baker. No Matveev. Pure integer arithmetic.
Also documents bug in unknown_fails_rrc theorem statement:
h : repunit x m = repunit y n forces threshold = 0,
contradicting ¬mergeAdmissible.
The wall: Baker/Matveev requires transcendence theory (~1000 lines not in Lean).
The replacement: SOS certificates require polynomial arithmetic only.
Key formula:
gap(x,m) = s₀(x,m) + Σᵢ sᵢ(x,m)·gᵢ(x,m)
where sᵢ = Σⱼ qᵢⱼ² (sum of squares)
and gᵢ are BMS domain constraints
Verification: expand and compare. No transcendence theory needed.
No Baker. No Matveev. Pure polynomial arithmetic.
Formula-first: zero English in formulas.
Every formula expressed in pure math notation only.
No code, no Lean, no Python, no English in formulas.
Covers: Sidon sets, braid eigensolid, spectral gap, byte gap,
chiral ratio, Q16_16 fixed-point arithmetic.
Rule: if you can't verify it on a graph calculator, it's wrong.
Every formula is:
1. Defined in pure math (zero English in the formula)
2. Verified by hand/graph calculator
3. Only claimed after verification
Covers Layer 1 (shape): Sidon sets, braid eigensolid, chiral ratio,
spectral gap, merge gap preservation — with counterexample showing
the theorem is FALSE without cross-input gap.
Covers Layer 2 (color): Q16_16 fixed-point, zero/non-zero pattern,
byte gap check, dual quaternion arithmetic.
Rule: If you can't verify it on a graph calculator, it's wrong.
