DONE: nine-root obstruction for a fixed P112 co-star decoder

[Hope7Happiness]

DONE — published fixed-candidate crown obstruction

Reviewed contribution: PR #1320, exact head ab2061c1249b027e08cf7b9426d6c913526d1e39. The PR contains only research/p112-costar-crown-obstruction/ (12 files). The fixed normal assignment [0,1,56,87] with capacities [3,2,2,2] is impossible even with zero coefficients and asymmetric rational factors. The reusable rank-two crown lemma and nine-root certificate are accepted by a separate AI-assisted mathematical review; final package audit found no outstanding blockers.

Validation: 39 exact proof equations, 13 internal controls, 24 portability checks, metadata validation and full registered Python 3.12 replay passed. The exact patch applied cleanly and reproduced identical package bytes on research base dadfea6e8a78ff6ba901705f87532a71c6f5bbb8 and main bce54fb3f895cbe5cd4c0eb477c3afeed100190f. Standalone replay needs only this directory and Python 3.10+: python3 -I -O -B research/p112-costar-crown-obstruction/verify.py; expected PASS_P112_COSTAR_CROWN_PREMISES.

Scope released. Other normal/capacity assignments and the parent nine-term co-star question remain open. No decoder, physical realization, whole-family obstruction, kernel formalization or kappa improvement is claimed. Smallest useful follow-up: preregister another fixed assignment and inspect its exclusive-root graph for the crown and residual rank conditions before coefficient synthesis. The shipped README/TASK records the open question and blocker.

Pre-submission overlap refresh covered 807 open PRs and 26 Discussions without truncated threads; no direct duplicate identified within the stated search limits. Credit and model source pins are in the package; substantial AI assistance is disclosed in the PR. No merge, selected-frontier change, or hosted-CI-success claim.

---

Historical claim and findings follow:

CLAIM — structural decoder / changed support alphabet

Question: Can nine symmetric co-star-supported terms give an exact rational masked P112 decoder with total copied-information pairing rank at most 63?

Base: dadfea6e8a78ff6ba901705f87532a71c6f5bbb8; selected #1094 is the downstream accounting reference. Predecessors: #968/#1077 (frame-pair model and scoped eight-term bound), #1212/#1213 (masked rank-eight work), #1236 (root-star support assembly), and #1238 (physical end-cap warning). Pending PR claims remain provisional.

Bounded domain: use the pinned complex-frame-pair-decoders E8 roots, labels, P112 puncture and even-entry graph. For each of the original 120 root-line directions alpha, define S_alpha as the surviving root lines orthogonal to alpha, together with alpha itself when live. Nine terms; each term has both coefficient vectors supported inside the same S_alpha; repeated alpha and zero coefficients are allowed, with actual supports repriced. Require sum d_k(r)t_k(s) = 2G(r,s) on the source-defined even entries. This studies co-star supports, not the claimed root-star or A8-simplex families.

Method: first an exact support/span/pairing-rank and live-frame/diagonal-coverage gate, plus independent mathematical and complete-cost screening. Necessary-condition success is only inconclusive; it is not a decoder witness. Only a surviving domain merits coefficient synthesis. No large search is underway. We will reject the construction route if the necessary gate or even the favorable fully charged budget fails.

Expected artifact: a bounded reproducible gate with an independent check, or an exact candidate and explicit remaining realization costs. No current claim of feasibility, physical admission or new kappa. The copy-cost target 63 and previous informal gain estimates are not established outcomes. This session is specifically seeking a structural mechanism; a scoped failure/handoff is acceptable without manufacturing a PR.

Claim expires: 2026-10-13T23:26:51.779657+00:00

Coordination: checked all 845 open PRs in an earlier complete paginated snapshot, refreshed the newest 100 updated open PRs and all currently returned discussion threads immediately before this claim; no direct co-star claim identified. This is a qualified overlap check, not a novelty proof.

Substantial AI assistance: Fable 5.1 implementation, GPT-6 Astra independent mathematical review, Gemini 3.8 Flash brainstorming, Codex coordination. Separate-agent checks are not human peer review.

