[jeremykothe2]

Summary

Conditional κ = 0.001614202339036103. This is +1.479e-6 over PR600 (0.001612722852614221) and +1.481e-6 over PR596. The conservative model gives 0.001614202336182603.

This PR extends the hyperplane-end construction of PR591/PR592/PR596 from 38 to 46 hyperplane-ended helpers per provider word (ck, atm3 and jp8). The 8 new helpers per word (registers 496, 497, 520, 521, 544, 545, 568 and 569) each have one cleanup gate h -= p. Their partner p has one earlier cleanup gate x -= p that only reads p. Since neither gate writes p and h ≠ x, the two gates commute exactly (the cross term is [p = h]·E_xp = 0). So h -= p can run first, at the hyperplane join U, and h ends at U (width 8 → 7, local profile {1:+2, 2:−1, 3:+1, 4:−1} per helper). The previous builder accepted only helpers whose cleanup gate was the first on its registers. That rule was stricter than the Lean hyperplane-end theorem (PR593) requires.

Dispatch: ck ×45, atm3 ×21, jp8 ×6, all with 46 hyperplane-ended helpers. The literal owner map comes from a RINS MIP around the LP vertex and sits within 9.4e-8 of the LP upper bound for this menu (κ ≤ 0.0016142960).

Soundness. No verifier rule changes; only the constructor's admissibility rule does (code/build_hpe.py, now a commutation test).

• The 46 helpers use the same 3 (E, U) pairs that PR593 proves in Lean with no (N) hypothesis (hpe_word_exact); check_hpe_pairs.py passes on every word.
• The audit recomputes every paid climb and asserts exact equality with the profile, so the reordering can't hide a cost.
• The proof note PROOF-COMMUTING-PREFIX.md ships in the package. An independent review found the rule sound, with control-hygiene fixes, all applied. Its final check on the exact package code passed every strict global step.

Controls. Each word's hyperplane_end step runs 21 controls, all of which must behave as stated:

• a partner gate that writes p (or scales it) is rejected by the commutation assert, with a pinned message;
• each of the 8 real new helpers with its skipped x -= p flipped to p -= x is rejected;
• removing the 8 partner U→FULL climb charges is rejected;
• plus the 9 inherited raw-word controls and the existing one-gate-rule controls.

How it was found

• A census of every cleanup gate on PR596's words. PR599's multi-gate and cold extensions admit no further helpers there: each failing helper's frame reaches FULL at some cleanup gate. The census did find the 8 commuting-prefix helpers per word.
• An LP screen over {ck, atm3, jp8} × {38, 46 hyperplane-ended helpers} gave κ ≤ 0.0016142960. The owner map comes from a RINS MIP bounded around the crossover vertex, with dispatch fixed at 45/21/6.

Package

research/complex-571-hpem46/ contains 35 files, including the reviewed proof note PROOF-COMMUTING-PREFIX.md. Five sources are pinned externally by manifest and file hashes, and nothing is copied from them:

• PR568 (research/complex-multicold, 71c99ac);
• PR569 (research/larger-gain, 897213a);
• PR571 (research/structural-gain, b7bdc5a);
• PR575 (research/complex-joint-prefix, eac6f7e);
• PR583 (research/kernel-frame-coalescing, 89be768).

The package is fully data-driven. data/SPEC.json describes each provider as a typed chain of build steps (pinned base word, then promote, greedy_kernels, joint_prefix, frame_coalesce, gate_move_coalesce or hyperplane_end, each with its paired omission and coverage audits), plus the dispatch, the owner and plan hashes, and every expected value. The single verify.py and code/ contain no witness constants. They rebuild every provider from the pinned sources, recompute everything, and compare the results with the spec.

Verification

Fetch the pinned source commits first:

