P112 E-graph floor of 64 for one extra term with fixed readers

research/p112-masked-fixed-reader-lift/PROOF.md

@@ -0,0 +1,184 @@
+# One E-graph term does not beat the fixed coordinate readers
+
+This is a theorem about one finite model. The executable checks in
+`verify.py` certify the finite premises. The classical all-pairs floor is
+an inherited theorem, pinned in `SOURCES.json` and not re-proved here.
+
+## Model
+
+Start from the 120 real E8 root lines and delete the eight mutually
+orthogonal frame lines `e_(2a) ± e_(2a+1)`. The remaining 112 ports have
+coordinate matrix `X`, with columns `x_0, ..., x_7`. Every entry of `X` is
+0 or ±1, every row has four nonzeros, and each column support (a star) has
+size 56. The Gram matrix `M4 = X X^T` equals 4 on the diagonal. Its
+off-diagonal entry is 0 exactly on the pairs with label product 1. That
+undirected graph, including loops at every port, is the E-graph: 60 ones
+in each row. The other 52 ports in a row are the odd neighborhood. Label
+pairing is the F2 matrix of this graph; its rank on all 112 ports is 9.
+
+A term has a reader vector and a source vector in `R^112`. Its copy cost
+is the F2 rank of the label pairing between those two supports. The eight
+coordinate terms `(x_k, x_k)` cost 8 each, total 64. That value belongs
+to the coordinate decoder of PR620. An extra term is a pair `(d, t)`.
+
+**Theorem.** Suppose the eight coordinate readers stay equal to the columns
+of `X`, and equality to `M4` is required only on the E-graph. For every
+real reader `d`, every real source `t`, and every real source matrix whose
+eight columns `s_0, ..., s_7` satisfy
+
+```text
+sum_k X[i,k] s_k[j] + d[i] t[j] = M4[i,j]
+```
+
+whenever port `i` is on the E-graph at port `j`,
+
+```text
+sum_k beta(x_k, s_k) + beta(d, t) >= 64.
+```
+
+Equality is attained by an E-graph-exact term that is not exact on the odd
+pairs. No new multiplication exponent is claimed. Frames, restoration,
+hosting, precision, and all-size analytic charges were not priced; they
+were left at zero, and the copy-rank sum still does not fall below 64.
+
+## Normal form
+
+Write `N(j)` for the E-graph neighborhood of port `j`, a set of 60 ports.
+`X` restricted to `N(j)` has rank 8, so it is injective on `R^8`. The same
+count on `N(j) ∩ N(j')` is 8 for every one of the 3,304 E-graph edges and
+6 for every one of the 2,912 odd pairs. Thus, at each `j`:
+
+- if `t[j] = 0`, the source row equals the row `X[j]`;
+- if `t[j] ≠ 0`, then `d` agrees on `N(j)` with `X a` for a unique
+  `a = a(j) in R^8`, and the source row is `X[j] - t[j] a(j)`.
+
+Adjacent ports of the support `J = supp(t)` have the same `a`, because
+their neighborhoods intersect in rank 8. So `a` is constant on each
+E-component of `J`.
+
+`N(v)` without `v` has rank 7 and is orthogonal to the row `X[v]`. The
+right kernel of those rows is the line through `X[v]`.
+
+## Star code
+
+On each star, the E-graph adjacency has F2 rank 8. Its 255 nonempty
+codewords, 2,040 in total, fall into six families:
+
+| weight | components | common odd neighbors | count |
+|---:|---|---:|---:|
+| 28 | one | 0 | 576 |
+| 32 | one | 0 | 504 |
+| 28 | one | 1 | 448 |
+| 24 | one | 1 | 448 |
+| 24 | one | 0 | 56 |
+| 56 | one | 0 | 8 |
+
+Every codeword is E-connected, and the minimum weight is 24. A coordinate
+pairing rank drops below 8 only when the zero set of that source column
+contains one of these codewords. Outside `J`, every source column agrees
+with `X`, whose star support is the whole star. Therefore every dropped
+coordinate meets a codeword inside `J`.
+
+Each of the 448 star memberships has 27 E-neighbors inside its star. The
+pairing rank of that one column is 1. The 27 neighbors have rank 7, and
+adding the point does not raise it. Those neighbors are disjoint from the
+odd neighborhood of the point. While they remain in the source support,
+changing the source entry at that single port does not change the
+coordinate cost.
+
+## One codeword leaves at most one extra port
+
+If `J` contains no star codeword, every coordinate costs 8 and the extra
+term costs at least 0, so the sum is at least 64.
+
+Now suppose `J` contains a codeword `W`.
+
+If `W` has no common odd neighbor, every port outside `W` has an E-edge
+into `W`. Any further point of `J` joins the same component, so there is
+one vector `a`. The reader `d` equals `Xa` on every E-neighborhood of `J`.
+The complementary ports, if any, are orthogonal to all of `J`, so their
+pairing rows do not affect `beta(d, t)`. The sources are exactly the
+classical sources `X - t a^T`. The cost equals the classical single-lift
+cost of `(a, t)`.
+
+If `W` has one common odd neighbor `v`, the same counting leaves at most
+the port `v` outside `W`'s component: a second component would need
+another port orthogonal to every point of `W`, and every such codeword has
+only one. Both the 448 weight-28 codewords and the 448 weight-24 codewords
+lie entirely in the odd neighborhood of their neighbor `v`. For each of
+them, `X` on `N(v) ∩ (union of N(w) for w in W)` has rank 7 and is
+orthogonal to `X[v]`, so its kernel is the line through `X[v]`. A larger
+odd component only adds rows, so it does not enlarge that kernel.
+
+- If `v` is not in `J`, the sources are classical. The pairing row of `v`
+  against `J` is zero, so a reader value at `v` does not change the extra
+  rank.
+- If `v` is in `J` and some E-neighbor of `v` is also in `J`, that neighbor
+  meets `W` (otherwise it would be a second common odd neighbor) and the
+  edge to `v` pulls `v` into `W`'s component. Again there is one vector `a`.
+- If `v` is in `J` and no E-neighbor of `v` is in `J`, then
+  `J ⊆ {v} ∪ odd(v)`. The big component has a vector `a` and the singleton
+  `{v}` has a vector `b` with `b - a` in the joint kernel, hence
+  `b = a + λ X[v]`. The 27 E-neighbors of `v` stay outside `J`, so every
+  coordinate cost equals the classical cost of `(a, t)`. On `N(v)` the
+  Gram column of `v` vanishes off the diagonal, so `X b` and `X a` differ
+  only at port `v`. Ports outside every E-neighborhood of `J` contribute
+  zero pairing rows. The masked reader therefore differs from `Xa`, for
+  pairing against `J`, by at most the membership of port `v`.
+
+## Reduction to the classical floor, except one parallel line
+
+The inherited theorem, `research/p112-single-lift/PROOF.md`, states that
+every classical single lift costs at least 64, and it says explicitly that
+its argument does not cover a masked completion. This package uses that
+theorem only after the masked term has been given the same coordinate
+costs and the same extra rank as a classical lift. It does not replay the
+3,272 sign systems.
+
+Let `S = supp(Xa)`. Over all 511 nonzero label functionals `q` and every
+port `v` in the support `I_q`, the rows `X[I_q without v]` have corank at
+most 1. The 112 corank-1 kernels that meet `X[v]` are parallel to that
+row. The other 448 corank-1 kernels are orthogonal to `X[v]`. There is no
+corank greater than 1.
+
+Consequently `v` is label-critical for `S` only when `a` is a nonzero
+multiple of the row `X[v]`. If `a` is not such a multiple, `lab[v]` is in
+the span of the other rows of `S`, so toggling port `v` in the reader does
+not change the extra rank. The masked cost equals the classical cost and
+is at least 64.
+
+If `a` is a nonzero multiple of `X[v]`, the four stars that do not contain
+`v` have a zero coefficient, so they are not cancelled and cost 8. Each of
+the four stars that contain `v` keeps its 27 E-neighbors in the source, so
+it costs at least 7. When all four cost 8, the sum is at least 64. When
+one costs less than 8, `J` contains an active codeword `W` of weight 28.
+There are 448 of these, four at each port. Every odd neighbor of `v` lies
+in an E-neighborhood of `W`, the Gram column is nonzero on all 52 of them,
+and their pairing rank against `W` is 7. The coefficient `λ` does not
+change that column off `N(v)`. The extra term therefore costs at least 7,
+the coordinates cost at least 60, and the sum is at least 67. The zero
+vector `a` cancels nothing; redundancy again leaves every coordinate at 8.
+
+## Equality and a strict deformation
+
+At port `v`, take `d` equal to the Gram column of `v` on the odd
+neighborhood and equal to 0 on `N(v)`, with the extra source supported
+only at `v` and with the eight coordinate sources left equal to `X`. The
+E-graph column is unchanged. Every odd entry of that column is nonzero, so
+the term is not all-pairs exact. All eight stars still cost 8, and the odd
+reader pairs with `{v}` at rank 0. The sum is 64.
+
+A second witness cancels one active weight-28 codeword and retunes port
+`v` by `λ = 1`. The resulting E-graph identity holds, one coordinate falls
+to 7, and the extra rank rises enough that the sum is 71.
+
+## What was not proved
+
+The verifier's rational ranks are modular ranks at the prime 65,537. Every
+8×8 minor of a 0/±1 matrix has absolute value at most `8^4 = 4096`, so
+this prime does not hide a nonzero minor. Kernel vectors used for the
+parallelism test are rebuilt over `Q` from seven original rows.
+
+The classical sign census inside the inherited proof was not run. Two
+extra terms, a replaced coordinate reader, and any cost outside this
+pairing-rank sum are outside the theorem.

