Classify six once-each signed frames: support, but no word

research/six-signed-once-support/PROOF.md

@@ -0,0 +1,195 @@
+# Six once-each signed frames meet support and miss every word
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Claim
+
+In the PR2085/2112 formal register model, let `F1,...,F6` be nonzero symmetric rational rank-one matrices with
+
+```
+F1 + ... + F6 = 4I
+```
+
+and with no old call. Target support is possible. Every solution is, after relabeling the six frames, the old quadruple `{A,B,P,Q}` together with a rational rank-one splitting of the remaining `2I`. Every such solution fails the inherited character inequality, so none of them is a word.
+
+The selected record stays κ = `781451/250000000`. This does not lower the eight-call minimum. Five frames plus one old call, six frames plus an old call, and seven or more added frames are untouched. The five-frame count `116280` does not carry over: the allowed subset sizes here are 2, 3, and 4.
+
+## 1. Inherited facts
+
+Addresses are rational symmetric 2-by-2 matrices. A coefficient vector `(a,b,c)` means `aA+bB+cP`, with trace `a+b+c` and
+
+```
+Q(a,b,c) = 2ab + c(a+b) = 2 det.
+```
+
+The matrix is nonzero and rank one exactly when the vector is nonzero and `Q = 0`. The old frames are `A=(1,0,0)`, `B=(0,1,0)`, `P=(0,0,1)`, and `Q=A+B-P=(1,1,-1)`. The four targets, each of trace 2 and determinant `1/2`, are
+
+```
+AP=(1,0,1), AQ=(2,1,-1), BP=(0,1,1), BQ=(1,2,-1).
+```
+
+Their sum is `4I=(4,4,0)`. The determinant identity and the subset-sum necessity are inherited from `research/bit-two-signed-frame-floor`, Section 1, and are not reproved. In particular, with no old call the paid addresses sum to `4I`, and each target is a subset sum of those addresses, each address used at most once. For an additive character `χ` of the group generated by `A,B,P` and the six addresses,
+
+```
+(number of calls detected by χ) >= (number of targets detected by χ).
+```
+
+That inequality is not reproved here.
+
+## 2. The shortest equation, and which subset sizes can occur
+
+Six new labels, each used once, with no old call, give the determinant equation `F1+...+F6 = 4I`.
+
+**Lemma 1.** A subset that sums to a target has size 2, 3, or 4.
+
+The empty sum is 0. A single frame has determinant 0, not `1/2`. The sum of all six frames is `4I`, whose trace is 8, not 2. A five-frame subset leaves one frame equal to `4I-H`. For a target `H`,
+
+```
+det(4I-H) = 16 - 4·trace(H) + det(H) = 17/2 ≠ 0,
+```
+
+so `4I-H` is not rank one. Sizes 2, 3, and 4 remain. There are `C(6,2)+C(6,3)+C(6,4) = 50` such subsets. The four targets are distinct, so the four subsets are distinct. The domain is the `C(50,4) = 230300` unordered 4-tuples, each with `4! = 24` assignments of the targets.
+
+## 3. Support is attained, and the trace-2 family is not a word
+
+**Proposition 2.** The addresses
+
+```
+A, P, B, Q, 2A, 2B
+```
+
+are nonzero and rank one, sum to `4I`, and realize the four targets as `A+P`, `A+Q`, `B+P`, and `B+Q`. The same is true of `A,B,P,Q,2P,2Q`.
+
+These are support witnesses. They are not words: `χ(a,b,c)=a+b mod 2` detects `A` and `B` only, while it detects all four targets. The count is 2 against 4.
+
+The witnesses sit in a larger family. Suppose four of the frames are `{A,B,P,Q}`, which sum to `2I`, and the other two are `G` and `H=2I-G`. Expanding gives the polynomial identity
+
+```
+Q(2I-G) = 8 - 4·trace(G) + Q(G).
+```
+
+Thus if `G` is rank one, `H` is rank one if and only if `trace(G)=2`. Both then have trace 2, so neither is zero. Every such pair meets target support, because the four targets are already subset sums of `{A,B,P,Q}`.
+
+**Proposition 3.** Every rational rank-one `G` of trace 2 has an odd positive integer `D` with `D·G` in `2Λ`, where `Λ` is the integer lattice of coefficient vectors. Consequently every character `Λ+ZG → F2` vanishes on `G` and on `2I-G`.
+
+Write `p=a+b` and `c=2-p`. Rank one says `2ab=p(2-p)`, so `(a-b)^2 = p(4-p)`. Set `s=p-2` and `u=a-b`. Then `s^2+u^2=4`. The rational points are `s=-2`, which is `G=2P`, and
+
+```
+s = 2(1-v^2)/(1+v^2),  u = 4v/(1+v^2)
+```
+
+for `v` rational. Hence `p=4/(1+v^2)`, `c=2(v^2-1)/(1+v^2)`, and
+
+```
+a = 2(1+v)/(1+v^2),  b = 2(1-v)/(1+v^2).
+```
+
+Clear `v=r/t` in lowest terms and set `D=r^2+t^2`. Then
+
+```
+D·G = (2t(t+r), 2t(t-r), 2(r^2-t^2)),
+```
+
+which lies in `2Λ`. If `D` is odd we are done. If `D` is even then `r` and `t` are both odd, so `D/2` is odd, `t+r` and `t-r` are even, and `(D/2)·G` lies in `2Λ`. The point `2P` is already in `2Λ`. Replacing `v` by `-v` swaps `a` and `b`.
+
+Let `D'` be that odd multiplier, and let `χ` be any character of `Λ+ZG`. Then `χ(D'G)=D'χ(G)=χ(G)` in `F2`, while `D'G` is in `2Λ`, so `χ(G)=0`. The same holds for `H`, because `H+G=2I` and `χ(2I)=0`. The extension exists: if `nG` lies in `Λ`, then `D'(nG)` lies in `2Λ`, and `D'` odd forces `χ(nG)=0`.
+
+**Proposition 4.** On this family, `χ_AB(a,b,c)=a+b mod 2` detects two calls and four targets.
+
+It detects `A` and `B`, and neither `P` nor `Q=A+B-P`. It detects every target, because each target has odd `a+b`. The two padding frames contribute nothing, by Proposition 3. The inherited inequality forbids a word.
+
+So the family meets support and contains no word. Sections 4 through 7 show it is the whole support locus.
+
+## 4. Orbits and degree-1 certificates
+
+Column relabeling does not change the existence of a rank-one solution. For a 4-tuple of subsets, let `K` be the lexicographically least 4-tuple obtained by reordering the six columns so that their degrees are nonincreasing, ties included. The set of such reorderings is constant on an `S6`-orbit, and `K` itself lies in the orbit, so the fibers of `K` are exactly the orbits. There are 658 orbits.
+
+For one representative of each orbit and each of the 24 target assignments, row-reduce the 5-by-6 incidence matrix whose rows are the four subset indicators and a final row of ones. The right-hand side is the four targets and `(4,4,0)`. A free kernel vector `k` contributes an unknown `T` in `Q^3`, and frame `j` is `P_j + k_j T`. Each frame then imposes one quadric.
+
+**Proposition 5.** Outside the two orbits of Sections 5 and 6, every consistent assignment has degree-at-most-1 multipliers `m_j` with `Σ m_j Q(F_j) = 1` in the polynomial ring. There is therefore no rational, or even complex, solution.
+
+The census is 4,224 inconsistent systems, 11,472 systems of nullity 1 with such a certificate, and 80 systems of nullity 2 with such a certificate. The verifier finds the multipliers by linear algebra and re-expands the product, so the identity does not depend on trusting the row reduction. A constant nonzero quadric, from a frame frozen off the rank-one cone, is the special case of a degree-0 multiplier. The two exceptional orbits are the degree-sorted minima of
+
+```
+(3,5,10,12) = {{0,1},{0,2},{1,3},{2,3}}
+(7,11,21,25) = {{0,1,2},{0,1,3},{0,2,4},{0,3,4}}.
+```
+
+No other orbit fails to produce the constant 1.
+
+## 5. The four-cycle
+
+For masks `(3,5,10,12)`, columns 4 and 5 lie in no subset. Exactly eight target assignments are consistent. In each of them the kernel splits as one vector supported on the four used columns and one vector supported on the two padding columns. The used frames are an affine line `P_j + k_j T`. Exactly one of the four old frames, tried as the value of `T`, makes those four frames equal to `{A,B,P,Q}`. The four used quadrics then contain each coordinate polynomial `T_i - (T0)_i`: degree-at-most-1 multipliers re-expand to that linear polynomial. The used frames are therefore exactly `{A,B,P,Q}` and nothing else. Their sum is `2I`.
+
+The padding kernel is a line `G`, `2I-G`. Both quadrics and the identity of Section 3 force `trace(G)=2` and `Q(G)=0`. This is the family of Propositions 2 through 4. The witness masks `(3,6,9,12)` have the same orbit key, so the explicit witness is this orbit.
+
+## 6. Four triples through one frame
+
+For masks `(7,11,21,25)` the degrees are `(4,2,2,2,2,0)`. Column 0 lies in every triple and column 5 lies in none. Adding the four triple equations and comparing with the total gives `F5 = F0 + 2I` on every consistent assignment; the verifier checks that the particular solution and both kernel vectors satisfy it. The identity
+
+```
+Q(2I+F) = Q(F) + 4·trace(F) + 8
+```
+
+then says that rank one of both `F0` and `F5` forces `trace(F0)=-2`.
+
+Exactly eight assignments are consistent. They are one assignment, its swap of the two equation pairs, and the images of those two under the linear involutions
+
+```
+σ(a,b,c) = (b,a,c),  τ(a,b,c) = (a+c, b+c, -c).
+```
+
+Both preserve `Q`, fix `4I`, and permute the four targets. `σ` exchanges the sign of `B-A`. `τ` exchanges the sign of `Q-P`. It is enough to rule out the two representatives
+
+```
+(AP, AQ, BP, BQ)  and  (AP, BP, AQ, BQ).
+```
+
+**First representative.** Write `W=(x,y,z)` for the frame paired with the common frame in the first two triples, and let the third triple differ from the first by `Δ=(-1,1,0)`. Then
+
+```
+Q(W+Δ) - Q(W) = 2(x-y-1).
+```
+
+Both quadrics vanish only if `x=y+1`. The cone equation becomes `2y(y+1)+z(2y+1)=0`. At `y=-1/2` this is `-1/2`, so `y≠-1/2` and `z=-2y(y+1)/(2y+1)`. Impose trace `-2` and rank one on the common frame, and write `p` for the sum of its first two coordinates. The two remaining quadrics clear to equations linear in `p`. Their coefficient determinant is `-4f(y)`, where
+
+```
+f(y) = 2(y^2-y)^2 + 4y + 1.
+```
+
+For `y>=0`, `f(y)>=1`. For `t>0`, `f(-t)=k(t)` with
+
+```
+k(t) = 2t^4 + 4t^3 + 2t^2 - 4t + 1,  m(t) = 2t^3 + 3t^2 + t - 1,
+k(t) = (t + 1/2) m(t) + (1/2)(3 - 7t - t^2).
+```
+
+The derivative `m'(t)=6t^2+6t+1` has negative roots, because its discriminant is 12, the sum of the roots is `-1`, and their product is `1/6`. Thus `m` is increasing on `[0,∞)`. Since `m(1/3)<0` and `m(2/5)>0`, the unique nonnegative root `t0` lies in `(1/3, 2/5)`. There `k` equals the remainder, which is decreasing and at least its value `1/50` at `2/5`. So `f` has no real root. The denominator `2y+1` was the only point removed, and it is not a solution. This representative has no real solution.
+
+**Second representative.** The same subtraction with `Δ=(1,1,-2)` gives `Q(W+Δ)-Q(W)=2(z-1)`, so `z=1`. Then `2xy+x+y=0`, or `(2x+1)(2y+1)=1`. The value `x=-1/2` makes the cone equation `-1/2`, so `y=-x/(2x+1)`. The common frame runs over the circle `(a+1)^2+(b+1)^2=2` with `c=-2-a-b`. Stereographic projection from `(a,b)=(0,-2)` gives, for finite rational or real `v`,
+
+```
+a = -2(1+v)/(1+v^2),  b = -2v(1+v)/(1+v^2),
+```
+
+and every circle point except `(0,-2,0)` arises this way: if `s=a+1≠1`, the slope `v=(1-t)/(1-s)` with `t=b+1` reproduces the point, which the verifier checks by reducing the cleared identities on `s^2+t^2=2`. The missing point `F=(0,-2,0)` makes the two remaining cleared quadrics `2(1-x)(5x+2)` and `-2x(7x+3)`. The second vanishes at `0` and `-3/7`, and the first does not.
+
+For every finite `v`, the two remaining quadrics clear to polynomials `qY,qZ` in `(x,v)`, each exactly divisible by the extraneous factor `2x+1`. Euclidean algorithm on the quotients leaves a remainder in `v` alone,
+
+```
+122880 + 1613824 v^2 + ... + 2580480 v^30,
+```
+
+with every coefficient positive and only even powers. It has no real root. Thus the quotients have no common root, `x=-1/2` is not a solution, and this representative has no real solution either.
+
+The eight assignments are therefore empty over the reals, hence over the rationals.
+
+## 7. Conclusion
+
+Every rational support solution belongs to one of the 658 orbits. Every orbit except the four-cycle is empty over the rationals, by a re-expanded degree-1 certificate or by Section 6. Every four-cycle solution is the family of Section 3, up to order of the frames. Every member of that family fails `χ_AB`. Therefore six once-each rank-one frames with no old call can meet target support, and no such tuple is a word.
+
+The certificate shows there is no solution of the quadrics in the nonexceptional orbits, so it is not a search that might have missed a rational point. The two exceptional orbits are solved by identities, not by sampling. The explicit addresses in Proposition 2 are witnesses of support only.
+
+## What this does not say
+
+A character count of 2 against 4 uses the six-call equation and the residual `4I`. It says nothing about five added frames plus one old call, about six frames plus an old call, or about seven or more added frames. It does not change κ. No predecessor theorem is reopened: the four-frame support proof, the five-frame support proof, and the three-frame character stay as they are.

