DONE: jf0 pairing cost is exactly 19

[RossRichardson]

DONE / HANDOFF / RELEASED — 2026-10-14T22:07:03.773482+00:00; priority revision 4.

The exact raw pairing cost of the pinned eleven-line jf0 configuration is 19, with coordinate ranks (6,6,7). Three fixed unit-triangular minors prove the lower bound for every admissible binary pairing; the identity plus both directions of (2,8), (3,4), (9,10) attains it. This closes item 4 of the independent-check request, with all 2^41 completions covered by a written proof rather than enumeration.

Public artifact: PR2176, exact head 1d31ddb569895377154caeba1f90951057fd2a55. Registered replay, independent row-span oracle and 12 normal/optimized behavioral groups pass locally. Both checkers also pass in read-only relocation. No human/formal-kernel review or new kappa claim; hosted checks are queued. Claim released.

Evidence and limits

The finite source is PR2162 at 113a718265c62aec301c5695f4bfb9c421bef7ab, research/char2-jets/data/jf0.json, SHA256 cd8a8c2436e0a025348af0b52ccb48a4f64535b0ff8df32cbe13da73673266b7. Proof: PROOF.md.

Reproduce: python3.12 -B scripts/research_package.py --package research/jf0-pairing-optimum. The primary checks 51 forced zeros and the full upper matrix; the independent checker builds complete binary row spans of sizes 64,64,128. Controls include exact source binding, forbidden even-but-nonzero rational incidence, missing evidence, changed ranks and actual guard removal. Neither checker imports predecessor code or uses SAT.

Only the raw three-block rank sum is settled. Higher-order jets for jf0, the universal rank-three conjecture, physical COPY/supplier costs and the selected exponent remain unchanged or unaddressed. Next optional bounded check: compare fixed-minor certificates for the already-solved jf1/jf2 with their known costs 12/14; stop if this method is insufficient. No open claim on those.

Credit remains with DreamingOfClouds (Claude Opus 5.5 assistance) for the configuration, prior lower bound and request, and PR1590/PR2111/PR446/PR595 for the model. This successor proof/check package is by Ross Richardson with substantial OpenAI Codex assistance and separately assigned mathematical proof/checker agents, under Apache-2.0.

Final overlap: 421 open PRs and 855 Discussion records at 22:03–22:05 UTC, complete pagination/no warnings; scoped matches were the predecessor/request and this investigation. Search is not novelty proof. Base main and priority revision stayed unchanged.

Original scope and claim

Status: CLAIM, 2026-10-14 21:59 UTC, priority revision 4.

Taking item 4 of DreamingOfClouds independent-check request in #1166 (comment18934590): determine the exact pairing cost of the eleven-line jf0 configuration from PR2162, pinned at 113a718265c62aec301c5695f4bfb9c421bef7ab.

Object: every binary 11x11 pairing B with unit diagonal and off-diagonal support only on rational incidences P_i dot Q_j=0; objective sum of the three F2 coordinate-block ranks. Method: a universal fixed-minor lower certificate, plus an explicit upper witness and separately implemented exact checker. Initial inspection suggests lower bound 19 from minors of sizes 6,6,7; this is still being independently checked. No SAT result is needed for that proposed lower bound.

Base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. This is an explicitly recorded scope change from the portable-replay/verifier-engineering draw (nonce 05def5c4e1ed792501eda6cba1f2a576) to a live mathematical handoff. Fresh all-open-PR/discussion snapshot plus targeted jf0 search found the source request, not another claimed exact-cost audit; search is not novelty proof.

Expected artifact: dependency-free source-pinned certificate package, proof, failure controls and focused PR. Stop after one bounded session with a certified interval if an attaining witness is not found. Local-only until published. No physical supplier, general rank-three theorem or new kappa claim.

Credit: DreamingOfClouds with Claude Opus 5.5 for jf0 and the prior lower bound/request; the #1590/#2111 decoder framework remains inherited. This audit is by Ross Richardson with substantial OpenAI Codex assistance, including mathematical specialist checks.

Claim expires 2026-10-14 23:59 UTC.