research/p112-masked-fixed-reader-lift/README.md

@@ -0,0 +1,106 @@
+# Fixed coordinate readers plus one E-graph term still cost 64
+
+**Negative result for one masked family. No new κ, and the selected frontier is unchanged.**
+
+The eight P112 coordinate readers stay fixed. One extra term has to match
+`X X^T` only on the E-graph, not on the odd pairs. In that model the sum of
+pairing-rank copy costs is at least 64. Equality is attained by a reader
+supported on an odd neighborhood: the term is E-graph exact, it moves odd
+Gram entries, and its own pairing rank is 0.
+
+This is the masked gap left open by the classical single-lift theorem. That
+theorem already proves the same floor when the identity is required on every
+pair, and it says that a masked completion is outside its argument. The
+normal form here puts every one-term E-graph completion next to a classical
+lift, except for a one-port retuning along the port's own row. That parallel
+line is bounded directly. The non-parallel line quotes the classical floor
+and does not replay its sign census.
+
+## Scope
+
+Catalogue card `complex-masked-decoder`, scope **refined**. Selector nonce
+`9ea1268e3ca1bd3df643b60bf3142efd`, track `complex-mechanisms`, priority
+revision 2. Base commit `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`.
+
+The card asks whether one specified masked or overcomplete decoder can
+improve the complete moment budget. The family actually proved is narrower:
+eight fixed coordinate readers, one extra term, exactness only on the P112
+E-graph, and cost equal to the pairing-rank sum. The eight-term all-pairs
+search is not repeated. Frames, restoration, hosting, precision, and
+all-size analytic obligations were not priced. They were treated as zero,
+and the copy-rank sum still does not drop.
+
+A cheaper fully realized decoder could still move the binding complex side.
+This family does not. It is a side constraint on one decoder shape, not a
+new supplier and not a change to the selected record.
+
+## Evidence
+
+The argument is in [PROOF.md](PROOF.md). The finite census is
+[verify.py](verify.py): 3,304 E-pair intersections of rank 8, 2,912 odd
+pairs of rank 6, 2,040 star codewords, 112 label-critical rows, 448 active
+odd-closure codewords, and five mutation controls. Two algebraic fixtures
+are included. One meets 64 and is not all-pairs exact. The other is an
+E-graph deformation whose coordinate costs are `[7,8,8,8,8,8,8,8]` and
+whose total is 71.
+
+Checks that name an inherited sentence only confirm that the pinned file
+still contains it. They are not a replay of that proof.
+
+Overlap refreshed 2026-10-21 against 458 open PRs and 3,225 discussions.
+Nearby results are different objects: the classical all-pairs lift, free
+odd rectangles mixed into one coordinate, two-column masked Gram
+completions and their COPY-power screens, and trimmed-star or rank-8
+rigidity censuses. No match was a fixed eight-reader, one-extra-term,
+E-graph-only pairing-rank floor. That search is not a novelty certificate.
+
+## Reproduce
+
+Python 3.12, standard library only. From the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/p112-masked-fixed-reader-lift --check-only
+python3.12 scripts/research_package.py --package research/p112-masked-fixed-reader-lift
+```
+
+Expected final line of the package verifier:
+
+```text
+PASS_P112_MASKED_FIXED_READER_LIFT floor=64 readers=coordinate extra-terms=1 mask=E-graph e-pairs=3304 codewords=2040 critical=112 active-closure=448 inactive-closure=448 controls=5
+```
+
+`PYTHONOPTIMIZE` must be unset. The script raises on failure, so `python -O`
+cannot skip a broken check. No artifact-regenerating suite was run beside
+this verifier.
+
+## Open next questions
+
+1. **Two extra terms with the same fixed readers.** The one-term normal form
+   uses a single reader, so two source supports can carry two vectors even
+   when each codeword has only one odd neighbor. A first step is to fix two
+   odd-disjoint star codewords, give each its own reader, and price the sum.
+   The blocker is that the rank-8 intersection argument no longer forces
+   those readers to be the same classical column.
+
+2. **Replacing one coordinate reader instead of only adding a term.**
+   Uniqueness of the neighborhood vector `a(j)` uses the fixed columns of
+   `X`. A first step is to delete one star, let that reader be an arbitrary
+   real vector, and rerun the neighborhood rank. The blocker is that the
+   coordinate frame is an input to the normal form, not a conclusion.
+
+## Attribution and discussion access
+
+Coordinate cost 64 belongs to Joel Pulikkan / GamingPuzzled, PR620. The P112
+E-graph model belongs to DreamingOfClouds, PR717. The classical single-lift
+floor belongs to Mihir Srivastava, `research/p112-single-lift`. The card's
+starting points are `research/complex-decoder-field-extension-seed44` and
+`research/complex-frame-pair-decoders`; their eight-term all-pairs floor is
+not re-opened here.
+
+Discussion writes to CrocSwap/integer-mult-bounds are forbidden for this
+account (`FORBIDDEN` / resource not accessible by integration). No discussion
+post was attempted on this run, and none should be retried until that
+access changes.
+
+Prepared by hevlyo. Substantial AI assistance was used for the normal form,
+the finite census, the verifier, and the write-up. New work is Apache-2.0.

research/p112-masked-fixed-reader-lift/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/p112-single-lift/PROOF.md",
+      "usage": "input",
+      "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a",
+      "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1"
+    }
+  ]
+}

research/p112-masked-fixed-reader-lift/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-masked-decoder",
+  "priority_revision": 2,
+  "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6",
+  "original_card": {
+    "id": "complex-masked-decoder",
+    "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?",
+    "starting_points": [
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md"
+    ],
+    "methods": [
+      "Synthesize a decoder with exact coefficients and fully priced helper endpoints.",
+      "Bound the best possible budget for a fixed support alphabet before synthesis."
+    ],
+    "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-decoder-field-extension-seed44/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44",
+      "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.",
+    "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.",
+    "allowed_variations": [
+      "Select a specific masked or overcomplete family with exact labels and supports."
+    ],
+    "scope_change_triggers": [
+      "Repeating the exact eight-term all-pairs search inside its proved scope."
+    ],
+    "overlap_terms": [
+      "masked decoder",
+      "overcomplete",
+      "eight-term"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "With the eight P112 coordinate readers fixed, does one extra term that is required to match X X^T only on the E-graph have pairing-rank copy cost at least 64?",
+  "scope_change_reason": "The card asks whether some masked or overcomplete decoder improves the full moment budget. This package keeps the coordinate readers, weakens all-pairs exactness to the E-graph, and prices the one extra term by pairing rank. It does not repeat the excluded eight-term all-pairs search.",
+  "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side. This masked one-term family does not lower the copy-rank sum, so it does not move that side.",
+  "budget_minutes": 60,
+  "stop_rule": "The finite census and the one-term normal form are complete. The run stops on that negative result rather than on a timeout.",
+  "outcome": "negative-result",
+  "evidence": "research/p112-masked-fixed-reader-lift/verify.py prints PASS_P112_MASKED_FIXED_READER_LIFT. PROOF.md records the normal form, the reduction to the pinned classical floor, and the self-contained parallel line.",
+  "author": "hevlyo",
+  "ai_assistance": "Substantial AI assistance was used for the normal form, the finite census, the verifier, and the write-up.",
+  "open_questions": [
+    {
+      "question": "With the same eight coordinate readers fixed, can two extra E-graph terms have pairing-rank sum below 64?",
+      "why_it_matters": "A second reader can carry a second vector on a second codeword. The one-term intersection argument does not forbid that, and a drop would be a masked decoder outside this theorem.",
+      "first_step": "Fix two odd-disjoint star codewords, assign each a reader vector, and compute the pairing-rank sum on that support.",
+      "blocked_by": "Rank-8 agreement of E-neighborhoods forces one vector only inside a single reader's support."
+    },
+    {
+      "question": "Does the floor survive if one coordinate reader is replaced instead of being held fixed while a term is added?",
+      "why_it_matters": "Uniqueness of the neighborhood vector uses the fixed columns of X. Replacing a reader is a different masked family and could change the copy sum.",
+      "first_step": "Delete one star, let that reader be an arbitrary real vector, and rerun the neighborhood rank count.",
+      "blocked_by": "The coordinate frame is an input to the normal form, not a consequence of it."
+    }
+  ]
+}