κ = 8.01083628465007e-4: #346's w3 bit word with Sussman's Lean-checked E8 unit as the complex supplier (+0.96 % over #350)

[DaysSky]

Conditional κ = 801083628465007/10¹⁸ ≈ 8.01083628465007e-4: +0.96 % over #350 (7.93469326753735e-4), +1.07 % over #346 (7.92580093369946e-4), +4.82 % over #315. The bit side binds; the complex supplier is 9.3 % above it.

This PR adds one self-contained package, research/w3-p10b-e8-complex/, with its own workflow. No existing file changes except one .gitattributes line (-text -whitespace, as #186/#210/#348 do for byte-pinned packages).

Change and mathematical scope

Only the complex supplier changes.

• Every complex program so far in this repository has been a paired-cube program: the star scatter with h centres of rank h − 2.
• This PR uses Jacob Sussman's E8 unit instead: gcert1-e8-r783 from jacobalansussman/wht-power-saving-lean at 9c94857, published 10 October.
• It is a gcert/1 program on the E8 label family: h = 9, v = 120, R = 783, m = 45, eight retained totals at the full frame, and an explicit scatter table.
• It is the certificate behind his kernel-checked theorem wht_main_block_B2Ge8x (∃ solve W, WHTProgram solve W ∧ WHTTimeBoundsAt (1 - 8762479/10^10) W). His README notes that this repository's complex side is that quantity.
• Its five-stage B₂ histogram, computed by the complex guard here, equals the one his gxrate reports (tally 56,715, deficit 120).

side	supplier	coarse saving
bit	#346's word, byte-identical (73 files pinned by git blob at 11b4de5)	c = 32069035133443/(4·10¹⁶) ≈ 8.01725878e-4
complex	Sussman's E8 unit	b = 876248285600677/10¹⁸ ≈ 8.76248286e-4

κ. #315's outer assembly (as in #346) runs with c capped by (1 − 10⁻⁹)·b, which does not bind here. It takes three bootstrap steps and η = 10⁻¹². All 47 strict constraints are positive, and the adjacent 10⁻¹⁸ κ is rejected.

What is new in the checks. #315's portable complex checks, as #346 ported them, assumed the star scatter and h centres of rank h − 2. They now read these from the certificate, the way gx.scat_row does (code/complex/code/scatter.py):

• the scatter is a table or the star rule;
• there may be any number of retained totals, up to h reserved centre slots;
• each centre child has its total's frame rank;
• final climbs are exactly the helpers not already at the full frame, and no x or y role (783 − 8 = 775 for E8).

On #346's own p = 10 program, the generalized checks reproduce every #346 pin. They are byte-identical to the original checks on both scalar schedules, both splice programs, the primitive expansions, the ledger, the labels and the precision guard (code/complex/regress_pr346.py).

Fit with the finite bridge. The precision margins are wider than at p = 10:

	E8	#346 (p = 10)	requirement
external row coefficient	11,119	15,125	< 20,161
half-shrink	40 < 45	84 < 100	2·max child < m
induction gap	49·B	115·B	≥ 1·B

Retained hypotheses and open obligations.

• Bit side. All of κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346's obligations are retained unchanged: Conditional κ = 0.000752893499605334868002344: source-bound w3 word and complete finite admission (+0.1855% over #309) #310's native downstream chain is not ported to p = 10; Conditional κ = 7.64230861320245e-4: the paired-cube bit word at cube size p = 10 (h = 20, m = 100), with a new centre-sharing complex supplier (+1.21% over #314) #315's scalar/prime/finite stages are replaced by the official cohort checkers; the additive row constants 9909 + 252 are kept; every inherited Conditional κ = 7.64230861320245e-4: the paired-cube bit word at cube size p = 10 (h = 20, m = 100), with a new centre-sharing complex supplier (+1.21% over #314) #315/Conditional κ = 7.696840393833340e-4: a stronger p = 10 bit word — re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word) #325 interface remains an assumption.
• Complex side.
  • The generalized portable checks are new code, regression-checked against κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346 as above.
  • A stronger bit supplier: fixed-coordinate and face-diagonal bit local circuit on PR168 v4 (effective bit saving 6.7734e-4) #200's complete checker and Source-assisted v4 complex word with PR189's bit supplier: conditional κ = 6.674324e-4 #194's contract work on the Compose the v4 source-assisted complex word with the PR200 bit supplier: conditional κ = 6.768823e-4 #202-tree producer format, so they are not run on E8. In their place stand Sussman's Lean theorem (checked in his repository, not rebuilt here), his gx.check1, his gxcore mirror and his independent replay, and the byte-for-byte regeneration of the theorem's Lean data from this certificate.
• This is a conditional finite construction, not a formal verification of the multiplication theorem.

Because the bit side binds, a bit-side gain on this word raises κ until it reaches about 8.76e-4.

Validation

python -m pip install -r research/w3-p10b-e8-complex/requirements.txt    # numpy==2.5.3 mpmath==1.3.0; also g++ and Boost headers
bash research/w3-p10b-e8-complex/verify.sh /tmp/w3-p10b-e8-verify          # ~5 min

What it runs:

0. The manifest, and the κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346 provenance: git blob ids of the 73 inherited files.
1. The base snapshot (Conditional κ = 7.696840393833340e-4: a stronger p = 10 bit word — re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word) #325 p10b) is hash-checked, and its root equals Conditional κ = 7.696840393833340e-4: a stronger p = 10 bit word — re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word) #325's.
2. Design T and 3. twin condensation (Conditional κ = 0.000752893499605334868002344: source-bound w3 word and complete finite admission (+0.1855% over #309) #310, ported in κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346) rebuild the final word to the shipped hash. Both run with κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346's ported verifier: legality, all F₂ columns, nondegeneracy.
3. Conditional κ = 7.14026746429965·10⁻⁴ on #249's word: 890 kernel families, #263/#270 retimings, #273's target-prefix squares and 126 cleanup sandwiches (#271), composed (+0.42% over #259; above #271/#275) #266's official legality and five-stage columns checkers; exact nondegeneracy and prime witnesses on the 320 new frames; the width-100 bank tiling.
4. The complex supplier:
   • the generalized complex guard: gx.check1 with the exact scalar identity, gxcore, flipped-sign controls, labels, scalar words and lifetimes, the five-window splice with all mutation controls, and the precision guard;
   • the Lean binding: Sussman's generators, vendored unchanged, regenerate from the vendored certificate the 24 Lean modules and the comparator configuration of wht_main_block_B2Ge8x, all byte-identical to his files (no Lean run here);
   • his stand-alone replay.py, which shares no code with gx, accepts the certificate at 8762479;
   • exact b from both rational moment engines with the 10⁻¹⁶ fallback, with the adjacent grid point excluded.
5. Exact c, then the outer assembly: 47 strict constraints, and the adjacent κ rejected.

Local result (macOS, Python 3.12.13 and 3.14.8, numpy 2.5.3, mpmath 1.3.0, Apple clang, Boost 1.86 headers):

$ bash research/w3-p10b-e8-complex/verify.sh /tmp/w3-p10b-e8-verify        (identical on 3.12.13 and 3.14.8; compiler warnings omitted)
== 0. package manifest and PR #346 provenance
   all files match MANIFEST.sha256
   73 files byte-identical to PR #346 at 11b4de5 (git blob ids); 11 edited, 32 not carried over
== 1. base word (PR #325 p10b, exported): records hash OK
   base bit root 0.0007702769095630427
== 2. Design T (w3, ported to h = 20)
[legality] violations=0 final_mismatch=0 copies=20 erases=20 used_frames=11762 degenerate=0
[F2] X_not_restored=0 H_not_restored=0 resid_sigma0=0 resid_other=0
== 3. twin condensation
[legality] violations=0 final_mismatch=0 copies=20 erases=20 used_frames=12082 degenerate=0
[F2] X_not_restored=0 H_not_restored=0 resid_sigma0=0 resid_other=0
   final records hash OK (c6a9311acfcf85f4a5775ed0187e31f84531614bb08434ef887ae1e63dda99c4)
   rebuilt word equals the shipped word
== 4. official PR #266 checkers (h, v, R and the copy count generalized), exact frames, primes, banks
PASS pairs 0 ADD 358128 mass 169560 COPY24
   five-stage formal columns PASS
PASS prime witnesses for 320 new frames; max determinant bits 6 ; primes [2, 3]
PASS exact width-100 tiling with 60 replicas: (((19, 19, 19, 19, 4, 4, 4, 4, 4, 4), 7200), ((4, ..., 4), 1152), ((20, 20, 20, 20, 20), 71280))
== 5. complex supplier (Sussman's E8 unit): gx.check1 + gxcore, labels, scalar words, splice, precision guard, Lean binding, exact b
guard: PASS_FRESH_COMPLEX_LABEL_SCALAR_SPLICE_PRECISION | gx.check1: ACCEPTED (labels, bl | rows 11119 < 20161
Lean binding: RESULT: REPRODUCED (25 repository files reproduced byte for byte, 0 different, 3 generated files not in the repository) (wht_main_block_B2Ge8x modules regenerated from this certificate)
stand-alone replay: REPLAY ACCEPTED: R=783 W=1263 D=120 cst=72 N=9039 figure=8762479  E8 family: True  (0.3 s)
PASS complex coarse saving b = 876248285600677/1000000000000000000 0.000876248285600677 (two engines, 10^-16 fallback, adjacent grid point excluded)
== 6. bit coarse saving and outer assembly (PR #315 engines)
bit coarse c = 32069035133443/40000000000000000 0.000801725878336075 (two engines + 1e-16 fallback, adjacent grid excluded)
complex b = 876248285600677/1000000000000000000 0.000876248285600677 | binding: bit
KAPPA = 801083628465007/1000000000000000000 = 8.010836284650e-04 | 47 strict constraints positive, adjacent grid point rejected
PASS conditional kappa = 801083628465007/1000000000000000000 = 0.000801083628465007

$ python3 -B research/w3-p10b-e8-complex/code/complex/regress_pr346.py <PR #346>/research/w3-p10b-complex-p10
PASS: on PR #346's p = 10 program the generalized complex checks reproduce every pin and the original scalar schedules, splice programs, primitive expansions, ledger, labels and precision guard byte for byte

Finite certificate checks only; the proof obligations listed above remain open.

Credits and AI disclosure

• Complex unit, Lean theorem, generators and replay: Jacob Sussman (wht-power-saving-lean, Apache-2.0; his LICENSE and NOTICE are vendored). His unit uses devices from this repository: jamesyc Birth-read slot recycling: conditional kappa 1.1038332094346e-4 #124 and eumemic Late compensation and joint frame refinement: conditional κ = 4.24830828577e-4 #143 (slot reuse with a compensating read), Chafik Boukhalfa A stronger bit supplier: fixed-coordinate and face-diagonal bit local circuit on PR168 v4 (effective bit saving 6.7734e-4) #200/A stronger complex supplier: PR200's reuse pairing on the source-assisted v4 word, complex saving 7.0991·10⁻⁴ (+1.28% over #194; no new κ, bit binds) #233 (late pairing), and icekylinx Source-assisted common-frame compression for conditional kappa = 6.566436e-4 #184, carried in ikeboy's Source-assisted complex word on PR168 v4 modules: conditional κ = 6.626307e-4 #191/Pair donors to avoid parity erasure on the source-assisted v4 word: conditional κ = 6.647872e-4 #193 (in-place pair).
• Bit word and package base: LJH-217 (κ = 7.92580093369946e-4: w3 cube layer on #325's p10b word with a stronger p = 10 complex supplier #346), on DreamingOfClouds' Conditional κ = 7.696840393833340e-4: a stronger p = 10 bit word — re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word) #325/Conditional κ = 7.64230861320245e-4: the paired-cube bit word at cube size p = 10 (h = 20, m = 100), with a new centre-sharing complex supplier (+1.21% over #314) #315 and utcorvusvolat-dotcom's w3 work (Conditional κ = 0.000752893499605334868002344: source-bound w3 word and complete finite admission (+0.1855% over #309) #310).
• Official checkers: Conditional κ = 7.14026746429965·10⁻⁴ on #249's word: 890 kernel families, #263/#270 retimings, #273's target-prefix squares and 126 cleanup sandwiches (#271), composed (+0.42% over #259; above #271/#275) #266.
• Complex checks: the Conditional κ = 7.64230861320245e-4: the paired-cube bit word at cube size p = 10 (h = 20, m = 100), with a new centre-sharing complex supplier (+1.21% over #314) #315/A stronger complex supplier: compile-cost-annealed complex modules, five-stage complex saving 7635/10⁷ (+1.17% over #233; no new κ) #304/The source-assisted complex word of #233 as one explicit numbered program (gcert/1): reference-checked, 7.547361·10⁻⁴ in the Lean-checked five-stage layout (no new κ) #256/A stronger complex supplier: PR200's reuse pairing on the source-assisted v4 word, complex saving 7.0991·10⁻⁴ (+1.28% over #194; no new κ, bit binds) #233/Compose the v4 source-assisted complex word with the PR200 bit supplier: conditional κ = 6.768823e-4 #202/A stronger bit supplier: fixed-coordinate and face-diagonal bit local circuit on PR168 v4 (effective bit saving 6.7734e-4) #200/Source-assisted v4 complex word with PR189's bit supplier: conditional κ = 6.674324e-4 #194/Source-assisted common-frame compression for conditional kappa = 6.566436e-4 #184 lineage.

See NOTICE.md.

The generalization, the Lean binding and the package were prepared by DaysSky, assisted with Claude.

[ahrazzle]

Independent empty-directory Lean reproduction of the E8x ceiling (new hardware) — audit of the quantity that now caps κ

I rebuilt the fourth-revision Lean tree from an empty directory on new hardware (Apple M1 Max, 10 cores, 64 GB, macOS 27.0.1, Lean v4.34.1, Python 3.14.6 — neither of Sussman's two machines) and kernel-checked the theorems behind this PR's complex supplier, closing the "checked in his repository, not rebuilt here" caveat from this PR's description and VERIFY.md §10.7 point 4.

Pinned inputs. wht-power-saving-lean @ 9c94857 ("Fourth result"); certificate gcert1-e8-r783 gz sha256 4b92f00f…, canonical sha256 3594f19c… — byte-identical to the copy vendored in this PR at inputs/e8/tools/certificate/. toolchain leanprover/lean4:v4.34.1, mathlib rev d13f23f7… per lake-manifest.

What I ran and got (all matching the protocol's expected outputs exactly):

1. Byte-exact regeneration (Python, generators unchanged): gx regen_check_e8.py → 25 files REPRODUCED; fourier regen_check_e8.py → 14 files REPRODUCED.
2. Empty-directory build (fresh clone, .lake empty at start; lake update + lake build): base modules exit 0; then the 24 E8 certificate modules and the 15 FourierE8 modules each Build completed successfully with 0 error lines; sorry discipline exact (5 lines, all challenge-file declarations, as VERIFY.md 10.4 records). lake build --no-build over the built roots: All targets up-to-date (9236 jobs).
3. Axiom audit: wht_main_block_B2Ge8x, transform_mainE8, convolution_mainE8 all [propext, Classical.choice, Quot.sound] (the permitted axioms); hillsE8_program also clean.
4. tools/Compare.lean (certificate-vs-Lean-term): all three theorems OK — same kernel term, identical dependencies, permitted axioms.
5. Official comparator (leanprover/comparator @ d03acab, lean4export @ 076e8e5, macOS seatbelt sandbox as the linux landrun stand-in): both E8 configs — B2Ge8x.json and UniformFourierE8.json — "Lean default kernel accepts the solution / Your solution is okay!", exit 0, 171 replayed / 0 built.
6. §10.4 Python checkers on the certificate: refcheck, gxdry, replay all accept at 8762479 (evaluated 8762482 holds / 8762483 fails).
7. Negative controls (§10.5 group 1, seven mutations M1–M7, including the M4 total-frame mutation Sussman flags as the one Python-only gap): all seven refused by all three checkers, intact copy accepted by all three.

Conclusion for this PR's ledger: the 8762479/10^10 ceiling — which caps every future κ at ≈8.76248e-4 on this supplier — is now kernel-checked on an empty directory on third hardware, through Sussman's own official comparator path, with the certificate pinned byte-for-byte to the copy vendored here. Nothing in the E8x pipeline needed patching to reproduce; the reproduction is clean.

Two minor observations (not defects, for the record):

• tools/fourier/regen_check_e8.py silently treats a stray CLI argument (e.g. an accidentally-passed --keep, which belongs to the gx script) as a seam module name, producing a misleading 1 DIFFERENT line. Zero-argument invocation (as VERIFY.md specifies) reproduces 14/14. A usage guard would help future hands.
• The macOS landrun shim (sandbox-exec seatbelt profile) works correctly as the linux landrun stand-in for the comparator's re-execution step — worth stating explicitly for other Apple-silicon reproducers.

Automated posting by agentic team with human oversight.

[ahrazzle]

Bit-side headroom characterization (the binding side) — full #352 verify reproduced on new hardware

Two things: (a) I reproduced this PR's entire verify.sh end-to-end on third hardware (Apple M1 Max, GCC 16.2.0 via shim for bits/stdc++.h, Boost 1.92, Python 3.14 + numpy/mpmath — all 7 stages PASS, κ = 8.010836284650e-4), and (b) a sensitivity analysis of the now-binding bit side that maps exactly where the remaining 9.3% headroom lives and why it is not reachable by retuning.

Reproduction. Fresh checkout of this PR's head, bash research/w3-p10b-e8-complex/verify.sh /tmp/...:

• manifest + provenance: 73 files byte-identical to PR #346 at 11b4de5
• base word records hash OK; base bit root 7.70276909563042e-4
• Design T: BHcount12: 120, 120 cubes, 480 freed ids, 7200 forward ADDs removed; legality/F2 clean
• twin condensation: final records hash OK, rebuilt word == shipped word
• official #266 checkers: PASS pairs 0 ADD 358128 mass 169560 COPY24, five-stage columns PASS, prime witnesses PASS (max det 6 bits, primes {2,3}), exact width-100 tiling PASS (60 replicas)
• complex supplier: gx.check1 ACCEPTED, Lean binding REPRODUCED (25 files, 0 different), stand-alone replay ACCEPTED ... figure=8762479, b = 876248285600677/10^18 (two engines)
• assembly: c = 32069035133443/4e16 (two engines + 1e-16 fallback), KAPPA = 801083628465007/10^18, 47 strict constraints positive, adjacent grid rejected

Headroom analysis (using this package's own exact moment.certify engine, profile read from the shipped word's kappa.json):

The bit profile is low-rank-heavy by design: 75.2% of the 2,845,200 normalized calls sit at ranks 1–3 (rank 1 alone: 44.1%), mid ranks 4–18 hold 22.4%, high ranks (19, 38, 42) only 2.4%. That shape is what makes c large. Measured response surface:

1. Reducing resid with the profile held fixed collapses c (−24% for resid −100). The moment balance requires resid and the profile to move together; W = 4v + resid/h enters the denominator.
2. Mass-conserving rank shifts toward high ranks lower c monotonically (−0.09% per 1000 calls moved 1→19, −2.05% for moving all 20,920 rank-1 calls to 19). The root rewards the low-rank concentration.
3. Therefore c is word-intrinsic — a local optimum of this word's structure class. The census {0:480, 4:1200, 19:480, 20:5940} is not tunable slack: the 480 rank-0 entries are the freed Design-T helpers (deleted, not banked), the 1200 rank-4 entries are addcomp.py's structural comp-read pairs, and the 480 rank-19 are the twin-condensation leftovers.

What raised c so far (and what would raise it further): each w3 step lowered resid by freeing helpers at the same profile shape — base 7.7028e-4 → Design T 8.0034e-4 (480 freed) → twin 8.0173e-4 (320 line frames). Design T's own output says unused ids 480 with BHcount12: 120 — the eligible free pool is exhausted for this base word. The remaining 9.3% to the complex cap (8.7625e-4) therefore needs either (i) a new base word with a better initial-frame dim distribution (a fresh PR #325 derivative with more dim-19/20 initial frames, in the spirit of #340's cube-orientation work), or (ii) a stronger complex supplier above 8.7625e-4 (Sussman's next unit).

Happy to share the full verify log or the analysis script (headroom_final.py) as a PR if useful. No changes to this PR's code — reproduction + analysis only.

Automated posting by agentic team with human oversight.

[Mister-Meeseeks]

Thank you @DaysSky. This contribution is now retained on main in the scoped 100-PR review and contributor credits.

Contribution: Integration of Sussman's E8 complex unit with the w3 bit word.

Review and limits: The local Lean unit does not formalize the multiplication assembly. Finite guard/pricing evidence and inherited native-interface qualifications remain explicit.

The complete original source, notices and relevant execution evidence are retained through the pinned source archive. The review distinguishes fresh local runs, source-bound historical Linux CI and prior exact-head review; it does not claim 100 fresh full mathematical audits. Closing this historical PR as reconciled. This preserves parallel and cumulative credit without replacing the selected frontier or promoting priced research targets to completed constructions.

Reviewed head: 04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2. Publication: 4040a0f46d67b41c36a472a7cd4af791fd4c36cc.