Verification — Ladder V1–V4 × 8 languages

An independent checker, an interactive laboratory, seven pinned toolchains — and the multi-language ports of milestones M1–M3, landed.

The principle

Numbers printed by the code that defines them are repetition, not verification. The TRIVORTEX ladder therefore lives in verification/trivortex/python/verify.py — a script that shares no code with the core document: it re-implements the closed form of Theorem 3.1, the Chaplygin combination, the Kirchhoff right-hand side and its own RK4 stepper from scratch, then checks the document's claims against its own arithmetic. Every run emits a JSON protocol (parameters, residuals, tolerances, wall time) — the same "numbers are bound to runs" discipline used across the repository.

The four checks

Check	Statement	Criterion (registered)	Result
V1	Theorem 3.1 closed form: 2π/3 choreography + periodicity T_r = 2π/ω	separation error ≤ 1e-12; periodicity residual ≤ 1e-12	PASS — 6.9e-14 / 9.4e-14
V2	Lagrange triangle: rigid rotation at ω = 3Γ/(2πa²)	shape drift ≤ 1e-10; ω relative error ≤ 1e-6	PASS — 1.6e-14 / 2.9e-12
V3	Vortex integrals H, P, Q, I conserved (equal Γ)	worst relative drift ≤ 1e-10	PASS — 2.9e-14
V4	Integrals conserved for Γ = (1, 2, 3), generic triangle	worst relative drift ≤ 1e-10	PASS — 2.9e-14

Run it

python3 verification/trivortex/python/verify.py --preset quick    # ~0.5 s (CI)
python3 verification/trivortex/python/verify.py --preset default  # ~2 s
python3 verification/trivortex/python/verify.py --preset full     # ~35 s
python3 verification/trivortex/python/lab.py                      # the interactive laboratory
python -m pytest verification/tests/ -v                           # 63 tests

Honesty notes

The C_Ch drift is a diagnostic, not a conservation law. The combination C_Ch(t) = r²(θ̇ − q·A_θ) with A_θ = 1/r oscillates together with the radial modulation of Theorem 3.1 — Section 6 of the document records its endpoint drift over the window [0, 100·T], and the ladder reports the same number as a diagnostic with no pass/fail role. The window-independent conserved quantities of the dynamics are the vortex integrals H, P, Q, I — and those are what V3–V4 certify. Any future language port must keep this separation.

Multi-language roadmap — milestones M1–M3 landed

Directory	Artifact	Milestone	Status
trivortex/python/	working ladder V1–V4 + JSON	M0	done
tests/	pytest guard (63 tests)	M0	done
trivortex/python/lab.py	interactive scientific laboratory — bilingual, custom parameters, 600 dpi figures	M0+	landed
coq/	Trivortex.v — statement layer, choreography + periodicity proven, zero axioms	M1	landed
lean4/	Trivortex.lean — Mathlib formalization, #print axioms closed	M1	landed
rust/	f64 numeric twin + bilingual lab — 14/14 tests, protocol committed	M1	landed
isabelle/	Trivortex.thy — HOL session + optional SMT bounds	M2	landed
agda/	Trivortex.agda — constructive C3 rotation lattice (rot³ ≡ id)	M2	landed
cpp/	CMake/CTest port + −O2 benchmark — 21 guards, ≈1.7e7 rhs/s	M3	landed
haskell/	Double + exact ℚ(√3) dual — anchors hold by computation	M3	landed

Next — roadmap §7.1. M4 hardening: blocking port jobs after three green days, the Isabelle SMT session online, the Lean Mathlib cache, a generated site table, release v1.2 · M5 depth: 50-digit mpmath anchors, the Julia third numeric twin, the Chaplygin integral identity proven in Coq and Lean, the exact Haskell run over the full ladder · M6 widening: the V5 regular N-gon ring check, the rust-vs-c++ benchmark board. Every track names its acceptance criterion in advance.

Seven Docker toolchains are pinned under verification/docker/; every port keeps its checked acceptance criteria in its directory README, and the CI runs all ports non-blocking via verification-ports.yml until each stays green for three consecutive days. Full details in the framework README.