Repository navigation
Combine PR #3 shared exclusions with retained totals and stage sharing - #4
Conversation
…ithmetic Three libraries in the same Lake project prove each PR's counts, eta, log bounds, exponent certificates or moments, slacks, margins and min g > kappa (310 theorems, standard axioms only). PRChecksB.PR5Analytic also proves CrocSwap#5's analytic inequalities and PRChecksC the CrocSwap#10 bulk-guard Taylor bound. Drift tests tie every Lean literal to each PR's own certificate. The PR files they read are vendored under formal/open-prs/data with their head commits and SHA-256 in MANIFEST.json, checked by tests/test_open_pr_lean.py. formal/open-prs/README.md records scope (CrocSwap#1-CrocSwap#12 as of 2026-10-08) and the findings: the CrocSwap#3/CrocSwap#8 ceiling, CrocSwap#3 docs line 102, CrocSwap#4's outdated notes, the CrocSwap#5/CrocSwap#6 g4 wording, CrocSwap#6's window size, and CrocSwap#5's Harvey-van der Hoeven wording. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015MYnETxrAa57d3wqw3v9HR
|
Integrated and retained on main in 377e2bd. Thank you @dleen for this contribution. The complete original source tree at Reviewed scope: Retained-total complex circuit: full h24 coefficients, role frames and rational guards; small dirty-state and both physical phase directions; exact historical 591/10^12 assembly. Original PDF is stale and retained only as history. The batch review and per-file dispositions cover every original changed path. Local focused checks passed; regenerated artifacts match the submitted sources. Attribution is also recorded in CONTRIBUTORS.md. This is integration of historical research and finite evidence, not a new selected κ or full formal verification of inherited tape/analytic interfaces. Linux replay jobs are tracked separately. |
Combine the shared-exclusion producer from #3 with retained exclusion totals and stage-1/3 bank sharing. At h=24, this reduces auxiliary roles to 90,950 and certifies complex saving 2.97e-8, about 2.12× #3's 1.4e-8. The bit producer remains unchanged, so the conditional headline stays κ = 591/10¹² > 2⁻³¹; the combination supplies additional complex headroom.
scripts/complex_circuit.pyis copied verbatim from eumemic's Claude-assisted #3 atdfe5b818aad4d386cb5dd7d76df108088107765d. The composition retains existing one-point exclusion sums and the global sum, uses grouped low/full scatter, and shares stage-1/3 auxiliary banks. The larger global coefficient is implemented as half-sized passes: every added scalar gate is charged, while repeated equal-frame incidences add zero rank. Arbitrary dirty scratch, both frame directions, and endpoint corrections are preserved.The focused changes include the exact producer/certificate, regression checks, Markdown composition argument, and regenerated alternative manuscript patch. A separate proposition binds the new constants; the preceding rectangle proof/PDF remains available as a historical variant. The pinned upstream source is unchanged. Lean research and agent exploration are excluded.
Validation:
make verifypassed 168 tests and all patch checks. After cleanup and the proof-text correction, all five focused tests pass; the combined certificate and patch reproduce byte-for-byte, every recorded source hash matches, and the imported #3 builder is byte-identical. Full h24 checks cover side coefficients, retained integer multiplicities and both compiled frame directions; h8 checks cover dirty-scratch basis inputs, normalized scatter coefficients and all physical phase edges. An independent agent review checked the composition and gate accounting. The new TeX/PDF was not rebuilt.This remains conditional on the retained fixed-tape, compact-control and analytic interfaces, rather than a full formal multiplication theorem or a runtime benchmark. Prepared with substantial Claude and OpenAI Codex assistance; #3's producer is credited to eumemic, and grouped retention/stage sharing to dleen.