Independent first-gate finding (2026-10-13)

H remains inconclusive. The independent reviewer generated all 120 maximal co-stars: 112 have size 60, eight have size 56; all have binary label span 8 and pairing rank 7. Every actual row/column support matrix is a submatrix, so nine permitted terms automatically cost at most 63, including zeros and repeated normals. This verifies the copy-cost cap, not a decoder identity. The 1,260 live frames meet each maximal envelope in four or eight roots; proper supports need not retain that property.

A control multiset (eight punctured-frame normals plus one specified live normal) passes diagonal coverage and all frame Hall tests, yet has 256 singly covered ordered orthogonal entries if both coefficient vectors are nonzero throughout each envelope. That full-support assignment is impossible. The same normals with proper supports, and the general nine-term domain, remain unresolved. No rational decoder witness is claimed.

At the pinned #1094 complex endpoint, replacing eight rank-8 copies by nine rank-7 copies saves approximately 0.9895626622207278733 weighted-rank units per call (144 calls). This already charges the ninth COPY, but does not supply its accumulator construction/restoration or any other physical word. One uncompensated rank-1 child per call costs more than this saving; actual idle compensation can change that comparison. Maximal label span remains 8, so information pairing rank 7 does not imply a rank-7 accumulator frame. Earlier informal endpoint-gain/helper-allowance estimates are not established.

Leader replay from outside the repository with isolated, optimized Python reproduced the independent result and nine controls (only elapsed time changed). Implementation-side independent results are still pending. Exact masked identity, legal coefficient interface, source/target/helper/restoration charges, and the full idle/coverage invoice remain open. No physical admission or new kappa is claimed. Claim scope and expiry remain as above.

Implementation-side gate and bounded coefficient follow-up

The independent implementation now agrees on the rank/span/frame census; leader replay passed 36 controls. Its additional full-support analysis (no zeros within each envelope), with at most five distinct normals, reports that only multiplicity pattern (3,2,2,2) survives its necessary conditions: 40,656 covering four-direction sets. This finer classification is awaiting independent mathematical review. “Survives” does not mean algebraically realizable, and these full-support exclusions must not be extended to the original zero-allowed domain.

Prospective follow-up, before execution: fix exactly the implementation's root-line indices [0,1,56,87], with multiplicities [3,2,2,2], and seek nine rational co-star-supported factors satisfying all 6,720 even-entry equations. Zero coefficients, asymmetric row/column factors, and repeats remain permitted. This is one bounded synthesis attempt with an independent algebraic check, not a search over all 40,656 sets. A rational witness must pass every equation exactly; numerical fit or numerical failure is inconclusive. An exact contradiction only excludes this fixed candidate. No physical invoice or kappa claim follows without separate realization/accounting.

Fixed-candidate finding: a nine-root rank obstruction

The independent algebraic investigation found an exact obstruction for the just-preregistered normals [0,1,56,87] with multiplicities [3,2,2,2], including zero coefficients and distinct left/right factors. Six roots supported exclusively by normal 87 form a rank-two crown configuration. Their nonzero diagonal equations force the two sides of that crown onto two independent factor lines. This forces normal 87's contribution to vanish on three additional mutually orthogonal roots. Those roots lie outside normals 0 and 56, so only normal 1's two terms remain, yet they must realize 4I_3. Rank at most two cannot equal rank three.

This is an exact masked-equation obstruction, not a numerical search failure. A nine-root certificate and written proof are available locally; the independent checker and leader replay passed eight controls. A second independent mathematical review is now checking the proof before final acceptance/publication. The checker verifies the premises of the written lemma; it is not a proof-assistant formalization. The fixed-candidate synthesis worker has been notified to stop further search and preserve its actual work.

The reviewer also reproduced the 40,656 necessary-condition survivors and found no false exclusion in the stated full-support classification. One coordinate-decoder positive control was bound to co-star instead of actual root-star supports; that control is being corrected. The independent correctly bound test passes. The older combinatorial survivor count remains a necessary-condition result, and the new proof rejects its first fixed example. Other direction sets and multiplicity assignments, and the original nine-term family, remain unresolved. No decoder, physical admission, or kappa improvement is claimed.

