Repository navigation
CLAIM: global rank-8 rigidity on the 896 admissible P104 units (closes the last P104 orbit after #1212/#1389) #1395
Replies: 1 comment
|
DONE: #1399 (head Rank-8 rigidity holds on the 896 admissible P104 units. In the E-graph model, eight costly terms give cst ≥ 56 there, which PR717's P104 decoders attain. On #1212's pivot, all 14 blocks carry a complete class, so Lemmas 5–6 fix The independent verifier runs 15 checks in 0.1 s, and Open: P105–P110, and nine or more costly terms. |
Uh oh!
There was an error while loading. Please reload this page.
CLAIM: global rank-8 rigidity on the 896 admissible (type (1,…,1)) P104 units (JosieElliston, with Claude via Claude Code). Expires 2026-10-14T02:30Z.
Question. PR #1212 (burntout76, head
57099cb5) proves rank-8 gauge rigidity of the E-graph system,K = D(2G)D^{-1}, on P112, P120 and the 336 type-(2,2,2,2) units. My #1389 closes P111 and the 28 type-(4,4) units. On the 896 admissible units (PR717's P104 among them), #1212's §10 records that four classes keep only two live rows, so Lemma 5 has no grip. Does Theorem 1 hold there, and with it the eight-costly-term floor cst ≥ 56?Method. A propagation lemma. On #1212's admissible pivot, all 14 blocks have a complete class, so Lemmas 5–6 already fix the global scaling
gon the 22 complete classes. A two-row lineithen gets its form directly from (E2), applied in both orders against witnessesjin complete classes: each witnessed column pair givesa_ik ε_ik / g_k = a_ik' ε_ik' / g_k'. If the witnessed pairs connectT_i, thena_i ∝ ε_i gandb_i ∝ ε_i / g, and (E0) fixes the product. No in-class equation is used. The finite input, witness connectivity, comes from a new standard-library checker. #1212's zero exclusion on this unit is replayed.Scope. Card
complex-masked-decoder(chooser nonce6dba39f7133593e3228f8833f5d6594a), refined to this obligation. Basebce54fb3. This is the open next question of #1389. Not covered: nine or more costly terms, any construction, and any κ.Overlap. No claim or PR found on global rigidity for the admissible units (overlap search refreshed 00:05Z). #1292 and #1367 are local (tangent) only. Expected artifact: a research package and a PR.
All reactions