Conditional κ = 0.001612722852614221: improved owner map for the PR596 hyperplane-ended witness

[jeremykothe2]

Summary

Conditional κ = 0.001612722852614221. This is +1.48e-9 over our PR596 (0.0016127213726553). The conservative model gives 0.001612722849763179.

This PR has the same construction, providers, dispatch (ck ×53, atm3 ×19) and verifier as PR596. Only the literal owner map changes: a 2-swap ejection chain on idle remainders turns {1:1,3:281,12:1} into {1:2,3:279,5:1,12:1}. The concave moment cost favours uneven holes. The package also ships the declarative inputs data/WITNESS.json (inputs only) and data/EXPECTED.json (expected values, generated by recomputation), plus a definition-first README.md. data/cand.json is the search-side candidate description; its warm-start owner map is shipped as data/search/WARM-OWNERS.json.gz (a search input that the verifiers do not read).

This PR has the same construction, providers, build steps and verifier as PR591. Only the dispatch and the literal owner map change: ck ×53 and atm3 ×19 calls, all with hyperplane-ended helpers (PR591 used ck ×66, atm3 ×5, jp8 ×1). The LP upper bound for this menu is κ ≤ 0.0016127416, and this map is within 2.2e-8 of it.

This PR keeps PR588's construction (PR582's three providers with all eight frame coalescences) and adds hyperplane-ended helpers. In each of the three providers (here ck and atm3), 38 entering width-8 helpers per call have exactly one cleanup gate h -= p, where p is a partner whose final frame and h's final frame span a hyperplane U (dim 8). That gate commutes to the end of part B at frame U. The helper then ends at U instead of FULL, so its residual width drops from 8 to 7: local profile {1:+3, 2:−2} per helper, mass-neutral, deficit unchanged at 2560. The width-7 helpers then pair exactly with width-9 helpers in rank-16 owner slots, filling forced rank-3 holes.

Why this is legitimate. Ending at FULL is a convention of the inherited code, not a proof obligation:

• Lean Lemma A's hypothesis (F) is stated on actual extended labels and never names FULL.
• Lemma C and Lemma G need only invertible common labels.
• The nested-children lemma gives T_U T_E^{-1} = L(C_[|U|−|E|]⊗I)R with rank-zero L and R.

The full argument and every changed assertion are in PROOF-HYPERPLANE-END.md. An independent review found one real issue: the pre-wrapper recipe was ambiguous at three entrances shared by FULL-ended and U-ended helpers. It is fixed, and both wrappers are now keyed by (start, final).

Verifier changes.

• Helper width is computed as |final| − |E| at all 9 global sites that previously hard-coded 9 − |E|.
• A per-site revert control puts back the old formula at each site, and each one must fail. All 9 are rejected, the invoice site through a mandatory terminal-codimension check.
• The new typed build step hyperplane_end checks commutation, exact scalar replay, the wrapped product L^{-1}T_U T_E^{-1}R^{-1} = C_[7]⊗I (global phase included), widths, and cleanup. It carries replay, wrapper and raw-word negative controls.

The literal owner map (all-HPE dispatch) was found by an RINS-bounded MIP around the pattern LP vertex, within 2e-5 objective units of the LP bound. The paid profile is the global profile recorded in data/EXPECTED.json.

How it was found

• An LP/MILP screen over free dispatch of {ck, atm3, jp8, e8} gave an upper bound of 0.0016015477. The integer solution chose 66/5/1.
• The owner map comes from an exact-window MILP with the dispatch fixed, warm-started from PR571's owner map. Every solution of that model expands literally through Kőnig colouring, and HiGHS solved it to optimality.

Package

research/complex-571-hpeq6/ contains 33 files. 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

PR568, PR569, PR571 and PR575 are not merged, so fetch their pinned 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-hpeq6/verify.py --work /tmp/571-hpeq6 \
  --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 (31 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 (byte-identical to the generated package, committed blobs equal its MANIFEST, pin check passes, spec.py check OK). The official run from that clean clone then gave PASS_HPEQ6_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001612722852614221, 32/32 stages exit 0, 323 s, with no reused baseline or locals. The receipt records MANIFEST sha256 cac3d56d…, 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: PR596, 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: 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 hyperplane-end construction and proof, 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.