Independent proof acceptance and implementation closure

A second agent independently reconstructed the nine roots and reviewed every inference of the crown proof; it found no mathematical blocker for the fixed candidate. Its separate exact premise checker passed five negative and three positive controls, reproduced by the leader. This remains AI-assisted review of a written proof, not human peer review or kernel formalization.

The implementation worker's blind numerical search made 29 restarts, used 120.02 CPU seconds, and found no witness (best sum of squared masked residuals approximately 864). That search is inconclusive on its own. Only after receiving the completed proof did the worker replay its ten premises on its own model, successfully; this later check is explicitly proof-informed. Its coordinate-decoder control now uses actual root-star supports; 38 gate controls pass and the census is unchanged.

We are packaging the accepted fixed-candidate theorem, nine-root certificate, and standalone read-only exact checker independently of historical census, timing receipts, and moving selected-result files. Final package review and portability validation remain pending. Other candidates and the parent nine-term question remain open; no kappa improvement is claimed.

[philippeVV]

FINDING: no nine-term masked P112 co-star decoder uses 3–6 distinct normals. This is an exact non-existence result and makes no κ claim. It extends the #1320 obstruction for one fixed assignment to every assignment with k ≤ 6 normals.

Package: research/p112-costar-k6-closure/ (fork commit 86624376).

• Model. M = Σ₉ u_t v_tᵀ on P112. Each term's supports lie in the co-star S_α of its normal. The masked target is 2G on the 6,720 even entries. Zeros, repeated normals and D ≠ T are allowed. The result holds over any field of characteristic ≠ 2.
• Cases. A case is (an orbit under the 172,032-element F0 stabiliser, a capacity composition):

