Prove no F2 sum of letters hosts the P104 frame-0 indicator.

research/p104-frame0-letter-sum/PROOF.md

@@ -0,0 +1,189 @@
+# No sum of letters hosts the frame-0 indicator
+
+No new κ. The selected record stays `781451/250000000`. This note answers the
+sum question left open by PR #7031. It does not redo that product census, it
+does not host another frame, and it does not name monomials on the selected
+invoice.
+
+## 1. Hypotheses
+
+Ports, the odd graph, and the simple-root chart are those of PR #7031. Frame 0
+of the #7014 witness is the ordered 8-tuple
+
+```text
+11, 21, 38, 56, 140, 146, 161, 191.
+```
+
+A **letter** `λ_i` is the root-line functional `j ↦ (<r_i, r_j> + 1) mod 2`.
+In the chart every label has ninth coordinate 1, and the accepted identity
+`S9(u_i, u_j) = (<r_i, r_j> + 1) mod 2` makes each letter an affine function
+
+```text
+λ_i = 1 + (linear form in x0, ..., x7).
+```
+
+A **sum of letters** is an `F_2` linear combination of these 120 functions.
+Repetitions cancel in pairs, so every sum is the sum of a set of distinct
+letters. The sum **hosts** the row when its value is 1 on the eight frame
+lines and 0 on the other 112 root lines. Agreement on the 104 P104 lines is
+the weaker condition used below; it is already impossible.
+
+The charge of a word is the set of square-free monomials in its algebraic
+normal form, in this fixed chart, with `x_i^2 = x_i`. As in #7031, a
+**new** monomial is one of degree at least 2. The constant and the eight
+variables are not new.
+
+Sums in `Z`, thresholds, and sums of products are outside these hypotheses.
+
+## 2. The explicit sum
+
+**Proposition.** The sum of four frame letters cancels:
+
+```text
+λ_11 + λ_21 + λ_38 + λ_56 = 0.
+```
+
+The chart polynomials, recomputed from the labels, are
+
+```text
+λ_11 = 1 + x1 + x2 + x4 + x5,
+λ_21 = 1 + x0 + x1 + x2 + x4 + x5,
+λ_38 = 1 + x0 + x1 + x2 + x4,
+λ_56 = 1 + x1 + x2 + x4.
+```
+
+Each of `1, x0, x1, x2, x4, x5` occurs an even number of times (`4, 2, 4, 4,
+4, 2`), and `x3, x6, x7` do not occur. The sum is the zero polynomial. Its
+monomial list is empty, so it has **zero** new monomials. On every root line
+the value is 0, including the eight frame lines, so the sum does not host
+the row.
+
+The same direct count gives thirteen further cancelling fours inside the
+frame, and the sum of all eight frame letters is zero as well. No nonempty
+subset of the eight of size other than 4 or 8 cancels. Deleting any one
+letter from `λ_11 + λ_21 + λ_38 + λ_56` leaves a nonzero affine function.
+None of the 255 nonempty subset-sums of the eight frame letters hosts the
+row. That 255-count is an exhaustive census of a finite domain. It is not a
+census of sums that use a letter from outside the frame.
+
+One single letter has the same new-monomial count and also fails. For
+example `λ_11` expands to `1, x1, x2, x4, x5` (zero new monomials). It equals
+1 on all eight frame lines and also equals 1 on a line outside the frame.
+
+## 3. Every sum is affine, and none hosts
+
+**Theorem.** Under the hypotheses in §1, every sum of letters has algebraic
+normal form of degree at most 1, hence has zero new monomials. No such sum
+agrees with the frame-0 indicator on the 104 P104 lines. In particular, no
+sum hosts the #7031 row on all 120 root lines, and no sum hosts that row
+with fewer than 40 new monomials.
+
+The degree bound is the sum of affine functions. It does not use a search.
+The zero new-monomial count is the same degree cut #7031 uses for the
+product charge. Every sum would be strictly below 40 on that cut. The
+obstruction is that none of them hosts.
+
+**Four-line parity.** Let `v(j) ∈ F_2^9` be the eight chart coordinates of
+root line `j`, followed by a constant coordinate 1. For an affine function
+`f(x) = c + Σ a_i x_i`, the sum of `f` over a set of lines equals the
+`F_2` dot product of `(a, c)` with the sum of their vectors `v(j)`. The four
+P104 ports `478, 11, 14, 475` have chart coordinates
+
+```text
+478: (0, 0, 1, 1, 0, 0, 0, 0),
+11:  (0, 1, 0, 1, 1, 0, 0, 0),
+14:  (1, 1, 1, 1, 0, 1, 0, 1),
+475: (1, 0, 0, 1, 1, 1, 0, 1).
+```
+
+Each coordinate appears an even number of times, and the four constant
+coordinates sum to 0. Therefore `v(478) + v(11) + v(14) + v(475) = 0`, and
+every affine function has value-sum 0 on these four lines. Any three of the
+four vectors already sum to something nonzero, so the dependence has size
+exactly 4.
+
+Port 11 is in the frame. Ports 478, 14 and 475 are in P104 and are not in
+the frame. The indicator therefore takes values `0, 1, 0, 0` and has
+value-sum 1. No affine function can match it on these four lines, hence
+none matches it on all 104 P104 lines, hence none matches it on all 120
+root lines.
+
+A second four, also inside P104, gives the same contradiction. Ports
+`21, 13, 493, 501` have coordinates
+
+```text
+21:  (0, 0, 1, 1, 1, 0, 0, 0),
+13:  (0, 1, 0, 1, 1, 1, 0, 0),
+493: (0, 1, 1, 1, 1, 0, 0, 0),
+501: (0, 0, 0, 1, 1, 1, 0, 0),
+```
+
+which sum to 0, while the indicator is 1 only at port 21.
+
+The cancelling frame sum of §2 is a dependence of the other kind. The
+evaluation labels of ports `11, 21, 38, 56` also sum to 0, but all four
+ports are in the frame, so the indicator sum is 0 as well. That relation
+does not separate the indicator from the affine functions. Clearing the
+frame membership of port 11 in the first four would likewise make the
+indicator sum even, and that altered row would not be obstructed by this
+particular four.
+
+## 4. Finite censuses
+
+These domains are finite, every element is visited, and the counts are
+checked by `verify.py`. They are not samples.
+
+1. **Chart identity.** All `120 × 120` pairings match
+   `(<r_i, r_j> + 1) mod 2`. Every letter has constant term 1, and the 120
+   letter vectors in `F_2^9` are distinct and have rank 9. Subset sums of
+   the letters are therefore exactly the 512 affine functions. The census
+   of affine functions is the census of sums.
+
+2. **Distances.** Evaluated on the 120 root lines, the 512 affine functions
+   have Hamming distances
+
+   ```text
+   8, 48, 56, 64, 72, 112
+   with multiplicities
+   1,  7, 248, 248, 7,  1.
+   ```
+
+   The unique function at distance 8 is the zero polynomial, which is the
+   explicit sum of §2. It matches the 112 non-frame lines and misses the
+   eight frame lines. Every other sum misses at least 48 lines. On the 104
+   P104 lines the distances are
+
+   ```text
+   8, 36, 44, 48, 52, 56, 60, 68, 96
+   with multiplicities
+   1,  3, 12, 199, 82, 199, 12, 3,  1.
+   ```
+
+   Again the minimum is 8 and is achieved only by zero. No affine function
+   hosts on either domain.
+
+3. **Short obstructions.** No subset of 1, 2, or 3 of the 120 root lines has
+   augmented-label sum 0. Exactly 7168 subsets of size 4 have augmented-label
+   sum 0 and indicator sum 1. Each of those 7168 meets the frame in exactly
+   one line. Exactly 4384 of them lie entirely in the 104 P104 lines. The
+   two fours of §3 are in that list. This is why a one-line, two-line, or
+   three-line witness cannot exist, and why size 4 is the minimum.
+
+4. **Short syzygies.** No set of 1, 2, or 3 distinct letters sums to the
+   zero function. Exactly 32130 sets of four letters do. The explicit sum
+   of §2 is one of them. The zero function is therefore achieved by a
+   nonempty sum, not only by the empty combination.
+
+5. **Frame-letter sums.** Of the 255 nonempty subset-sums of the eight
+   frame letters, 15 are the zero polynomial (14 fours and the full eight)
+   and none hosts the row.
+
+## 5. What this does not say
+
+The product in #7031 is not a sum. Its 40 new monomials remain a
+product-hosting charge. This note does not prove that 40 is minimal for
+sums of products, for a different chart, or for a circuit that is not an
+`F_2` sum of letters. It does not prove that the indicator is non-affine
+as a function on all of `F_2^8`; the obstruction is only on root lines. A
+failed search outside this alphabet would not be a minimality proof. No
+selected-invoice histogram is computed, and κ is unchanged.

