Lean certificate check

[princezuda]

Change and mathematical scope
This PR inherits the dependencies of OpenAI's theorem and the Harvey–van der Hoeven results. If the dependency or dependencies are found to be invalid, this is likely invalid as written.

It adds formal and independent checks only. No bound, certificate, patch or note changes. Nothing here is a formal verification of the full multiplication theorem.

formal/lean/ (Lean 4 v4.21.0, Mathlib v4.21.0). Every theorem depends only on propext, Classical.choice and Quot.sound; there is no sorry and no native_decide. It proves:

the κ = 83/10¹² certificate arithmetic: the counts, η, the exponent certificates, all 31 slacks, the margins, and 2⁻³⁴ < κ < g₃;
the exact scoped ceiling κ < U ≈ 8.3695980744·10⁻¹¹, with a negative control showing the enclosure exceeds U·(1 − 10⁻²⁴);
the guard note's depth derivation (Guard.lean), for every depth function that satisfies the note's two recursion inequalities, instantiated at the certified constants;
the paired circuit's frame algebra (Frames.lean): neighbor indicators are orthogonal under I − J/9, and spans of triples through a common point are anisotropic;
the compact-control address algebra (Movement.lean): the four-step parity identity, the later-source pass, the no-carry guard with exact packed-digit updates, and the repair permutation;
the layout's row arithmetic (Layout.lean).
formal/lean/SOURCES.md pairs every declaration with the note, upstream or certificate line it formalizes.

formal/circuit/. An independent check of the R = 509194 circuit that imports none of this repository's code. It recomputes every support from scratch: 450394 additions, all with disjoint supports; 58800 partial outputs, all exact; every target's neighbors partitioned; a common point at every node; and c + q = 509194 roles.

formal/open-prs/. The certificate arithmetic of the open PRs #3–#12 (libraries PRChecksA/B/C, 310 theorems), including #5's analytic inequalities and #10's bulk-guard Taylor bound. No certificate value is wrong. Circuit role counts are taken as given, and constructions written only in prose are not checked. #1 and #2 are superseded and were not Lean-checked. PRs opened after #12 are not covered. Findings:

#3 and #8: the "next ceiling" κ < 5.92·10⁻¹⁰ holds only with the bit exponent fixed at 1 − 296/10¹¹. The published h = 50 network supports 1 − τ = 2964/10¹², so the ceiling for that network is κ < 593/10¹². Their conclusion κ < 2⁻³⁰ is still valid.
#3: docs/research/complex-circuit.md:102 writes a_b/5 < 5.92e-10, but a_b/5 = 5.92·10⁻¹⁰ exactly, so the < should be =.
#4: its notes and abstract describe an older construction (R_aux = 365760, 1 − σ = 750/10¹¹), not the certified one (R = 90950, 1 − σ = 2970/10¹¹). The notes are invalid as written; the certificate and κ = 591/10¹² check.
#5 and #6: "g₂, g₃, g₄ ≤ a·min{ε, 1 − ε}" is false for g₄. At #5's witness, ε = 49999/100000, so g₄ = a(1 − ε) is slightly larger than a·ε. The true statement is min{g₃, g₄} ≤ a·min{ε, 1 − ε}, and both ceilings still hold.
#6: "a further 3% on a_b would close this window" holds only at the chosen β = 19/25. The guard allows smaller β, so the window closes at about 7.7%.
#5, Harvey–van der Hoeven wording. Its use of the lemmas holds: its parameters fail the literal hypothesis θ ≥ p/α⁴, but the proofs use that hypothesis only to obtain α²θ ≥ 1, which #5 assumes directly, and in one cost line, which #5 replaces. The text should:
say that θ ≥ p/α⁴ was also used to obtain α²θ ≥ 1;
add one sentence that the proofs of Lemmas 4.8, 4.9 and 4.11 use only 2 ≤ α < √p, s < t < 2^p, p ≥ 100 and the norms of Proposition 4.7(i);
correct the E map: its error bound with F = e^(πα²/4) fails once α ≥ 21. With F := 2^⌈1.14α²⌉, P = 34p still suffices.
None of these findings changes a headline κ.

Not verified:

the tape-machine level: tapes, streaming and running time;
that the algorithm meets the depth-recursion hypotheses;
the open PRs' prose constructions and circuit role counts;
the upstream theorem.
Prepared with substantial assistance from Claude (Anthropic).

Validation
cd formal/lean && lake build builds all four libraries.
python3 -m unittest discover -s tests passes: 169 tests, 4 of them new.
test_lean_sources: every declaration is listed in SOURCES.md, every cited line still contains its quoted text, and every certificate value equals its Lean literal.
test_paired_circuit_check: the independent checker accepts the real circuit at h = 14 and rejects mutated circuits.
test_open_pr_lean: the drift tests for #3–#12, plus SHA-256 checks of the vendored PR files against their recorded head commits.
The full h = 50 circuit check (formal/circuit/check_paired.py) takes about 2 minutes and is not part of the test suite.
Finite tests check implementations and identities; the Lean proofs cover only the statements listed above.