k	cases	initial L1 (#1422 clique demand, sharpened)	propagation	last step
3	56	56	0	–
4	1,960	1,925	35	–
5	39,690	39,140	550	–
6	701,568	637,744	63,801	23

• Rules. All rules are zero-robust:
  • L0 (diagonal);
  • L1/L1Z (rank demand on orthogonal or forced-zero cliques);
  • L2G (a tight block forces kills);
  • L3, a generalisation of @Hope7Happiness's crown lemma: for a capacity-2 owned graph, projective 2-colouring gives a contradiction on odd cycles, and odd distance forces independence.
• Certificates. Every case carries a certificate that an independent stdlib verifier replays. I re-ran the k ≤ 4 ones myself (2,016/2,016). The k=5 and k=6 certificates replay as 39,690 and 701,545 respectively. Orbit completeness is checked for k ≤ 6.
• The last 23 cases all have the shape: an A2 triple with capacities (2,2,2), plus three orthogonal capacity-1 normals in its E6. Two lemmas close them:
  • Lemma C (SAT, UNSAT under CaDiCaL and Glucose): not every class can be served by ≥ 2 rank-1 terms. The orthogonal-triangle clauses come from det(4I − Q) = 0.
  • Lemma B′ (414 Nullstellensatz certificates, all denominators powers of 2): a class block that gets P_a plus at most one rank-1 term is infeasible.
  • I re-ran both checkers myself.
• Not covered:
  • k = 7, 8, 9 distinct normals. This is in progress here, and I will post separately.
  • Supports outside the co-star.
  • Rank ≤ 8, which Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212 covers.

Reproduction commands and expected outputs are in the README. k ≤ 5 and the 23 cases take minutes; the full k=6 regeneration takes about 30–45 minutes with 15 workers.

Credit: @Hope7Happiness (#1267, #1320), @jeremydiviney (#1422), @burntout76 (#1212), @DreamingOfClouds (#717), @themilkman216 (#968). Prepared with substantial Claude (Anthropic) assistance.

[philippeVV]

Addendum: k = 7, 8, 9 distinct normals are still open. I found no decoder. These cases are not closed.

• k = 7. Every 7-set is H-equivalent to a 6-orbit representative plus one line, which gives 3,681,288 extension sets.
  • 1,305,898 of them do not cover, so L0 kills them.
  • The covering ones give 66,510,920 (set, composition) pairs. The initial L1 filter kills 34,500,067.
  • The engine closes every survivor from the first 34,000 extensions.
  • A uniform sample leaves 7 of 13,242 engine cases open, all with caps (2,2,1⁵), for example normals (2,3,4,5,56,87,112). I'd estimate a few hundred open orbit cases.
• k = 8, 9. Only samples so far.
  • k = 8: 39 of 40 closed.
  • k = 9: 19 of 30 closed.
  • Sets containing F0 survive.
• Bessel lemma. For any line α and orthogonal clique Q, |S_α ∩ Q| ≥ |Q| − 4, because Σ_q (α·q)² ≤ |α|²·2/2 = 4. So at k = 9 the initial clique test can only bite on cliques of size ≤ 4. The pure clique-counting argument cannot close k ≥ 7 uniformly.
• F0-containing sets pass every support-level rule. With full co-star supports, orthogonal lines have 0, 2 or 4 common seers, and every block 4-clique and every frame meets enough groups. Closing these needs value-level algebra (a Schur rank-1 identity: M − ¼M[:,Q]M[Q,:] has rank ≤ 1 for a frame Q).
• Numerics (suggestive only). Least-squares fits on the propagated supports of every survivor tried stall at a residual of 848–976, meaning at least 53 diagonal entries are unmet. The same solver reaches about 0 once the capacity is raised to 27. Nothing points to a cost-≤63 decoder.

Certificates replay with the same independent verifier, with 0 failures over 4.3M replays (full or sampled). The next step for k = 7 is about 75 CPU-hours of engine work, then SAT or Gröbner on the survivors. k = 8 and 9 need a value-level lemma first. Released for anyone who wants to continue.

[philippeVV]

Addendum 2: every normal set containing F0 is now closed. This covers the obstruction my previous addendum flagged. Package: f0/ (fork commit 680986f8). Run python3 f0/check_F0.py; it needs python-sat and takes about 3 s.

• Structure. The live lines form 28 orthogonal 4-cliques, two per F0 block. Each clique's lines share the same 4 F0 seers.
• Triangle lemma (value-level). Take three cliques that pairwise share exactly one F0 pair P and contain matched 2-subsets forming an orthogonal 6-set. Suppose two of them are pure-like and the third has at most 3 other terms.
  • Then E = ¼V[A]ᵀU[A] is idempotent, and its complement forces the third clique's projection to 0.
  • That leaves 4I − (nilpotent), which has rank 4 > 3, a contradiction.
  • The Nullstellensatz certificate has 849 cofactor terms, degree ≤ 6, and only power-of-2 denominators.
• Case A (F0 with caps (2,1⁷), any cap-2 normal): a pure/pure/cap-2 triangle always exists, so the lemma applies.
• Case B (F0 ∪ {x}, caps 1⁹): a SAT encoding over the x-term's support (FR plus TRI clauses) is UNSAT for all 112 x under both CaDiCaL and Glucose. Dropping either clause family makes it SAT.

As a side remark, the same E versus I − E odd-cycle argument shows that eight cap-1 F0 terms alone are infeasible, consistent with #1212.

Still open: the other k = 7, 8, 9 normal sets (non-F0 survivors). No κ claim.

[philippeVV]

Addendum 3: Lemma S, a support-level SAT, closes every k = 7 and k = 9 survivor found so far. The complete k ≥ 7 families are still not enumerated, so this is not yet a theorem for k ≥ 7. Package: lemmaS/ (fork commit a85ab165).

• Lemma S. Use Booleans A[g,r] ⇔ D_g[r,:] ≠ 0 and B[g,r] ⇔ T_g[r,:] ≠ 0. They are invariant under GL(c_g). Every decoder satisfies:

  • (D) every diagonal is covered by some A∧B;
  • (X) a capacity-1 product on an orthogonal pair needs a second group alive there;
  • (R) the frame-rank clause: 8 ≤ Σ c_g over groups touching each live 8-frame. By Bessel, every co-star meets every frame in at least 4 lines, so e_g = c_g and the slack is 1.

  UNSAT proves non-existence over any field of characteristic ≠ 2. No Nullstellensatz certificate is needed.

• k = 7. All 53 engine survivors are UNSAT on both CaDiCaL and Glucose. That is the 7 from Addendum 1 plus 46 from two new uniform samples, about 70k engine pairs. All 53 have capacities (2,2,1⁵), with the two capacity-2 normals spanning an A2.

• k = 9. All 416 engine survivors from 1,030 sampled sets are UNSAT on both solvers.

• Cross-check. It also re-closes the 23 hard k = 6 cases without Lemmas B′/C.

• Verification.

  • The checker check_S.py is standalone: it rebuilds E8, pins the Prove a nine-root obstruction for one masked P112 co-star decoder #1320 line-order SHA-256, and enumerates all 262,928 cliques itself.
  • I re-ran the k = 7 file independently and all 53 cases are UNSAT.
  • Positive control: with true supports fixed, random exact integer decoders (including ± cancellations and capacity-2 groups) are SAT in 22/22 trials.

• What remains for a full k = 7 theorem. About 3.2M orbit-deduplicated (set, composition) pairs through the engine (≈70 CPU-h), then Lemma S on the survivors. Since Lemma S kills everything sampled, I'd conjecture the nine-term co-star route is closed for every k.

Prepared with substantial Claude Code (Claude Opus 5.5) assistance; no independent human review claimed.

[philippeVV]

Addendum 4: k = 7 is closed, all of it.

No nine-term masked P112 co-star decoder has terms using exactly 7 distinct normals, over any field of characteristic ≠ 2. This covers every 7-set of normals and all 28 capacity compositions. It makes no new κ, decoder or cost claim.

Package: research/p112-costar-k6-closure/k7/ @ 66d222ff (README has the full method, counts and reproduction).

Case list is complete. I extended the 32,292 6-orbit representatives by every line and got 419,952 7-orbits under H (|H| = 172,032): 269,160 covering and 150,792 non-covering.

• Completeness is checked independently of stage 1 and of the 6-orbit list.
• orb_indep.py brute-forces all of H to show each representative is the lex-least sorted image of itself.
• It also checks Σ|H|/|Stab| = C(120,7) = 59,487,568,920 exactly.

Exact part. Of the 7,536,480 (orbit, composition) cases, 7,534,138 are closed by certificates: an initial L1 clique, or engine kills plus a final L0/L1/L1Z/L3odd contradiction.

• The certificates are replayed with plain Python sets during the run.
• They were replayed again from disk afterwards, with 0 failures and each case appearing exactly once.

SAT part. The remaining 2,342 survivors are closed by Lemma S (Addendum 3), extended to allow capacity 3. Each case is UNSAT on both CaDiCaL 1.5.3 and Glucose 4; there are no DRAT proofs, which is the same standard as Addendum 3.

• 2,332 close with frame cliques alone.
• 8 more close with all cliques of slack ≤ 2.
• The last 2 are one case up to symmetry: set (0,2,3,14,15,56,80) with caps 2 on {3,15} or {2,14}. They need slack ≤ 4 (9.8M clauses). I re-ran both separately: UNSAT on both solvers.

Corrections to Addendum 3.

• The survivors are not all of the A2 type: 2,111 have an A2 capacity-2 pair, 222 have an orthogonal pair, and 9 are (3,1⁶).
• The cost estimate there was based on an incomplete stage 1. The true figures are 32.01M raw filter-surviving pairs and 3,636,308 after orbit dedup.
• The real cost was about 11 CPU-h for stage 2 plus about 1 h for Lemma S.

Status. k = 3–7 are closed. For k = 8 and 9, only the sets containing F0 are closed, plus the sampled k = 9 engine survivors.

Prepared with substantial Claude Code assistance. A sub-agent ran the enumeration. I independently re-ran the completeness check and the two hardest SAT cases.