The selected conditional saving is κ=0.0016127213726553, Jeremy Kothe's
#596 on #591/#592 with eumemic's #543 bit supplier. See the
review,
integration receipt,
selected record and
PR ledger. The public replay is make frontier596-verify.
#593/#599 add scoped Lean proofs; #589 adds bit headroom; #595/#598 add research. #594's independent replay contribution is incorporated, while its older branch differences await reconciliation. All inherited all-size/realization/hosting/ precision/tape/analytic conditions remain; this is not a full formal proof of multiplication. Remote Linux CI status is recorded separately from local checks.
The selected reviewed conditional witness is κ=400569730495803/250000000000000000=0.001602278921983212, from Jeremy Kothe's #588 with eumemic's #543 bit supplier. The preceding #535/#510 checkpoint is preserved.
See the selected record,
review and assumptions,
execution receipts, and
per-PR dispositions.
The public make frontier588-verify command cold-rebuilt both finite suppliers
and their exact composition. All-size/compiler/common-label/mutable-basis,
pooled-cell hosting, normalized residual, precision/tape and analytic
interfaces remain conditional. Linux CI is tracked separately; no full Lean
multiplication theorem is claimed.
The frozen round covers 43 construction, research and tooling PRs through #588. Separate Lean proposals and later arrivals stay in the next queue. Parallel and superseded mechanisms, exact diagnostics and negative results retain attribution in the contributor record. The research integration index preserves earlier non-frontier contributions. Larger pending claims remain proposals until reviewed.
Earlier “selected” statements below are historical snapshots.
The selected conditional witness is κ=330942774629799/500000000000000000 =0.000661885549259598, from Dugongue's #186, on chafreaky's #181 and eumemic's #168. It is approximately 2^-10.56113: 43.60% above the preceding published checkpoint and 40.18% above the recycled-bit review checkpoint.
See the round-eight review,
selected record,
construction,
bank scheduling supplement,
and integration validation.
Reproduce with make entrance-bank-verify.
Published on main on 2026-10-09; the receipt identifies the tested branch/head.
The retained analytic, uniform-recursion and fixed-tape interfaces remain
assumptions. Finite replay and scoped formal contributions do not formalize
the multiplication theorem. #185's reviewed leaf bootstrap does not further
raise this witness, whose complex supplier already binds.
The assembly-domain audit distinguishes the
enforced b<1/32 range from the balance kappa<a/(1+a) and the independent
retained Gaussian condition kappa<1/4. Its larger-supplier examples are
arithmetic diagnostics, not new witnesses or an enlarged theorem domain.
The preceding reviewed recycled-bit composition was κ=0.000472154791; its round-seven review retains the evidence.
Earlier local experiments and rounds-three-through-five reviews are now preserved as dated historical records. Their old frontier and pending-work statements do not supersede this page; the retired shared-aggregate search remains retired.
Everything below is historical and retains its checkpoint-specific scope.
The selected conditional witness is κ=4609169/10000000000=0.0004609169,
from icekylinx's PR #144.
This is about 9.03 times the preceding main saving, approximately 2^-11.0832.
It is above 2^-12 and below 2^-11.
The construction builds on icekylinx's compiler lineage, an664's #128 completed-core sharing, eumemic's #117 producer, Zhihao Chen's #97 physical ledger and Swapnil Jain's underlying frozen word. See the review and attribution, validation receipt, selected result record, and reproduction guide.
The retained upstream analytic, semantic and fixed-tape interfaces remain assumed. The finite controls and written audit do not formally verify the full multiplication theorem. The review distinguishes local checks from head-pinned Linux CI evidence; no independent human peer review is claimed.
Everything below is historical. Its “current” and “selected” statements refer to the corresponding checkpoint.
The selected conditional witness is κ=25508460085039/500000000000000000 =5.1016920170078e-5 > 2^-15, from Avi Eisenberg's #62 pair assembly, eumemic's #57 compiler, and Alejandro Zarzuelo Urdiales's #61 parameter refinement. It is 23.71% above the previous #49 release, and remains below 2^-14. See the review and contribution ledger, independent arithmetic, and selected certificate.
The original #109 framework and inherited all-size analytic/fixed-tape interfaces remain assumed. Scoped Lean checks do not prove the full algorithm. Submissions after #62 are not included in this review checkpoint.
Everything below is historical; its numerical “current” and “latest” statements refer to the corresponding checkpoint.
The selected conditional witness is κ=4123863984/10^14=4.123863984e-5 > 2^-15,
from PR #49 at f95d2910e027495983b53cae1693cf535abf2569. It improves the
previous PR #39 release by 6.10%, retaining its analytic and fixed-tape contracts.
See the follow-up review,
integration record,
exact certificate, and
contributor record.
PR #45 (Gaussian parity and finite tensor execution) and PR #26 (historical arithmetic and algebraic contracts) are incorporated as scoped formal verification. Their Lean builds and axiom audits do not prove the complete multiplication theorem. The original #109 framework remains assumed; no independent human peer review is claimed.
The preserved research index collects the earlier compression and topology searches, with scoped exclusions and reproduction commands.
The previous PR #39 release and tested 2^-30 checkpoint at 1a74950 remain
preserved. Everything below is historical: “latest” and “current” refer to the
checkpoint, not the selected community follow-up witness.
Updated October 8, 2026. Author: Douglas Colkitt.
The latest included conditional witness is kappa=2^-30. Its note, certificate, and independent patch are described in the review guide. The previous 2^-31 construction and all older witnesses remain unchanged.
The bit circuit uses F3 scalar arithmetic and rational frames on five-subset labels at h=29. Its complete counts are
m_b=24389, W_b=589493540769997500,
s_b=14377157287342062574725,
a_b=467/10^11.
The complex circuit is retained at a_c=5/10^9. Parameters are
epsilon=1999/10000, c=1, beta=1/100, zeta=1/1000,
delta=1/10^6, C1=4961/1000,
lambda=1-4669/10^12, lambda'=1-4668/10^12,
kappa=2^-30.
The exact minimum assembly margin is
2332833/2500000000000000 > 2^-30. The bound remains conditional on the
pinned upstream theorem and the retained written extensions. Finite checks
and manuscript compilation are not independent mathematical verification.
Zhihao Chen's earlier PR #7 contains the same ternary motif with a different producer and stronger claimed bound. Further pending contributions claim larger improvements. See the contribution-review index for attribution, dependency order and the distinction between a submitted claim and a reviewed result. This checkpoint asserts neither priority nor a strongest-known algorithm.
Everything below records the preceding integration. Numerical uses of “current,” “latest,” or “retained” in that historical record refer to 2^-31; the parameters above supersede them for this checkpoint.
| State | Exponent saving kappa | Artifacts |
|---|---|---|
| Earlier published baseline | 2^-59 |
paired note, patch |
| Published compact-control checkpoint | 83/10^12 > 2^-34 |
note, certificate, patch |
| Integrated follow-up, pending publication | 2^-31 |
note, certificate, patch |
The latest witness increases kappa by approximately 5.61 times over the exact
preceding witness; the dyadic comparison 2^-34 to 2^-31 is eightfold.
These compare exponent savings, not practical runtime. All earlier certificates,
patches and the pinned upstream source remain unchanged.
The complex-network construction uses weighted
rectangles for disjoint triples, shared sums for intersection-two triples,
and binary phase frames valid in both signed directions. Transparent computation
restores arbitrary auxiliary inputs. A matching shares the complete first/third
auxiliary banks. At h_c=26, it has
m_c = 17576, W_c = 7082222160000,
s_c = 124477130005280000,
a_c = 1-sigma = 5/10^9.
The bit network remains h_b=50, m_b=125000, with
a_b=1-tau=296/10^11. Thus the complex interface now has the larger saving.
The bit interface is the bottleneck.
The retained compact-control construction moves compact dirty fields instead
of spaced windows, at cost O(V*((f log p)^tau+1)). It reserves two front
fields and one back field from existing address coordinates, preserves complete
ranges in every recursive child, restores arbitrary values, and charges
exceptional-address repair at every node. All three movement/layout/guard
proof sources are embedded verbatim in the new patch.
The certificate uses
epsilon = 199/1000, c = 1,
beta = 1/100, zeta = 1/1000, delta = 1/10000,
C1 = 4961/1000,
lambda = 1-293/10^11,
lambda' = 1-29/10^10,
kappa = 2^-31.
The internal, leaf and reservation exponents are
chi = tau+(1-beta)*max(sigma-tau,0) = tau,
leaf = sigma+beta*(1-sigma),
reserve = max(1-c,0) = 0.
All required comparisons are strict. The seven assembly margins have minimum
G = g3 = 5771/10^13 = 5.771e-10 > 2^-31.
The explicit new scalar-operation count fits the generalized guard's node
charge E=64*(W_c+m_c+1)^3. The guard still has
C1=5-4*beta+zeta, and epsilon*C1=987239/1000000<1.
Reserved-axis processing costs O(V log p) for c=1.
The old quadratic restriction from K^tau is absent. With the retained
certified bit exponent and Gaussian assembly inequality, the current scoped
ceiling is kappa<a_b/5=5.92e-10<2^-30. This is not an all-network limitation.
The new complex saving provides numerical headroom for 2^-30 if a stronger
bit construction is supplied; that is not another established witness.
The integration review guide identifies each new obligation and its tests. General arguments are supplied in:
- compressed complex construction;
- movement and deterministic repair;
- reservations, row splitting and recurrence;
- generalized guard.
The new certificate records all four source hashes. The combined patch applies directly to the pinned original and includes the full retained refinements. It updates every complex constant, the exponent ordering, scalar guard charge, final parameters and derived powers. It preserves the legacy wide-slot lemma for the appendix and retains the corrected local exceptional-stream sum.
Finite tests check exact signed scalar maps with independent dirty variables, rectangle partitions, binary residual bases, phase identities, matching, parameter inequalities and source integration. They do not simulate the entire multiplication machine or replace independent proof review. The retained compact-control arguments have the same review dependencies as before.
Completion checks passed: 176 tests, 18 patch-application checks, exact certificate/patch regeneration, and both note and manuscript builds.
Reproduce with make verify and make complex-note. See the
reproduction instructions for applying the patch and
building a manuscript preview without changing the pinned source.
The complex construction is integrated. The next improvement should target the bit finite network, especially methods transferable from the new circuit compression or a new topology. More complex-network tuning alone cannot cross the present bit/Gaussian ceiling. Independent review remains valuable for both the new phase-frame transfer and the retained compact-control tape proof.
The previous joint-frame obstruction remains scoped to its fixed-boundary, grouped-gate model. Older research pages retain their chronology; use this page when interpreting superseded targets and barriers.