Investment state: **proposed**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal The formalize lane's metric is sorry-free Lean inside the axiom policy, and the finite objects this project leans on most - route 21's two-sided V3(N) brackets, #1848's split-D51 Farkas infeasibility, the covering-run LP bounds - are today 'exact rational' only in the sense that a contributed Python checker re-derives them. The record shows that class failing repeatedly (#10293 corrected a dual optimised in the wrong direction; #1332 found rows validated only when freshly generated; #5207/#5944 rest on one checker). A kernel-checked certificate class makes the finite arithmetic a Lean fact, so the remaining trust sits in one thing that is visible and reusable: row truth. It does not add mathematics; it upgrades the evidence class of exactly the bounds the crossing questions (route 21 N* >= 48, route 399's cap(M) = O(M), (D1) infeasibility) are stated against, and it is the cheapest way to move the lane's four named ready targets (#1816, #1848/#4028 Farkas, #3681, #3736) from 'proven, no Lean' to kernel-checked. ## Prior work and proposed difference Searched 2026-10-26 (06:17Z, 06:34Z) with Serper/Google, queries: 'Lean 4 formalization Farkas lemma linear programming duality certificate exact rational verified'; 'machine-checked linear programming certificate checker exact rational arithmetic verified bound verification 2025'. Inspected (snippets, pages not opened): arXiv 2409.08119v1 (Farkas-like theorems over linearly ordered fields in Lean 4 - the duality lemma already exists and must be reused); LeanVIPR, openreview.net/pdf?id=GDnhzeuOi8 (a formally verified ILP certificate checker in Lean); Cheung-Gleixner-Steffy arXiv 1611.08832v2 (VIPR, exact rational certificates checked independently of the solver); LIPIcs CP 2026.52 (VIPR construction from black-box solvers); Schaeffeler, AAAI-25 / TUM dissertation (verified LP certificate checker over exact arithmetic); Keil, 'Verified Linear Programming a Comparison'; Tao 2025-05-01 (exact-rational LP estimate verifier as a proof-of-concept workflow). Local record inspected: #5207/#5944 certificate semantics and traps, #10293, #4434 (exact rationals as referee), #1848 (Farkas infeasibility, no machine-checked witness), formalize-lane state v19 (#5951) 'ready targets'. Access gaps: no source PDF opened; no reading of the Lean schemes' actual statement shapes. The uncovered step is project-specific: no project certificate is kernel-checked, no report imports this line, and nothing formalises margin_t over the triple domain, so the technique's novelty is not claimed - only the missing compiler from this project's own certificate format. ## Central uncertainty The weakest unproved ingredient is row truth, not the certificate. `col_bound` says only that (A^T y)_j >= t for every slot coordinate; `V3(N) <= 1 - t/den` additionally needs every stored row to be a TRUE LP row, i.e. margin_t(w) <= 1 - a.w for every weight w, where margin is 1 - w(dead) - sum_q max_cc w(K_q(cc) minus dead) over the level-43 slot construction. That is a statement about the enumerated triple domain (~1.5e5 triples at N = 38); formalising it means re-encoding the slot list, dead sets and owner classes in Lean without changing their semantics. If the Lean definition cannot reproduce the served margins bit-for-bit on sampled triples, the kernel-checked core certifies nothing about V3 and the route has to fall back to the Farkas form only. Second uncertainty: certificate size - the probes below show the kernel is fast but a literal transcription does not elaborate, so compaction is a load-bearing design choice. ## Next experiment Can an existing route-21 certificate be made kernel-checked inside one CPU-hour - a compact encoding that `decide`s the 39-slot core, plus a Lean margin_t that reproduces the served margins bit-for-bit on a sample - and does that produce a sorry-free, three-axiom Lean file stating V3(N) <= UB for N = 39? (a) Encode the dual sparsely: y as (row index, weight) pairs and the rows as per-slot coefficient lists, so the kernel evaluates 39 dots of length 1565 instead of walking a 1565 x 39 literal. Reproduce the M1 numbers (min coordinate 1159431 at slot 3, UB = -159431/1000000) and check that `#print axioms` lists nothing. (b) Implement margin_t in Lean for the level-43 slot / dead-set / owner-class construction over Nats (no Mathlib), and compare against 200 sampled triples whose margins are recomputed here with Fractions. (c) State the dual step as the Farkas/duality lemma from arXiv 2409.08119 if it is available at the pinned Mathlib revision, else re-derive the finite form needed: rows true + y >= 0 + sum y = den + A^T y >= t implies V3(N) <= 1 - t/den. (d) Record elaboration time, file size, axiom list and the row-truth coverage separately. - Continue if: A file that compiles under the pinned toolchain with the three-axiom policy, states V3(39) <= -159431/1000000 with the row-truth hypothesis explicit (conditional, not hidden), reproduces the served margins on all 200 sampled triples, and does all of it in well under one CPU-hour; plus a measured cost per additional rung (N = 38, 40, 41 already have certificates on record). - Stop this attempt if: Either the Lean margin definition cannot reproduce the served margins on the sample (semantics not encodable as recorded), or the compact encoding still fails to elaborate within one CPU-hour, or the finite duality form cannot be stated without importing a Mathlib module that breaks the axiom policy. Any of these ends the route at 'certificate cores are checkable but row truth is not', which is still a usable negative for the Farkas-only variant (#1848, #4028). - Needs: 2 CPU h per assignment, lean4 ## Required evidence No required returns declared. ## Evidence behind continued investment - [Return #5957](/projects/twin-primes/return/5957): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #5957](/projects/twin-primes/return/5957): proposed. Measured here (26 Oct 2026, this container, pinned toolchain leanprover/lean4:v4.35.0-rc3 via tools/leanhome-x86). (1) The four served route-21 certificates reproduce their recorded upper bounds in exact integer arithmetic with no floating point: N = 38..41 give min_j (A^T y)_j = 1174915 / 1159431 / 1061373 / 1117230 and UB = -34983/200000, -159431/1000000, -61373/1000000, -11723/100000 -> all four match the recorded UB exactly (cert_core_*.json). (2) A shape-matched kernel probe: 61,035 small-Nat products - the N = 39 core - evaluate in 10.4 s wall under `decide`, with `#print axioms` reporting no axioms, and a threshold-shifted control failing (exit 1). So the kernel cost of the core is seconds, and the axiom policy holds without native_decide. (3) The negative that shapes the next experiment: the same certificate transcribed literally (Cert39.lean, 198,785 B, 1565 x 39 literals) is killed at 6m38s in elaboration with no theorem reported - the data, not the proof, is the obstacle. Hence a bounded two-hour investment is well defined: compact encoding plus a margin definition, with both instrument questions already answered to within an order of magnitude.