Repository navigation
Conversation
|
Thank you @chafreaky. This contribution is now recorded on main in the scoped reconciliation review and contributor credits. Contribution: Joint split/dual source combinations with restored import state. Review and limits: Exact-head CI evidence; retains the independent word checker and complete profile rather than assuming additive gains. The complete original source, proof/research notes, notices and relevant replay/CI evidence are retained through the pinned source archive. The review distinguishes fresh runs, exact-head historical CI and prior integration evidence. Closing this historical PR as reconciled; its obsolete headline does not replace the current selected bound, and draft/retracted claims retain their explicit qualifications. Reviewed head: |
Change and mathematical scope
This composes PR #59's split-pair group choices with PR #55's dual-suffix layout and the unchanged ranked joint compiler from PR #60. It improves PR #60's conditional exponent saving by 1.3974275711%:
The result remains conditional on the inherited base theorem and all-size analytic, residual-compiler, routing, recovery and fixed finite-alphabet multitape interfaces. This comparison is to #60. Main now records the stronger reviewed saving 5.1016920170078e-5; this contribution preserves a separate, weaker conditional construction and does not claim to improve that current frontier. No global optimization or practical runtime claim is made.
Construction
Use split-group vectors
[1,3,2]at h=23 and[1,2,2]at h=25. Both axes use PR #55's native suffix layout: input order at the top, the inherited deeper support orders, and the original total fold orders. The exact PR #60 ranked reclamation engine is unchanged. No paid clones or recorded PR #59 permutation overrides are used.Every selected frame transition, clearing XOR, output copy and cleanup is included. The exact bit saving is
2415663683/50000000000000, full rank mass is84903327575, and rank deficit is1846900. The fixed I+J data geometry and complex branch are inherited unchanged.The new package is separate in
research/split-dual/, with dedicated compiler, verifier and certificates. It privately loads the graph sources and restores temporary provider/module substitutions, including exceptional exits. Original PR #59 files and a complete immutable PR #60 comparison certificate remain pinned. Adding the target and notices refreshes only the old package's root-file source bindings and derived metadata; its code, words, profiles, numerical result and existing verifier remain intact.Attribution
The inherited construction retains Avi Eisenberg (@ikeboy) (#53), Rohan Arun (@rohanarun) (#44, #49), RaD (@hipotures) (#41, #51), @icekylinx (#36), Dominik Scholz (@DominikScholz) (#35), James Chang (@jamesyc) (#34), Zhihao Chen (@jacklightChen) (#7), and Aurel Prosz (@Paureel) (#1).
Earlier contributions and retained checks also credit @Bortlesboat (#2), @dleen (#4), Ryan S (@princezuda) (#26), Alejandro Zarzuelo Urdiales (@alejandrozu) (#45), and Douglas Colkitt (@Mister-Meeseeks) (maintainer integration). Swapnil Jain (@Swapnil-jain) retains the linked two-stage credit recorded in #29. OpenAI, David Harvey, Joris van der Hoeven and every earlier contributor retain their manuscript/source attribution. All original notices, licenses and contributor-specific AI-assistance disclosures remain attached to their sources.
Validation
All 36 checks now pass at final receipt-only head
701b1246e2def8b022a14309b5171138f2b12a52, including all three inherited Lean packages. The preceding receipt head hit an external Lean 4.31.0 download HTTP 500 before the matrix proof ran; the accurate metadata-only retry preserves every mathematical source, pin, word, profile and numerical certificate.The verified construction is
b07443b7fb73200eeca4e681a2bccc226ef938b1, with source freeze43368c897bf61e6cab9d7275451241d57083f8381af9871cf4bb8cc1d67e129f. The final repository receipt is a metadata-only follow-up; it does not change any source pin, word, profile or numerical certificate.make -j1 verify-jointpasses at the verified construction in 309.334 seconds, with a byte-clean checkout. This includes the predecessor witnesses and independent PR60/61 arithmetic/source binding.29a504fcompleted five groups before Apple clang rejected an inherited OpenMP flag; the remaining six completed with a task-local adapter to installed libomp and existing hash-verified Boost. Exact attempt and continuation records are retained. Canonical ordering of two derived receipts was restored without changing their parsed JSON values, then rechecked clean atb07443b.b07443b: eleven groups on Python 3.11, 3.13 and 3.14 plus all three inherited Lean packages. Both workflow invocations are green, 72 successful check runs total.ac0bc93full run also passed: 443 integrated tests, all focused checks and 20 patches in 1096.909 seconds. That historical record retains its own tested source freeze.Main
fc74109is integrated additively: all upstream additions and the complete current CI architecture remain. Independent reconciliation review confirms unchanged physical/numerical witnesses and only three root-file pin updates. The maintainer-reviewed headline remains 5.1016920170078e-5; this PR's separate conditional construction is weaker than that current frontier.Reproduce with:
certificates/split-dual-repository-validation.jsonrecords exact commits, source hashes, checks and log digests. Seeresearch/split-dual/PROOF.mdfor the local algebra and inherited all-size residual-compiler, routing, recovery and fixed-tape obligations. The inherited Lean checks do not constitute a formal proof of this complete multiplication theorem.