research/six-signed-once-support/README.md

@@ -0,0 +1,46 @@
+# Six once-each signed frames
+
+**Support is attained. No word, and no new κ.**
+
+The shortest determinant equation in six new labels, each used once and with no old call, is `F1+...+F6 = 4I`. Target support is possible: the addresses `A,P,B,Q,2A,2B` are nonzero and rank one, sum to `4I`, and realize the four targets as pair sums. The same holds for every rational rank-one splitting of the remaining `2I` after `{A,B,P,Q}`.
+
+None of those solutions is a word. The character `a+b mod 2` detects two calls and all four targets. The argument that this is the entire support locus is an exhaustive census of the 230,300 subset systems, written in [PROOF.md](PROOF.md). The selected record stays κ = `781451/250000000`.
+
+## Scope and evidence
+
+Original card: `bit-new-register-model`, with `scope_status: changed`. The card asks for a larger or nonabelian native alphabet. This package stays in the abelian symmetric 2-by-2 model and answers the six-frame question left open by the five-frame note, discussion comment 19514165. It is a scoped local result on that handoff. It does not open another construction round, and it does not redo the four-frame or five-frame support proofs.
+
+Evidence classes, kept apart:
+
+1. **Exhaustive finite census, hence a proof of the support classification.** Lemma 1 limits subset size to 2, 3, or 4, so there are 50 subsets and 230,300 unordered 4-tuples. Column relabeling gives 658 orbits. Outside two orbits, all 15,776 other assignment systems are linearly inconsistent or have a degree-1 Nullstellensatz certificate of 1, re-expanded by the verifier. The four-cycle orbit is exactly `{A,B,P,Q}` plus a trace-2 rank-one splitting of `2I`. The four-triple orbit has no real point.
+2. **Hand character obstruction on that locus.** Every rational member of the family is killed by `χ_AB`, extended by zero on the padding. The inequality is inherited and not reproved. The hypotheses are six once-each rank-one frames, no old call, and residual `4I`.
+3. **Explicit support witness, not a word.** `A,P,B,Q,2A,2B` meets support and has character counts 2 and 2. A witness is only a witness of support.
+
+The five-frame domain of 116,280 tuples does not carry over. Predecessor replays, Lean, Docker, and the selected-result cold replay were not run.
+
+Source commits, Git blobs, and SHA256 pins are in [SOURCES.json](SOURCES.json). The selected record and catalogue are historical provenance. Full Git history is needed to resolve those pins.
+
+## Reproduce
+
+From the repository root, with Python 3.12:
+
+```sh
+python3 scripts/research_package.py --package research/six-signed-once-support --check-only
+python3.12 scripts/research_package.py --package research/six-signed-once-support
+```
+
+The direct check is `python3 -I -W error -B research/six-signed-once-support/verify.py`. It reruns the orbit census and the certificate expansions. On this machine that takes about 35 seconds.
+
+## Open next questions
+
+Can five added signed rank-one frames plus one old call meet support at length 6? The six-frame census uses the residual `4I`. One old call replaces that residual, so neither the size cut nor the character count applies. A useful first step is one old projector `E` and the equation on five new frames summing to `4I-E`.
+
+Can seven or more added frames, or six frames plus an old call, lower the eight-call minimum? Both change the number of free addresses or the residual. No such equation is solved here.
+
+A support solution is not a word. On the locus above, the character obstruction is complete for six once-each frames with no old call.
+
+## Credit
+
+The register model is Cinna Davis's PR2085/2112 formal model. The determinant and the subset-sum necessity are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR6190. The four-frame support proof is merged PR #6952, discussion comment 19507121. The five-frame support proof, whose open question this answers, is open PR #7024, discussion comment 19514165. The three-frame all-old-once character is `research/three-signed-old-once` and is not redone.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review. New work is Apache-2.0.

research/six-signed-once-support/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}