research/p104-frame0-letter-sum/README.md

@@ -0,0 +1,110 @@
+# No sum of letters hosts one P104 frame indicator
+
+**No new κ.** The selected frontier stays `781451/250000000`. This package
+answers open question 2 of PR #7031: whether an `F_2` sum of root-line letters
+can host frame 0 with fewer than 40 new monomials. It does not redo the
+product hosting, it does not host frame 1, and it does not price the selected
+invoice.
+
+## Result
+
+Frame 0 is the odd-graph clique `11, 21, 38, 56, 140, 146, 161, 191`. A letter
+is one root-line pairing. In the inherited simple-root chart every letter is
+affine of the form `1 + (linear form)`, so every `F_2` sum has degree at most
+1. The new-monomial count, using the same degree cut as #7031, is therefore 0
+for every sum.
+
+The explicit sum of four frame letters cancels:
+
+```text
+λ_11 + λ_21 + λ_38 + λ_56 = 0.
+```
+
+Its monomial list is empty: zero monomials of degree at most 1 and **zero**
+new monomials. The value is 0 on every root line, so the sum misses all eight
+frame lines and does not host the row. A single letter such as `λ_11` expands
+to `1, x1, x2, x4, x5`, also with zero new monomials, and equals 1 outside the
+frame.
+
+No sum hosts the row. The four P104 ports `478, 11, 14, 475` have augmented
+chart labels summing to 0, so every affine function has value-sum 0 there.
+The indicator is 1 only at port 11, so its value-sum is 1. The same
+contradiction holds for `21, 13, 493, 501`. The argument is written in
+[PROOF.md](PROOF.md). It already fails on the 104 P104 lines, before the 16
+lines outside P104 are considered.
+
+The 120 letters span all 512 affine functions. On the 120 root lines their
+Hamming distances from the indicator are `8, 48, 56, 64, 72, 112` with
+multiplicities `1, 7, 248, 248, 7, 1`. The unique closest sum is the zero
+polynomial, at distance 8. No subset of one, two, or three root lines gives
+this parity obstruction; 7168 subsets of size 4 do, and 4384 of those lie
+inside P104.
+
+## Evidence class
+
+The degree bound and the four-line parity are written proofs. The chart
+identity, the rank-9 span, the distance histograms, the 7168 four-line
+obstructions, the 32130 four-letter syzygies, and the 255 subset-sums of the
+frame letters are exhaustive finite censuses. This is not a heuristic and not
+an incomplete search inside the sum alphabet.
+
+It is not a proof that 40 is minimal for sums of products, for another chart,
+or for a circuit that is not an `F_2` sum of letters. The #7031 product remains
+a hosting with 40 new monomials. That product is not a sum. No selected-invoice
+histogram is computed, and the result does not beat the selected profile.
+
+## Scope
+
+Catalogue card `complex-rank-shape-decoder`, priority revision 8, pinned at
+`17469fff78c22941280f04d39dc5a1faee09c840`. The card asks whether a decoder or
+coframe change improves the full signed moment. Scope is **changed** to open
+question 2 of
+[PR #7031](https://github.com/CrocSwap/integer-mult-bounds/pull/7031): the
+product census there does not cover sums. The connection to the bottleneck is
+recorded in [TASK.json](TASK.json). A joint bill cannot undercut the product
+charge by replacing this row with a sum of letters, because no such sum hosts
+the row. That is not a signed histogram and not a supplier admission.
+
+`data/frames.json` is the frame partition vendored by #7031 from PR #7014
+(head `949c0ada285aae619468ae49317c8d9f4df130f7`), byte hash
+`c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d`. Only frame 0
+is evaluated. Ports and the E8 line map are the #6933 inputs pinned in
+[SOURCES.json](SOURCES.json).
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3 -B research/p104-frame0-letter-sum/verify.py
+python3 -I -O -B research/p104-frame0-letter-sum/verify.py
+python3 -B scripts/research_package.py --package research/p104-frame0-letter-sum
+python3 -B scripts/check_research_commit.py --package research/p104-frame0-letter-sum --check-source-history
+```
+
+The verifier prints `PASS_P104_FRAME0_LETTER_SUM` with `explicit=11+21+38+56`,
+`monomials=0`, `new=0`, and `hosts=0`. Failure controls delete one letter of
+that sum, reject each proper subset of the obstructing four, keep a
+frame-supported dependence with even indicator parity out of the obstruction
+count, and reject the constant-1 function and the single letter `λ_11`.
+
+## Open next questions
+
+1. Can one explicit `F_2` sum of two products of root-line letters, each
+   product of length at least 2, host this same row with fewer than 40
+   monomials of degree at least 2? Pure sums are affine and cannot host. One
+   product of four letters already hosts with 40. A sum of two products is the
+   first expression that neither census covers. One miss is not a minimum.
+2. Among the `2^16` functions of the four #7031 forms
+   `p = 1 + x1 + x2 + x4`, `q = x0`, `r = x5`, and `s = x6 + x7`, what is the
+   minimum number of degree-at-least-2 monomials of a function that matches
+   the indicator on all 120 lines? This finite family contains the length-4
+   product and every sum of letters inside its span. It does not decide a
+   general circuit.
+
+## Credit
+
+Frame partition: unpaidmoon, PR #7014, as vendored by PR #7031. The product
+hosting and the 40-monomial charge: PR #7031. Ports and the odd-graph window:
+PR #6933. Label pairing: the inherited simple-root chart. Prepared by
+unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0.

research/p104-frame0-letter-sum/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-port-window-haemers/data/e8_line_map.json",
+      "usage": "input",
+      "git_blob": "19ea2d553aff60e53af50dd9582ab70730e93450",
+      "sha256": "b37530e8e9b2b3bd5be418d5ed3060a42ceb66e60ed3789f8ee79f29dabde437"
+    },
+    {
+      "path": "research/p104-port-window-haemers/data/ports_p104.json",
+      "usage": "input",
+      "git_blob": "8037fd10877f49063a1c8a530b40c27f2453dac0",
+      "sha256": "691c7b7d212112115b1bfc76db89f90d304ec448dc8c4a0c43d9a5954317146c"
+    }
+  ]
+}