Conditional κ = 0.001671387264390146: all eight mutable-leaver all-K cells, U8 hybrids and frame re-optimisation on PR799's word

[jeremykothe2]

Summary

Conditional κ = 0.001671387264390146 (conservative 0.001671387261540186). That is +9.43×10⁻⁶ over the merged #942 (0.001661960547713947) and +7.15×10⁻⁶ over #1004. The complex side binds; PR589's bit supplier is unchanged.

Change: mutable-leaver all-K cells. In the no-triangle word, all eight all-K delivery cells (01±, 23±, 45±, 67±) are replaced by a 21-gate circuit found by layered CP-SAT. It has no helper and uses leaver sources (registers with no later reads) as mutable scratch, which are restored before their next use. Each cell changes the raw paid profile by exactly −30H1+6H2+6H3. y−y sources are S6-relabelled away from targets carrying port-entrance dirt. On top of that, the PR799 layers are re-applied through the signed builders (NP/p6n, promo, jx), along with six of the eight #869 triangle-hybrid instances (two use helpers the cells remove). Finally, a pinned frame re-optimisation is applied; it changes frame annotations only.

Construction drivers: construction/leaver/ (reproduce_leaver.py --id k8 for the cells, then reproduce_leaver_chain.py for the stacked chain, with every intermediate word pinned in CHAIN-PINS-k8.json). All verifier code is the reviewed set from research/gauge44-barch (#869). Data was re-admitted with the R=480 SPEC through discovery, freeze_spec and the strict replay.

Controls: per-cell mutants M1–M6, rejected by both audit_local and the native audit. The per-end layer controls pass 95/95 on the p6n, promo, jx and hybrid words. On the frame-re-optimised word they run with signed not-applicable pins (LEC v2: identity mutants proven by sha equality, substitute sites rejected by both checkers), and in addition, because that word's scalar program, starts and helper_final are identical to the hybrid word's. There, the three frame-builder pin controls, the 6-mutant frame receipt and the native frame-chain audit apply (see PROOF-NOTE-LEAVER.md).

Independent review: SOUND. Separate reviewers covered the cells and leaver chain, the frame step, the hybrids on the new base, and the layer-end control variant. The committed tree was then checked byte-for-byte against the reviewed artifacts, and a clean leaver-chain run passed in check mode against the pins.

Verification

From a fresh clone of commit 779e80a, with no reused artifacts (Windows, CPython 3.11.11), running the README's clean-clone commands in order:

• verify_manifest.py: PASS, 169 files
• reproduce.py, reproduce_notri.py, reproduce_np.py, reproduce_p6n.py, reproduce_promo.py, reproduce_sw4.py, reproduce_frames.py, reproduce_jx.py, reproduce_leaver.py --id k8: all PASS
• reproduce_leaver_chain.py --id k8: an independent reviewer's clean run passed in check mode against CHAIN-PINS-k8 (final word db2c7cfb, all five LEC runs reject 95). A fresh-clone run of this stage, then audit_local and verify_global, will be posted as a comment when it finishes.
• Clean rebuild in check mode from a tree copy: chain to db2c7cfb, then audit_local PASS, then verify_global.py on the rebuilt locals: PASS_GAUGE44_STRICT_GLOBAL_REPLAY 0.001671387264390146

Scope

Conditional on PR645's premises and PR589's bit-supplier assumptions. This is a finite exact construction; no unconditional theorem or Lean certification is claimed.

Credits

• NewBArch's triangle-hybrid B delivery (Conditional κ = 0.001661948695165034: eight triangle-hybrid B deliveries in block 0 on PR799's word #869), and the PR799 lineage: chafreaky (Conditional κ = 0.001661202643272239: eight B-frame coalescences after SW4 #741, Conditional κ = 0.001660339298410333: four entrance promotions and 72 cold ends #685, Conditional κ = 0.001654269575689572: six more layered cold ends and full-48 packing #660 frames, owner map and packing), icekylinx (Gauge44 factory and whole-family assignment for conditional κ = 0.001649483702558979 #645 gauge44 construction and verifier), and the PR589 bit supplier. Every upstream contributor credited in Gauge44 factory and whole-family assignment for conditional κ = 0.001649483702558979 #645 retains credit.

Prepared with Claude Code (Anthropic).

[jeremykothe2]

Correction to the "Change" section. The sentence "Each cell changes the raw paid profile by exactly −30H1+6H2+6H3" is wrong. The measured per-cell change in the raw paid profile is +6H1 − 12H2 + 3H3 − 3H6 (rank mass −27, three helpers removed per cell). The totals are consistent with this: k5 − no-triangle = 5× this delta, and k8 − k5 = 3× this delta. The −30H1+6H2+6H3 figure was the CP-SAT set model's prediction for one cell, not the measured change in the word. The construction, controls, verification and κ (computed from the actual word by the strict replay) are unaffected. Thanks to thakrarsagar's independent audit (#1049) for catching this.

[jeremykothe2]

Correction to my previous comment. The original sentence is not wrong; it lacked its comparator. Measured in the raw word against the direct-triangle (all-K) cell it replaces, each leaver cell changes the profile by exactly −30H1+6H2+6H3. That is a measured value, not only the set model's prediction. Measured against the no-triangle base word, the per-cell change is +6H1 − 12H2 + 3H3 − 3H6 (rank mass −27; k5 − no-triangle = 5×, k8 − k5 = 3×), which is what #1049 reports. Both figures are correct for their stated comparators. κ, the construction and the verification are unaffected.

[jeremykothe2]

Reviewer note on where this claim lives. This branch is stacked on #1004, so it also carries research/gauge44-leaver/ (that is #1004's package, κ 0.001664233607446043). This PR's claim, κ 0.001671387264390146, is the package research/gauge44-leaver8/: its README, RESULT.json, CHAIN-PINS-k8 and verify commands. GitHub's 100-file diff listing may hide gauge44-leaver8/, so browse it via the branch tree. Thanks to thakrarsagar (#1069) for flagging this and for independently certifying the κ.