git fetch origin pull/568/head:pr568 pull/569/head:pr569 pull/571/head:pr571 pull/575/head:pr575 pull/583/head:pr583
for n in 568:71c99ac935a33bb7b59a1b4a7af8725a939b0b90 569:897213a855b7fb8a1b8b0e552a2f5c42e6c1b326 \
         571:b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3 575:eac6f7e 583:89be768; do git worktree add --detach ../pr${n%%:*} ${n#*:}; done
python3 -B research/complex-571-hpem46/verify.py --work /tmp/571-hpem46 \
  --source multicold=../pr568/research/complex-multicold \
  --source larger_gain=../pr569/research/larger-gain \
  --source structural_gain=../pr571/research/structural-gain \
  --source joint_prefix=../pr575/research/complex-joint-prefix \
  --source frame_coalescing=../pr583/research/kernel-frame-coalescing

Add --check-pins to check only the package and source pins.

verify.py uses only the standard library. It runs:

• the full PR558 replay;
• each provider's build chain, with all of its omission controls (PR568 multi-cut kernels, PR569 promotions, PR575 joint-prefix coverage and rank-five audits);
• the native chain and exact phase edges for all three providers;
• binding, the physical owner audit with its mutants, a fresh invoice, both exact moment engines, the 47 strict outer inequalities for each model, 147 assembly controls, and the phase-timing controls.

Local result (Windows, CPython 3.11.11): the commit was preflighted from a fresh clone first (committed blobs equal the MANIFEST, every file LF, pin check passes). The official run from that clean clone of 529ab7d then gave PASS_MHPE46_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001614202339036103, 49/49 stages exit 0, 458 s, with no reused baseline or locals. The receipt records MANIFEST sha256 1827ee8d…, equal to the committed MANIFEST.

GitHub CI has not run, and I make no claim about it.

Credits

• chafreaky: PR583 (frame coalescences), PR586 (portable identity checks and controls, and an independent macOS/Linux replay of PR584), PR579, PR577, PR572 and PR551.
• jon314159: PR575 (the joint prefix in all calls) and PR567.
• DominikScholz: PR571 (the joint prefix) and PR569 (entrance promotions and their constructor).
• jeremykothe2: PR600, PR596, PR593, PR592, PR591, PR588, PR584, PR576, PR578 and PR574.
• eumemic: PR564, PR561, PR562, PR558, PR550, PR543, PR507.
• rohanarun: PR559.
• Dugongue: PR552 and PR514.
• icekylinx: PR535 and PR531.
• DreamingOfClouds: PR599 (multi-gate and cold hyperplane-end Lean, which prompted the helper census behind this PR) and PR484.
• higherbeing: the open allocator.
• lydakis: PR275.
• Douglas Colkitt / CrocSwap: maintenance.
• The original OpenAI Weighted dual-suffix carriers: conditional κ = 7.9961717358e-5 #109 framework.

AI disclosure and authorship: Claude Opus 5.5 (Anthropic), running in the omp coding harness, did the work for this PR: the commuting-prefix construction rule and its proof note, the controls, the owner solve, the spec-driven package and this description. Jeremy Kothe (jeremykothe2) directed and reviewed it and is submitting it.

Scope

The result is conditional on the inherited all-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape/exact recovery, analytic transfer and the bit H1–H5 assumptions. It is finite exact evidence. It is not an unconditional theorem, a complete Lean proof, or a practical speedup.

[higherbeing]

Independent confirmation of the 46-helper count and of the admissibility rule.

Working from #592's pinned sources before this PR appeared, I reached the same construction independently: a census of the cleanup gates on the ck, atm3 and jp8 words found that #591's "first cleanup gate on both registers" rule excluded exactly 8 entering helpers per word whose partner is only read by an earlier cleanup gate (x -= p), and that two additions sharing a source commute. Ending those helpers as well gives 46 per word on all three providers, with the local paid Φ unchanged to within 1 Φ per call (local profile {1:2534, 2:488, 3:328, 4:184, 5:56, 6:56, 8:8} on ck). My closure-form builder (the chosen gates plus the non-commuting closure of what they pass, run after B at minimal frames) selects the same helpers; the closure is empty here, so the two constructions coincide. The extended words pass #592's five local admission stages and its raw-word mutation controls unchanged.

Owner-map side, as a cross-check of your LP bound: on #592's dispatch (ck × 53, atm3 × 19) the HiGHS LP ceiling on idle remainders is 42,321.7 Φ for the 38-helper menu (your #592/#596 maps attain it within 37 Φ) and 41,862.3 Φ for the 46-helper menu; an integral map from a restricted-pattern MIP with lazy cross-time Hall cuts reaches 41,890 Φ (remainders {3:197, 25:1, 48:1986}) and κ = 0.001613569610580215 through #592's unchanged global stages. Your 45/21/6 dispatch is better; I did not re-optimise the dispatch.

I am not opening a PR for this since it duplicates #601. Prepared by higherbeing with Claude Code assistance.