From e7271f9d709149590071f11a29dfe702d427b59a Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:11:52 +0000 Subject: [PATCH] Host P104 frame 1 and intersect its new monomials with the recorded forty. Frame 1 of the 104-by-13 witness is hosted by 149 products of root-line letters, all equal to one 120-monomial polynomial. Of the 111 monomials of degree at least 2, 31 lie in the 40 recorded for frame 0 and 80 are the additional charge. The selected kappa is unchanged. Co-authored-by: unpaidmoon --- .../PROOF.md | 322 +++++++++++ .../README.md | 133 +++++ .../SOURCES.json | 30 + .../TASK.json | 81 +++ .../VERIFY.json | 32 ++ .../data/frames.json | 157 ++++++ .../verify.py | 514 ++++++++++++++++++ 7 files changed, 1269 insertions(+) create mode 100644 research/p104-frame1-monomial-intersection/PROOF.md create mode 100644 research/p104-frame1-monomial-intersection/README.md create mode 100644 research/p104-frame1-monomial-intersection/SOURCES.json create mode 100644 research/p104-frame1-monomial-intersection/TASK.json create mode 100644 research/p104-frame1-monomial-intersection/VERIFY.json create mode 100644 research/p104-frame1-monomial-intersection/data/frames.json create mode 100644 research/p104-frame1-monomial-intersection/verify.py diff --git a/research/p104-frame1-monomial-intersection/PROOF.md b/research/p104-frame1-monomial-intersection/PROOF.md new file mode 100644 index 0000000000..1d088a19a2 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/PROOF.md @@ -0,0 +1,322 @@ +# Frame 1 hosted, and its overlap with the recorded forty + +No new κ. The selected record stays `781451/250000000`. This note hosts frame 1 +of the odd-character P104 window by a product of root-line letters, charges +every monomial of degree at least 2, and intersects that set with the 40 +monomials recorded for frame 0. It does not host frames 2 through 12 and it +does not compare a histogram with the selected profile. + +## 1. Hypotheses + +Ports and the odd graph are those of PR #6933. Two distinct ports are adjacent +when the parity of their bitwise-and popcount is 1. Frame 1 of the #7014 +witness, vendored at `data/frames.json`, is the ordered 8-tuple + +```text +13, 26, 131, 148, 262, 273, 392, 415. +``` + +A **letter** is a root-line functional `λ_i(j) = ( + 1) mod 2` on the +120 root lines. A **word** is a product of letters. The product is evaluated in +`F_2`, so the value is 1 only when every factor is 1. The word **hosts** the +frame-indicator row when, on all 120 lines, the product equals 1 on these eight +lines and equals 0 on the other 112. Restriction to the 104 P104 lines is then +the indicator of this frame. + +Labels use the inherited simple-root chart. If `B` is the doubled simple-root +basis, the label of a root `r` is its coordinate vector in `B`, reduced mod 2, +with a ninth coordinate 1. The symmetric form `S9` is the Cartan matrix of `B` +on the first eight coordinates and 1 on the ninth diagonal entry. The chart is +used because `S9(u_i, u_j) = ( + 1) mod 2` holds for every pair of +the 120 lines. That identity is checked exhaustively on all 14,400 pairs. It is +the same chart as in PR #7031. + +Square-free monomials are written in `x0, ..., x7`. The relation `x_i^2 = x_i` +is used throughout, so every function `F_2^8 → F_2` has one algebraic normal +form. Every affine function is idempotent in this ring: cross terms have +coefficient 2. + +The recorded forty are the degree-at-least-2 monomials of the frame-0 +polynomial proved in PR #7031, + +```text +(1 + x0)(1 + x1 + x2 + x4)(1 + x5)(1 + x6 + x7). +``` + +The variables in the four factors are disjoint, so the square-free expansion +has `2 · 4 · 2 · 3 = 48` monomials and no cancellation. Eight have degree at +most 1. The other 40 are the recorded charge. This note does not rerun the +frame-0 census. It locks the expansion by the ANF hash recorded with that +proof, `26803d29aa3141a357da4aa551195fe6378d3f2e1cba0c4291a4dedbce6ded2a`, +computed on the comma-joined sorted integer exponents. + +## 2. The word + +**Theorem.** Under the hypotheses above, frame 1 is hosted by a product of +root-line letters. The admissible letters are exactly the eight frame letters. +The hosting products are exactly the 149 subsets of those letters whose linear +parts span a fixed 4-dimensional space: none of length less than 4, then 56, +56, 28, 8, and 1 products of lengths 4 through 8. Every one of those 149 +products equals the same function + +```text +(1 + x1 + x3)(1 + x0 + x1 + x4)(1 + x1 + x2 + x5 + x6)(1 + x0 + x1 + x5 + x7). +``` + +The square-free support has 120 monomials. The degree counts are 1, 8, 27, 47, +and 37 in degrees 0 through 4. The 111 monomials of degree at least 2 are the +new charges for this row. Exactly 31 of them lie in the recorded 40. The other +80 are the additional charge once those 40 are already paid. Nine of the +recorded 40 do not occur in this polynomial. The joint degree-at-least-2 +support of the two words has 120 monomials. + +One hosting word, the lexicographically first length-4 subset in the frame +order, is the product of the letters of ports `13, 26, 131, 262`. + +The pairing matrix on the eight frame lines is the all-ones matrix and has +`F_2`-rank 1. That copy-cost is a different unit and is not added to the +monomial bill. + +## 3. The eight letters + +Write + +```text +p = x1 + x3, +q = x0 + x1 + x4, +r = x1 + x2 + x5 + x6, +s = x0 + x1 + x5 + x7, +``` + +and `P = 1 + p`, `Q = 1 + q`, `R = 1 + r`, `S = 1 + s`. The coefficient matrix +of `(p, q, r, s)` has columns `x3, x4, x2, x7` equal to the four standard basis +vectors, so these four forms are linearly independent. Their common zero `Z` has +16 points, and `PQRS` is the indicator of `Z`. + +The Cartan matrix mod 2, in the simple-root order, is + +```text +0 0 1 0 0 0 0 0 +0 0 0 1 0 0 0 0 +1 0 0 1 0 0 0 0 +0 1 1 0 1 0 0 0 +0 0 0 1 0 1 0 0 +0 0 0 0 1 0 1 0 +0 0 0 0 0 1 0 1 +0 0 0 0 0 0 1 0 +``` + +Each frame root solves uniquely against the simple basis. The odd coordinates, +which are the eight-bit labels, and the Cartan sums of those rows are: + +| Port | Odd coordinates | Sum of those Cartan rows | +|---:|---|---| +| 13 | 1, 3, 4, 5 | `x1 + x2 + x5 + x6` | +| 26 | 0, 4, 7 | `x2 + x3 + x5 + x6` | +| 131 | 0, 1, 3, 6 | `x1 + x3 + x4 + x5 + x7` | +| 148 | 5, 6, 7 | `x4 + x5 + x7` | +| 262 | 1, 2, 3, 4, 5, 6 | `x0 + x1 + x2 + x3 + x6 + x7` | +| 273 | 0, 2, 4, 6, 7 | `x0 + x2 + x6 + x7` | +| 392 | 0, 1, 2, 3 | `x0 + x1 + x4` | +| 415 | 2, 5, 7 | `x0 + x3 + x4` | + +The ninth label bit is 1, so the chart letter is 1 plus that linear form. In +the basis `(p, q, r, s)` the eight linear parts are + +```text +r, p + r, p + q + s, q + s, p + r + s, r + s, q, p + q. +``` + +Each has q-coefficient different from r-coefficient, and the eight tuples are +distinct. The set of vectors in `F_2^4` with that coefficient condition has +size 8, so these are all of them. Call that affine hyperplane `H`, and call +`W = {q-coefficient = r-coefficient}` the complementary linear hyperplane. + +The coordinate solves are eight invertible rational systems. `verify.py` +recomputes them and rejects a non-integral coordinate. The row sums above are +the letters once those bits are known. + +## 4. Which products host the row + +**Factor restriction.** A product equals 1 at a line only if every factor does. +Every root in this model has sum of squares 8, so the normalized dot of a root +with itself is 2 and every letter equals 1 on its own line. The 28 pairs of +distinct frame roots are orthogonal, which is checked pair by pair, so each +frame letter equals 1 on all eight frame lines. Thus every frame letter is +admissible. + +A letter outside the frame fails the same test. The eight frame labels span a +4-dimensional space `U`. Enumerating the orthogonal of `U` inside `F_2^8` +returns 16 vectors. Exactly eight of those vectors are eight-bit root-line +labels, and they are the frame labels. A root +label is annihilated by every form in `V = span{p, q, r, s}` exactly when it is +orthogonal to `U`, because the eight linear parts span `V` and each chart letter +is `1 + B(label, ·)`. The orthogonal census and the direct test of all 120 +letters agree: the admissible letters are the frame letters. Repetition does +not create a new `F_2` value, since every letter is idempotent. The nonempty +subsets of the eight letters therefore exhaust the hosting candidates. + +**Spanning criterion.** For a subset of these letters, the product equals 1 +exactly where every selected linear part vanishes. That common zero is `Z` if +and only if the selected vectors span `V`. The product is then the indicator of +`Z`, which is `PQRS`. If the vectors do not span `V`, the common zero has size +at least 32, so the product is a different function. + +**Length count.** This is a count of spanning subsets of `H` inside `F_2^4`. + +- No subset of size at most 3 spans a 4-dimensional space. +- `F_2^4` has 15 linear hyperplanes, one for each nonzero linear equation. One + of them is `W`, which misses `H`. Each of the other 14 meets `W` in a + 2-dimensional subspace and therefore meets `H` in `8 - 4 = 4` points. Those + four points are a coset of that 2-dimensional subspace, so they span a + 3-dimensional space and do not span `F_2^4`. +- The 14 four-point sets are distinct. If two distinct hyperplanes met `H` in + the same four points `S`, then `S` would equal their intersection, a linear + subspace. That subspace contains 0, and `H` does not. +- There are `C(8, 4) = 70` four-subsets, so 56 of them span `F_2^4`. +- A subset that does not span lies in some linear hyperplane. Inside `H` that + hyperplane contributes only four points. Every subset of size at least 5 + therefore spans. The counts are `C(8, 5) = 56`, `C(8, 6) = 28`, + `C(8, 7) = 8`, and `C(8, 8) = 1`. + +So the hosting products are 56 of length 4 and every subset of length at least +5. There are 149 of them, and each equals `PQRS` as a function on `F_2^8`. + +The lexicographically first length-4 mask, with bit `i` selecting the `i`-th +frame port, is `0b10111`, the ports `13, 26, 131, 262`. Their letters are +`R`, `1 + P + R`, `P + Q + S`, and `P + R + S`. The first two multiply to `PR`: + +```text +R(1 + P + R) = R(1 + P) + R^2 = R + PR + R = PR. +``` + +The last two multiply to `P + PR + PQ + QR + QS + SR + S`. Multiplying on the +left by `PR` cancels every term except `PQRS`. This is the same polynomial. +The spanning argument already covers the other 148 hosting products. + +`verify.py` evaluates all 255 nonempty pairing products on the 120 lines and +checks that the successful masks are exactly the spanning subsets, and that +each of those expansions equals `PQRS`. That loop is a complete pass over a +domain of size 255. It corroborates the identification of the letters. It is +not a sample. + +## 5. The flat meets the root lines in the frame + +`PQRS` equals 1 on a chart point exactly on `Z`. Evaluating it on the 120 +root-line labels returns exactly the eight frame labels. The domain of that +check is the full set of 120 lines. On root lines the function is therefore the +frame indicator. The eight ports lie in the P104 window, so the same statement +holds after restriction to the 104 lines. + +The support of the function on the whole chart is the 16-point flat `Z`, not +the indicator of eight points inside `F_2^8`. + +## 6. The bill + +Boolean multiplication of the four factors, reduced by `x_i^2 = x_i`, produces +120 monomials. The Möbius transform of the indicator of `Z` produces the same +set. The degree counts are + +```text +degree 0: 1, degree 1: 8, degree 2: 27, degree 3: 47, degree 4: 37. +``` + +The degree-1 monomials are `x0, x1, x2, x3, x4, x5, x6, x7`. The other 111 +monomials are the new charges. Their ANF hash, on the comma-joined sorted +exponents, is `df38586c54c752c2881df43e80653a9abffbaf5e49b9d76282919d3cf3c79765`. +The full 120-monomial hash is +`b2af6c2893e8104e3c9f54ce4db48f30f692c99f11ca877d81252ae5c36c0acd`. + +`Q`, `R`, and `S` do not use `x3`, while `P = (1 + x1) + x3`. The monomials +that contain `x3` are therefore `x3` times the monomials of `QRS`, disjoint +from the rest. Fifty-one of the 111 new monomials contain `x3`. The recorded +polynomial does not use `x3`, so all 51 lie outside the recorded 40 and inside +the additional charge. + +Of the 111 new monomials, the intersection with the recorded 40 has size 31, +degrees 16, 13, and 2 in degrees 2, 3, and 4. Hash +`2f7b63759f9780a1ae332df1ebbb987027c880cad97896fb39ebcb92194cc65b`. + +```text +x0*x1 x0*x2 x0*x4 x0*x5 x1*x5 x0*x1*x5 x2*x5 x0*x2*x5 x4*x5 x0*x4*x5 +x0*x6 x1*x6 x0*x1*x6 x4*x6 x0*x4*x6 x5*x6 x0*x5*x6 x1*x5*x6 x0*x1*x5*x6 x4*x5*x6 +x0*x7 x1*x7 x0*x1*x7 x2*x7 x0*x2*x7 x4*x7 x5*x7 x0*x5*x7 x1*x5*x7 x0*x1*x5*x7 x4*x5*x7 +``` + +The additional bill is the other 80, degrees 11, 34, and 35. Hash +`219f34e8bd473ae9927d0b6cb7d94c4b6de2b4c93f6b9c4c3b8355fdad4b13cb`. +Twenty-nine of them are free of `x3`; the other 51 contain `x3`. + +```text +x1*x2 x0*x1*x2 x0*x3 x1*x3 x0*x1*x3 x2*x3 x0*x2*x3 x1*x2*x3 +x1*x4 x0*x1*x4 x2*x4 x0*x2*x4 x1*x2*x4 x0*x1*x2*x4 x3*x4 x0*x3*x4 +x1*x3*x4 x0*x1*x3*x4 x2*x3*x4 x0*x2*x3*x4 x1*x2*x3*x4 x1*x2*x5 x0*x1*x2*x5 +x3*x5 x0*x3*x5 x1*x3*x5 x0*x1*x3*x5 x2*x3*x5 x0*x2*x3*x5 x1*x2*x3*x5 +x1*x4*x5 x0*x1*x4*x5 x2*x4*x5 x1*x2*x4*x5 x3*x4*x5 x0*x3*x4*x5 x2*x3*x4*x5 +x3*x6 x0*x3*x6 x1*x3*x6 x1*x4*x6 x0*x1*x4*x6 x3*x4*x6 x0*x3*x4*x6 x1*x3*x4*x6 +x3*x5*x6 x0*x3*x5*x6 x1*x3*x5*x6 x1*x4*x5*x6 x3*x4*x5*x6 +x1*x2*x7 x0*x1*x2*x7 x3*x7 x0*x3*x7 x1*x3*x7 x0*x1*x3*x7 x2*x3*x7 x0*x2*x3*x7 x1*x2*x3*x7 +x1*x4*x7 x2*x4*x7 x1*x2*x4*x7 x3*x4*x7 x1*x3*x4*x7 x2*x3*x4*x7 +x3*x5*x7 x0*x3*x5*x7 x1*x3*x5*x7 x1*x4*x5*x7 x3*x4*x5*x7 +x6*x7 x0*x6*x7 x1*x6*x7 x0*x1*x6*x7 x3*x6*x7 x0*x3*x6*x7 x1*x3*x6*x7 x4*x6*x7 x1*x4*x6*x7 x3*x4*x6*x7 +``` + +Nine recorded monomials are absent from frame 1, degrees 1, 4, and 4. Hash +`5ca7559ebd00485c0852a0f65479f721997ae1c8aaac9bbc2e4083a29da2c7bf`. + +```text +x2*x6 x0*x2*x6 x2*x5*x6 x0*x2*x5*x6 x0*x4*x5*x6 x0*x4*x7 x2*x5*x7 x0*x2*x5*x7 x0*x4*x5*x7 +``` + +The joint degree-at-least-2 support is the union of the 111 and these nine, so +it has size `111 + 9 = 120`. That count equals the number of monomials of the +frame-1 polynomial, and the two sets are different: the polynomial also +contains the constant and the eight degree-1 monomials, and it omits these +nine. The arithmetic identity `31 + 80 = 111` and `40 + 80 = 120` is the whole +comparison of the two charges. + +## 7. Evidence class + +The hosting classification, the length count, the equality of every spanning +product with `PQRS`, and the four-letter multiplication for ports +`13, 26, 131, 262` are proofs under the hypotheses in §1. The independence of +`p, q, r, s` and the idempotence used in the multiplication are part of those +proofs. + +The following are exhaustive finite censuses. Each domain is finite, every +element is tested, and the domain is the one named here. + +- The chart identity, on all 14,400 pairs of root lines. +- Pairwise orthogonality and the odd-graph condition, on all 28 pairs of frame + ports. +- The eight coordinate solves and the Cartan row sums. +- The admissible-letter test on all 120 lines, together with the 16-vector + orthogonal of the frame-label span. +- The agreement of all 255 subset products with the spanning prediction. +- The boolean expansion of `PQRS`, cross-checked by the Möbius transform of the + indicator of `Z` on all 256 chart points, and the evaluation of that function + on all 120 root-line labels. +- The comparison of the resulting degree-at-least-2 set with the 40 monomials + of the recorded closed form. + +These checks are not a heuristic and not an incomplete search inside this +alphabet. A failed search is not what is claimed. The length count is not being +inferred from a sample of words. + +## 8. What the bill does not decide + +The factor restriction uses products of root-line letters. A sum of such +products, a coordinate change, or a circuit that is not a product can be a +different hosting. This note gives no lower bound for those larger alphabets. +The 80 additional monomials are the exact remainder inside the product alphabet +and this chart, after the recorded 40 are paid. They are not a count of +Clifford routes, Gaussian children, or selected-invoice primitives. + +The selected frontier stays `781451/250000000`. Sharing 31 monomials makes the +algebraic union of these two rows smaller than the sum of the separate new +charges. That union is not a signed histogram, and frames 2 through 12 are not +expanded. The rank-1 pairing matrix is not part of the monomial bill. + +Frame partition: unpaidmoon, PR #7014. The recorded forty and the frame-0 +closed form: PR #7031. Ports and the odd-graph window: PR #6933. Prepared by +unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/p104-frame1-monomial-intersection/README.md b/research/p104-frame1-monomial-intersection/README.md new file mode 100644 index 0000000000..4a2e218495 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/README.md @@ -0,0 +1,133 @@ +# Frame 1 of the P104 window, and its overlap with the recorded forty + +**No new κ.** The selected frontier stays `781451/250000000`. This package hosts +frame 1 of the odd-character P104 window as a product of root-line labels, +charges every monomial of degree at least 2, and intersects that set with the +40 monomials recorded for frame 0. It does not host the other eleven rows and +it does not price a signed profile. + +## Result + +Frame 1 of the vendored 104-by-13 witness is the odd-graph clique + +```text +13, 26, 131, 148, 262, 273, 392, 415. +``` + +A letter is the pairing of one root line with all 120 root lines. In `F_2` a +product equals 1 only when every factor equals 1, so every factor of a hosting +word is identically 1 on these eight lines. The only such letters are the eight +frame letters. Their linear parts, in the inherited simple-root chart, are the +eight vectors of one affine hyperplane in a 4-dimensional space. A subset hosts +the row exactly when those vectors span the space. The hosting products are +therefore 56 words of length 4 and every subset of length 5, 6, 7, or 8. None +is shorter. Every one of the 149 products equals + +```text +(1 + x1 + x3)(1 + x0 + x1 + x4)(1 + x1 + x2 + x5 + x6)(1 + x0 + x1 + x5 + x7). +``` + +The lexicographically first length-4 word uses ports `13, 26, 131, 262`. The +square-free support has 120 monomials, with degree counts 1, 8, 27, 47, and 37. +The constant and all eight variables `x0, ..., x7` are the degree-at-most-1 +part. The other **111** monomials are the new charges for this row. + +The recorded forty are the degree-at-least-2 monomials of the frame-0 +polynomial from PR #7031, + +```text +(1 + x0)(1 + x1 + x2 + x4)(1 + x5)(1 + x6 + x7). +``` + +That expansion is locked by ANF hash +`26803d29aa3141a357da4aa551195fe6378d3f2e1cba0c4291a4dedbce6ded2a`. The frame-0 +census is not rerun. + +**Intersection:** 31 of the 111 lie in the recorded 40 (degrees 16, 13, 2). +**Additional bill:** the other 80 (degrees 11, 34, 35). Once the recorded 40 +are paid, frame 1 still charges these 80 monomials. Nine recorded monomials are +absent from frame 1. The joint degree-at-least-2 support of the two words has +120 monomials. Fifty-one of the 111 contain `x3`; the recorded polynomial does +not use `x3`, so all 51 are inside the additional 80. + +The names, hashes, and the proof of the hyperplane count are in +[PROOF.md](PROOF.md). The pairing matrix on the eight frame lines is the +all-ones matrix and has rank 1. That copy-cost is a different unit and is not +added to the monomial bill. + +## Evidence class + +The hosting classification, the length count, and the equality of every hosting +product with the four-factor polynomial are written proofs under the product +alphabet and this chart. The chart identity, the admissible-letter test, the +16-vector orthogonal, the 255 subset products, the boolean expansion, and its +Möbius cross-check are exhaustive finite censuses. Each domain is finite and +fully enumerated. This is not a heuristic and not an incomplete search inside +that alphabet. + +The same census gives no lower bound for a sum of letters, for another chart, +or for a circuit that is not a product. The 80 additional monomials are not a +selected-invoice histogram. The selected frontier stays `781451/250000000`. + +## 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. Open PR +[#7031](https://github.com/CrocSwap/integer-mult-bounds/pull/7031) hosts frame +0 and leaves, as its first open question, the hosting of frame 1 and the +intersection of the new monomials with the recorded 40. Scope is **changed** to +that question. The connection to the bottleneck is recorded in +[TASK.json](TASK.json): a later joint bill of two rows has to know which +monomials are shared, and this package stops at that intersection. + +`data/frames.json` is the frame partition from open PR #7014 (head +`949c0ada285aae619468ae49317c8d9f4df130f7`), the same bytes vendored by #7031, +hash `c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d`. This +package does not reprove the rank-13 factorisation and does not reprove the +frame-0 census. Ports and the E8 line map are the #6933 inputs pinned in +[SOURCES.json](SOURCES.json). + +Overlap was searched on 2026-11-10 against 339 open PR records, 7013 discussion +records, and the complete local note inventory at the base commit. The hits for +this question are #7031 and discussion comment 19514167, which state the +question and do not answer it. No open PR hosts frame 1. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B research/p104-frame1-monomial-intersection/verify.py +python3 -I -O -B research/p104-frame1-monomial-intersection/verify.py +python3 -B scripts/research_package.py --package research/p104-frame1-monomial-intersection +python3 -B scripts/check_research_commit.py --package research/p104-frame1-monomial-intersection --check-source-history +``` + +The verifier prints `PASS_P104_FRAME1_INTERSECTION` with +`word=13,26,131,262`, `new=111`, `intersection=31`, and `additional=80`. +Failure controls delete one canonical letter, count the 14 length-4 misses, +reject the rank-3 prefix, delete the constant monomial, and multiply by one +non-frame letter. + +Not run: the frame-0 product census, a sum-of-letters search, frames 2 through +12, the selected-supplier replay, `make frontier6030-verify`, and Lean. + +## Open next questions + +1. Host frame 2 of the same witness and intersect its degree-at-least-2 + monomials with the joint 120-monomial support of frames 0 and 1. The + two-row union is not yet a thirteen-row bill. The first step is the same + spanning test on `frames[2]`. Frames 2 through 12 are unexpanded here. +2. Can one circuit charge each of the 31 shared monomials once and still host + both rows? The intersection compares two separate expansions. It does not + exhibit a joint word. The first step is to take one hosting product from + each row and see whether a common subproduct realises exactly those 31 + monomials. + +## Credit + +Frame partition: unpaidmoon, PR #7014. Frame-0 hosting and the recorded forty: +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. diff --git a/research/p104-frame1-monomial-intersection/SOURCES.json b/research/p104-frame1-monomial-intersection/SOURCES.json new file mode 100644 index 0000000000..e0c65df5a4 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/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" + } + ] +} diff --git a/research/p104-frame1-monomial-intersection/TASK.json b/research/p104-frame1-monomial-intersection/TASK.json new file mode 100644 index 0000000000..7a764f4fa9 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Host frame 1 of the #7014 odd-character P104 window as a product of root-line labels, charge every degree-at-least-2 monomial, and intersect that set with the 40 monomials recorded for frame 0.", + "scope_change_reason": "The catalogue card asks whether a decoder or coframe change improves the full signed moment. Open PR #7031, question 1, asks a prior physical question: host frame 1 the same way as the frame-0 row and intersect its degree-at-least-2 monomials with the recorded 40. This package answers that question. It does not price a changed itinerary, so it cannot improve the signed moment.", + "bottleneck_link": "A joint signed bill of two frame rows needs the monomials they share. This package records the intersection of 31 and the additional charge of 80. Those sets are a prerequisite for pricing the two rows together. They are not a signed histogram and not a supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the frame-1 hosting word, its 111 new monomials, the intersection of 31, and the additional bill of 80. Do not host frames 2 through 12, do not search sums of letters, do not name #6030 primitives, and do not claim a kappa change.", + "outcome": "completed", + "evidence": "verify.py prints PASS_P104_FRAME1_INTERSECTION word=13,26,131,262 monomials=120 new=111 intersection=31 additional=80 joint=120. Evidence class: a written hosting classification by an affine hyperplane in F_2^4, plus exhaustive finite censuses of the chart identity, the admissible letters, the 255 subset products, and the boolean expansion of PQRS. The recorded 40 are the published frame-0 closed form, locked by its ANF hash; the frame-0 census is not rerun. Not a heuristic. Not a selected-profile comparison. Selected kappa remains 781451/250000000.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance. The chart identity, the 255-product agreement, the orthogonal census, and the polynomial expansion are rechecked by verify.py.", + "open_questions": [ + { + "question": "Which degree-at-least-2 monomials of frame 2 lie in the joint 120-monomial support of frames 0 and 1?", + "why_it_matters": "The two-row union is the first interaction between rows. It is not yet a bill for the other eleven frames of the witness.", + "first_step": "Repeat the spanning test and the boolean expansion on frames[2], then intersect the degree-at-least-2 monomials with the 120-monomial joint support recorded here.", + "blocked_by": "frames 2 through 12 are not expanded in this package" + }, + { + "question": "Can one circuit charge each of the 31 shared monomials once and still host both frame rows?", + "why_it_matters": "The intersection compares two separate expansions. A smaller joint bill needs a circuit that actually shares those monomials.", + "first_step": "Take one hosting product from each row and test whether a common subproduct realises exactly the 31 shared monomials while both indicators survive.", + "blocked_by": "this package does not build a joint circuit" + } + ] +} diff --git a/research/p104-frame1-monomial-intersection/VERIFY.json b/research/p104-frame1-monomial-intersection/VERIFY.json new file mode 100644 index 0000000000..3fdb885f4e --- /dev/null +++ b/research/p104-frame1-monomial-intersection/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-port-window-haemers/data/e8_line_map.json", + "research/p104-port-window-haemers/data/ports_p104.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Hosts frame 1 by the spanning criterion, checks the 255 pairing products, expands PQRS by multiplication and by the Mobius transform, and intersects the 111 degree-at-least-2 monomials with the recorded 40. Failure controls delete one canonical letter, count 14 length-4 misses, reject a rank-3 prefix, delete the constant monomial, and multiply by a non-frame letter. Prints PASS_P104_FRAME1_INTERSECTION with word=13,26,131,262, new=111, intersection=31, additional=80. Does not rerun the frame-0 census, does not replay the selected supplier, and does not change kappa." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same hosting, expansion, and intersection with isolated mode and assert stripping, confirming the checks are need() failures rather than assertions." + } + ] +} diff --git a/research/p104-frame1-monomial-intersection/data/frames.json b/research/p104-frame1-monomial-intersection/data/frames.json new file mode 100644 index 0000000000..793a32f489 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/data/frames.json @@ -0,0 +1,157 @@ +{ + "description": "Disjoint 8-cliques of the odd graph. frames partition the 104 P104 ports. excluded_odd_cliques are the two 8-cliques in the 120 weight-3-mod-4 vectors that P104 omits; together with frames they partition those 120 vectors. Integers are F_2^9 ports, bit i coordinate i.", + "frames": [ + [ + 11, + 21, + 38, + 56, + 140, + 146, + 161, + 191 + ], + [ + 13, + 26, + 131, + 148, + 262, + 273, + 392, + 415 + ], + [ + 14, + 69, + 164, + 239, + 276, + 351, + 446, + 501 + ], + [ + 19, + 41, + 74, + 112, + 280, + 290, + 321, + 379 + ], + [ + 22, + 37, + 196, + 247, + 268, + 319, + 478, + 493 + ], + [ + 28, + 49, + 133, + 168, + 265, + 292, + 400, + 445 + ], + [ + 35, + 81, + 176, + 194, + 274, + 352, + 385, + 499 + ], + [ + 44, + 84, + 152, + 224, + 304, + 328, + 388, + 508 + ], + [ + 50, + 70, + 138, + 254, + 259, + 375, + 443, + 463 + ], + [ + 73, + 98, + 208, + 251, + 324, + 367, + 477, + 502 + ], + [ + 88, + 100, + 193, + 253, + 322, + 382, + 475, + 487 + ], + [ + 134, + 145, + 200, + 223, + 416, + 439, + 494, + 505 + ], + [ + 261, + 296, + 336, + 381, + 386, + 431, + 471, + 506 + ] + ], + "excluded_odd_cliques": [ + [ + 7, + 25, + 42, + 52, + 76, + 82, + 97, + 127 + ], + [ + 67, + 104, + 137, + 162, + 266, + 289, + 448, + 491 + ] + ] +} diff --git a/research/p104-frame1-monomial-intersection/verify.py b/research/p104-frame1-monomial-intersection/verify.py new file mode 100644 index 0000000000..f1ba9747a1 --- /dev/null +++ b/research/p104-frame1-monomial-intersection/verify.py @@ -0,0 +1,514 @@ +#!/usr/bin/env python3 +"""Host frame 1 of the P104 odd-character window and intersect its new monomials. + +Frame 1 of the vendored 104-by-13 witness is hosted by a product of root-line +letters. Every hosting product equals one polynomial in the inherited +simple-root chart. That polynomial has 111 monomials of degree at least 2. +Thirty-one of them lie in the 40 monomials recorded for frame 0 by the closed +form in PR #7031. The other 80 are the additional charge of this row. + +The frame-0 product census is not rerun. The recorded 40 are the degree-at +least-2 part of the published expansion, locked by its ANF hash. No kappa +change. Standard library only. Checks are need() failures, so python -O still +runs them. +""" + +import hashlib +import json +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +REPO = ROOT.parents[1] +FRAMES_SHA256 = "c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d" +RECORDED_ANF_SHA256 = "26803d29aa3141a357da4aa551195fe6378d3f2e1cba0c4291a4dedbce6ded2a" +FRAME1_SHA256 = "b2af6c2893e8104e3c9f54ce4db48f30f692c99f11ca877d81252ae5c36c0acd" +NEW_SHA256 = "df38586c54c752c2881df43e80653a9abffbaf5e49b9d76282919d3cf3c79765" +INTERSECTION_SHA256 = "2f7b63759f9780a1ae332df1ebbb987027c880cad97896fb39ebcb92194cc65b" +ADDITIONAL_SHA256 = "219f34e8bd473ae9927d0b6cb7d94c4b6de2b4c93f6b9c4c3b8355fdad4b13cb" +ABSENT_SHA256 = "5ca7559ebd00485c0852a0f65479f721997ae1c8aaac9bbc2e4083a29da2c7bf" +CANONICAL_PORTS = (13, 26, 131, 262) +CANONICAL_MASK = 0b10111 +LENGTH_COUNTS = {1: 0, 2: 0, 3: 0, 4: 56, 5: 56, 6: 28, 7: 8, 8: 1} +DEGREE_COUNTS = {0: 1, 1: 8, 2: 27, 3: 47, 4: 37} +INTERSECTION_DEGREES = {2: 16, 3: 13, 4: 2} +ADDITIONAL_DEGREES = {2: 11, 3: 34, 4: 35} +ABSENT_DEGREES = {2: 1, 3: 4, 4: 4} +# Linear parts of the eight frame letters, in frame order. Every constant is 1. +LETTER_MASKS = (102, 108, 186, 176, 207, 197, 19, 25) +# Coordinates (p, q, r, s) of those linear parts. +LETTER_COORDINATES = ( + (0, 0, 1, 0), + (1, 0, 1, 0), + (1, 1, 0, 1), + (0, 1, 0, 1), + (1, 0, 1, 1), + (0, 0, 1, 1), + (0, 1, 0, 0), + (1, 1, 0, 0), +) +FORM_MASKS = {"p": 10, "q": 19, "r": 102, "s": 163} + + +def need(condition, message): + if not condition: + raise SystemExit(message) + + +def e8_roots(): + roots = [] + for left, right in combinations(range(8), 2): + for sign_left in (1, -1): + for sign_right in (1, -1): + vector = [0] * 8 + vector[left] = 2 * sign_left + vector[right] = 2 * sign_right + roots.append(tuple(vector)) + for signs in product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(tuple(signs)) + return roots + + +def simple_basis(): + basis = [ + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + ] + for index in range(1, 6): + vector = [0] * 8 + vector[index] = -2 + vector[index + 1] = 2 + basis.append(tuple(vector)) + return basis + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) // 4 + + +def cartan_mod2(basis): + return [[dot(basis[i], basis[j]) & 1 for j in range(8)] for i in range(8)] + + +def solve_coordinates(matrix, target): + rows = [[Fraction(entry) for entry in matrix[i]] + [Fraction(target[i])] for i in range(8)] + for column in range(8): + pivot = next(row for row in range(column, 8) if rows[row][column]) + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = 1 / rows[column][column] + rows[column] = [entry * scale for entry in rows[column]] + for row in range(8): + if row != column and rows[row][column]: + factor = rows[row][column] + rows[row] = [rows[row][col] - factor * rows[column][col] for col in range(9)] + solution = [rows[i][8] for i in range(8)] + need(all(entry.denominator == 1 for entry in solution), "root coordinates are not integral") + return tuple(int(entry) for entry in solution) + + +def pairing(form, left, right): + value = 0 + for i in range(8): + if (left >> i) & 1: + for j in range(8): + if (right >> j) & 1 and form[i][j]: + value ^= 1 + if (left >> 8) & 1 and (right >> 8) & 1: + value ^= 1 + return value + + +def bilinear(form, left, right): + value = 0 + for i in range(8): + if (left >> i) & 1: + for j in range(8): + if (right >> j) & 1 and form[i][j]: + value ^= 1 + return value + + +def label_of(root, matrix): + coordinates = solve_coordinates(matrix, root) + bits = 0 + for index, value in enumerate(coordinates): + if value & 1: + bits |= 1 << index + return bits | (1 << 8) + + +def negate(vector): + return tuple(-entry for entry in vector) + + +def root_lines(): + lines = [] + seen = set() + for root in e8_roots(): + key = root if root > negate(root) else negate(root) + if key not in seen: + seen.add(key) + lines.append(root) + need(len(lines) == 120, "expected 120 root lines") + need(len(e8_roots()) == 240, "expected 240 roots") + need(all(dot(root, root) == 2 for root in e8_roots()), "a root has norm squared other than 2") + return lines + + +def f2_rank(rows): + basis = {} + for row in rows: + value = row + while value: + pivot = value.bit_length() - 1 + if pivot in basis: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return len(basis) + + +def polynomial_multiply(left, right): + product = {} + for left_exp, left_coeff in left.items(): + for right_exp, right_coeff in right.items(): + exponent = left_exp | right_exp + product[exponent] = (product.get(exponent, 0) + left_coeff * right_coeff) & 1 + return {exponent: coeff for exponent, coeff in product.items() if coeff} + + +def linear_factor(mask, constant): + factor = {0: constant & 1} + for index in range(8): + if (mask >> index) & 1: + factor[1 << index] = (factor.get(1 << index, 0) + 1) & 1 + return {exponent: coeff for exponent, coeff in factor.items() if coeff} + + +def multiply_all(factors): + polynomial = {0: 1} + for factor in factors: + polynomial = polynomial_multiply(polynomial, factor) + return polynomial + + +def evaluate(polynomial, point): + value = 0 + for exponent in polynomial: + if (exponent & point) == exponent: + value ^= 1 + return value + + +def mobius_support(truth): + """Algebraic normal form of a boolean function, via the subset Möbius transform.""" + values = [1 if truth(point) else 0 for point in range(256)] + for index in range(8): + bit = 1 << index + for mask in range(256): + if mask & bit: + values[mask] ^= values[mask ^ bit] + return {mask for mask, coeff in enumerate(values) if coeff} + + +def monomial_name(exponent): + if exponent == 0: + return "1" + return "*".join("x{0}".format(index) for index in range(8) if (exponent >> index) & 1) + + +def digest(exponents): + payload = ",".join(str(exponent) for exponent in sorted(exponents)) + return hashlib.sha256(payload.encode()).hexdigest() + + +def letter_form(label, form): + mask = 0 + for index in range(8): + if pairing(form, label, 1 << index): + mask |= 1 << index + return mask, pairing(form, label, 1 << 8) + + +def load_inputs(): + frame_path = ROOT / "data" / "frames.json" + frame_bytes = frame_path.read_bytes() + need(hashlib.sha256(frame_bytes).hexdigest() == FRAMES_SHA256, "frames.json sha256 mismatch") + payload = json.loads(frame_bytes.decode()) + frames = payload["frames"] + need(len(frames) == 13 and all(len(frame) == 8 for frame in frames), "expected 13 frames of size 8") + covered = [port for frame in frames for port in frame] + need(len(covered) == len(set(covered)) == 104, "the 13 frames do not partition 104 ports") + ports = json.loads((REPO / "research/p104-port-window-haemers/data/ports_p104.json").read_text())["ports"] + line_map = json.loads((REPO / "research/p104-port-window-haemers/data/e8_line_map.json").read_text()) + vector_to_root = {vector: tuple(root) for vector, root in zip(line_map["vectors"], line_map["roots2"])} + need(len(ports) == 104 and len(set(ports)) == 104, "expected 104 distinct P104 ports") + need(set(covered) == set(ports), "the frame partition is not the P104 port set") + return frames, set(ports), vector_to_root + + +def build_labels(form, matrix, lines): + labels = [label_of(root, matrix) for root in lines] + need(len(set(labels)) == 120, "root-line labels are not distinct") + need(all((label >> 8) & 1 for label in labels), "a label is missing the ninth coordinate") + index = {} + for position, root in enumerate(lines): + index[root] = position + index[negate(root)] = position + mismatches = 0 + for left in range(120): + for right in range(120): + expected = (dot(lines[left], lines[right]) + 1) & 1 + if pairing(form, labels[left], labels[right]) != expected: + mismatches += 1 + need(mismatches == 0, "simple-root chart does not reproduce the label pairing") + return labels, index + + +def frame_geometry(frame, ports, vector_to_root, index): + need(set(frame) <= ports, "frame 1 is not contained in P104") + need(len(set(frame)) == 8, "frame 1 has a repeated port") + for left, right in combinations(frame, 2): + need((left & right).bit_count() & 1, "frame 1 is not an odd-graph clique") + need(dot(vector_to_root[left], vector_to_root[right]) == 0, "frame 1 roots are not pairwise orthogonal") + positions = [index[vector_to_root[port]] for port in frame] + need(len(set(positions)) == 8, "frame 1 does not use eight root lines") + return positions + + +def span_rank(vectors): + return f2_rank(vectors) + + +def coordinate_of(mask): + found = None + for code in range(16): + combined = 0 + for bit, name in enumerate(("p", "q", "r", "s")): + if (code >> bit) & 1: + combined ^= FORM_MASKS[name] + if combined == mask: + need(found is None, "a letter mask has two expressions in p, q, r, s") + found = code + need(found is not None, "a letter mask is outside span(p, q, r, s)") + return tuple((found >> bit) & 1 for bit in range(4)) + + +def predicted_hosting(coordinates): + counts = {length: 0 for length in range(1, 9)} + hosting = [] + for mask in range(1, 256): + selected = [coordinates[bit] for bit in range(8) if (mask >> bit) & 1] + # Pack coordinates as 4-bit integers, bit 0 = p through bit 3 = s. + rows = [sum(coord << index for index, coord in enumerate(vector)) for vector in selected] + if span_rank(rows) == 4: + counts[mask.bit_count()] += 1 + hosting.append(mask) + return counts, hosting + + +def product_values(rows, mask): + values = [1] * 120 + for letter, row in enumerate(rows): + if (mask >> letter) & 1: + for point in range(120): + values[point] &= row[point] + return values + + +def expand_mask(mask, forms): + factors = [linear_factor(*forms[letter]) for letter in range(8) if (mask >> letter) & 1] + return multiply_all(factors) + + +def recorded_polynomial(): + factors = ( + linear_factor(1 << 0, 1), + linear_factor((1 << 1) | (1 << 2) | (1 << 4), 1), + linear_factor(1 << 5, 1), + linear_factor((1 << 6) | (1 << 7), 1), + ) + return multiply_all(factors) + + +def frame1_polynomial(): + factors = ( + linear_factor((1 << 1) | (1 << 3), 1), + linear_factor((1 << 0) | (1 << 1) | (1 << 4), 1), + linear_factor((1 << 1) | (1 << 2) | (1 << 5) | (1 << 6), 1), + linear_factor((1 << 0) | (1 << 1) | (1 << 5) | (1 << 7), 1), + ) + return multiply_all(factors) + + +def orthogonal_root_labels(form, labels, frame_labels): + span = {0} + for label in frame_labels: + span |= {known ^ (label & 255) for known in span} + need(len(span) == 16, "frame labels do not span a 4-dimensional space") + need(f2_rank(label & 255 for label in frame_labels) == 4, "frame-label rank is not 4") + orthogonal = [ + candidate for candidate in range(256) + if all(bilinear(form, candidate, label & 255) == 0 for label in frame_labels) + ] + need(len(orthogonal) == 16, "the frame-label orthogonal does not have 16 vectors") + label_set = {label & 255 for label in labels} + return [candidate for candidate in orthogonal if candidate in label_set] + + +def run_controls(letter_rows, positions, polynomial, forms, outside_row, intersection, absent): + target = tuple(1 if point in set(positions) else 0 for point in range(120)) + dropped = CANONICAL_MASK ^ (1 << (CANONICAL_MASK.bit_length() - 1)) + need(tuple(product_values(letter_rows, dropped)) != target, "deleting one canonical letter still hosts the row") + failures = [ + mask for mask in range(256) + if mask.bit_count() == 4 and tuple(product_values(letter_rows, mask)) != target + ] + need(len(failures) == 14, "length-4 failure count is not 14") + need(tuple(product_values(letter_rows, 0b1111)) != target, "the rank-3 prefix still hosts the row") + without_constant = {exponent: coeff for exponent, coeff in polynomial.items() if exponent} + need( + any(evaluate(without_constant, point) != evaluate(polynomial, point) for point in range(256)), + "deleting the constant monomial did not change the chart function", + ) + need(any(outside_row[point] == 0 for point in positions), "a non-frame letter is 1 on every frame line") + canonical_values = product_values(letter_rows, CANONICAL_MASK) + killed = [canonical_values[point] & outside_row[point] for point in range(120)] + need(killed != list(target), "multiplying the canonical word by a non-frame letter still hosts the row") + extended = CANONICAL_MASK | (1 << 3) + need(expand_mask(extended, forms) == polynomial, "adding one more frame letter changed the polynomial") + need(3 in intersection, "x0*x1 left the intersection") + need(digest(exponent for exponent in intersection if exponent != 3) != INTERSECTION_SHA256, + "deleting x0*x1 left the intersection hash unchanged") + need(68 in absent and 68 not in polynomial, "x2*x6 is not an absent recorded monomial") + + +def main(): + frames, ports, vector_to_root = load_inputs() + basis = simple_basis() + matrix = list(zip(*basis)) + form = cartan_mod2(basis) + lines = root_lines() + labels, index = build_labels(form, matrix, lines) + frame = tuple(frames[1]) + positions = frame_geometry(frame, ports, vector_to_root, index) + forms = [letter_form(labels[source], form) for source in positions] + need([mask for mask, _constant in forms] == list(LETTER_MASKS), "frame-1 letter masks changed") + need(all(constant == 1 for _mask, constant in forms), "a frame-1 letter has constant term 0") + coordinates = [coordinate_of(mask) for mask, _constant in forms] + need(tuple(coordinates) == LETTER_COORDINATES, "frame-1 coordinates in p, q, r, s changed") + need(all(vector[1] ^ vector[2] == 1 for vector in coordinates), "a frame-1 vector left the affine hyperplane") + need(len(set(coordinates)) == 8, "the eight coordinate vectors are not distinct") + counts, hosting = predicted_hosting(coordinates) + need(counts == LENGTH_COUNTS, "span census counts changed: {0}".format(counts)) + need(sum(counts[length] for length in range(1, 4)) == 0, "a spanning set shorter than 4 exists") + canonical = min(mask for mask in hosting if mask.bit_count() == 4) + need(canonical == CANONICAL_MASK, "canonical mask changed: {0}".format(canonical)) + ports_used = tuple(frame[letter] for letter in range(8) if (canonical >> letter) & 1) + need(ports_used == CANONICAL_PORTS, "canonical word ports changed: {0}".format(ports_used)) + + letter_rows = [ + [pairing(form, labels[source], labels[point]) for point in range(120)] for source in positions + ] + target = tuple(1 if point in set(positions) else 0 for point in range(120)) + observed = [] + for mask in range(1, 256): + if tuple(product_values(letter_rows, mask)) == target: + observed.append(mask) + need(observed == hosting, "the pairing products and the spanning subsets disagree") + admissible = [ + position for position, label in enumerate(labels) + if all(pairing(form, label, labels[point]) == 1 for point in positions) + ] + need(set(admissible) == set(positions), "the letters equal to 1 on the frame are not exactly the frame") + orthogonal_hits = orthogonal_root_labels(form, labels, [labels[point] for point in positions]) + need( + set(orthogonal_hits) == {labels[point] & 255 for point in positions}, + "the frame-label orthogonal meets the root labels outside the frame", + ) + + polynomial = frame1_polynomial() + expansions = [expand_mask(mask, forms) for mask in hosting] + need(all(expansion == polynomial for expansion in expansions), "a hosting product differs from the four-factor form") + flat = mobius_support(lambda point: all(evaluate(linear_factor(FORM_MASKS[name], 0), point) == 0 for name in ("p", "q", "r", "s"))) + need(set(polynomial) == flat, "boolean multiplication disagrees with the Möbius transform of the flat") + need(len([point for point in range(256) if evaluate(polynomial, point)]) == 16, "chart support is not the 16-point flat") + label_hits = [point for point in range(120) if evaluate(polynomial, labels[point] & 255)] + need(label_hits == sorted(positions), "on root lines the word is not the frame indicator") + direct = product_values(letter_rows, canonical) + need(all(direct[point] == target[point] for point in range(120)), "direct product disagrees with the indicator") + port_of = {root: port for port, root in vector_to_root.items()} + port_of.update({negate(root): port for port, root in vector_to_root.items()}) + p104_hits = [ + point for point in range(120) + if port_of[lines[point]] in ports and evaluate(polynomial, labels[point] & 255) + ] + need(sorted(p104_hits) == sorted(positions), "on P104 the word is not the frame indicator") + + exponents = tuple(sorted(polynomial)) + need(digest(exponents) == FRAME1_SHA256, "frame-1 ANF sha256 mismatch") + degrees = dict(Counter(exponent.bit_count() for exponent in exponents)) + need(degrees == DEGREE_COUNTS, "degree counts changed: {0}".format(degrees)) + new_monomials = [exponent for exponent in exponents if exponent.bit_count() >= 2] + need(len(new_monomials) == 111, "new monomial count is not 111") + need(digest(new_monomials) == NEW_SHA256, "new-monomial sha256 mismatch") + with_x3 = [exponent for exponent in new_monomials if exponent & (1 << 3)] + need(len(with_x3) == 51, "the x3 part of the new bill is not 51") + + recorded = recorded_polynomial() + need(digest(sorted(recorded)) == RECORDED_ANF_SHA256, "recorded frame-0 ANF sha256 mismatch") + need(len(recorded) == 48, "recorded expansion does not have 48 monomials") + recorded_new = [exponent for exponent in sorted(recorded) if exponent.bit_count() >= 2] + need(len(recorded_new) == 40, "recorded new-monomial count is not 40") + need(all(exponent & (1 << 3) == 0 for exponent in recorded), "the recorded polynomial uses x3") + intersection = [exponent for exponent in new_monomials if exponent in recorded] + additional = [exponent for exponent in new_monomials if exponent not in recorded] + absent = [exponent for exponent in recorded_new if exponent not in polynomial] + need(len(intersection) == 31 and len(additional) == 80 and len(absent) == 9, "bill sizes changed") + need(digest(intersection) == INTERSECTION_SHA256, "intersection sha256 mismatch") + need(digest(additional) == ADDITIONAL_SHA256, "additional-bill sha256 mismatch") + need(digest(absent) == ABSENT_SHA256, "absent-monomial sha256 mismatch") + need( + dict(Counter(exponent.bit_count() for exponent in intersection)) == INTERSECTION_DEGREES, + "intersection degree counts changed", + ) + need( + dict(Counter(exponent.bit_count() for exponent in additional)) == ADDITIONAL_DEGREES, + "additional degree counts changed", + ) + need(dict(Counter(exponent.bit_count() for exponent in absent)) == ABSENT_DEGREES, "absent degree counts changed") + need(set(with_x3) <= set(additional), "a monomial containing x3 met the recorded 40") + need(len(set(new_monomials) - set(with_x3)) == 60, "the x3-free part of the new bill is not 60") + need(len(set(new_monomials) | set(recorded_new)) == 120, "joint degree-at-least-2 bill is not 120") + degree_one = [exponent for exponent in exponents if exponent.bit_count() == 1] + need(degree_one == [1, 2, 4, 8, 16, 32, 64, 128], "frame 1 does not use every degree-1 variable") + + support_rows = [] + for left in range(8): + mask = 0 + for right, point in enumerate(positions): + if letter_rows[left][point]: + mask |= 1 << right + support_rows.append(mask) + need(support_rows == [0xFF] * 8, "the frame pairing is not the all-ones matrix") + need(f2_rank(support_rows) == 1, "the frame support does not have pairing rank 1") + outside = next(point for point in range(120) if point not in set(positions)) + outside_row = [pairing(form, labels[outside], labels[point]) for point in range(120)] + run_controls(letter_rows, positions, polynomial, forms, outside_row, set(intersection), set(absent)) + print( + "PASS_P104_FRAME1_INTERSECTION word={word} monomials=120 new=111 " + "intersection=31 additional=80 joint=120 absent_from_frame1=9 " + "support_pairing_rank=1".format(word=",".join(str(port) for port in ports_used)) + ) + print("INTERSECTION " + " ".join(monomial_name(exponent) for exponent in intersection)) + print("ADDITIONAL " + " ".join(monomial_name(exponent) for exponent in additional)) + print("ABSENT " + " ".join(monomial_name(exponent) for exponent in absent)) + + +if __name__ == "__main__": + main()