Character-exclude the all-old-once three signed frames

research/three-signed-old-once/PROOF.md

@@ -0,0 +1,312 @@
+# Three signed frames, all old labels once, are character-excluded
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Claim
+
+In the PR2085/2112 formal register model, the seven-call count profile
+
+```
+(a,b,p,q,r,s,t) = (1,1,1,1,1,1,1)
+```
+
+admits no word. The reason is a character: every solution of `R+S+T = 2I` by three nonzero symmetric rational rank-one matrices admits an additive character `Λ → F2` that detects two calls and four targets.
+
+This is a scoped proof for that one profile. It does not change the selected κ `781451/250000000`, it does not exhibit a word, and it does not treat the other twenty three-frame census profiles or four-or-more added frames.
+
+The first-order inequality "detected calls ≥ detected targets" is inherited from the normalization recorded in `research/bit-two-signed-frame-floor/PROOF.md`, Section 1 (itself from PR2910). This file does not reprove that inequality. The new argument is the existence of the character.
+
+## 1. Setup
+
+Addresses are rational symmetric 2-by-2 matrices. Write
+
+```
+A = diag(1,0),  B = diag(0,1),
+P = [[1,1],[1,1]]/2,  Q = [[1,-1],[-1,1]]/2.
+```
+
+Then `A+B = P+Q = I`. A general element of the `Q`-span of `A,B,P` has coefficient vector `(a,b,c)` and matrix
+
+```
+[[a + c/2, c/2], [c/2, b + c/2]].
+```
+
+Its trace is `a+b+c` and its determinant is `ab + c(a+b)/2`. The matrix is nonzero and rank one exactly when that determinant is zero and the vector is nonzero.
+
+For a primitive integer vector `u = (u1,u2)`,
+
+```
+uu^T = u1(u1-u2) A + u2(u2-u1) B + 2 u1 u2 P.
+```
+
+Every nonzero symmetric rational rank-one matrix is `c uu^T` for a primitive integer `u` and a nonzero rational `c`: a nonzero column is a rational vector, and clearing a common denominator and content makes it primitive.
+
+Let `Λ` be the additive group generated by `A,B,P,R,S`. Since `I = A+B` and `Q = I-P`, both lie in `Λ` once `A,B,P` do. A character is a homomorphism `Λ → F2`. Equivalently, it is an integer-valued `Z`-linear form on coefficient vectors that is even on `2Λ`, read modulo 2.
+
+The profile above has determinant equation
+
+```
+R+S+T = 4I - A - B - P - Q = 2I,
+```
+
+because `A+B+P+Q = 2I`. Each of `R,S,T` is a nonzero symmetric rational rank-one matrix. The four targets are `A+P`, `A+Q`, `B+P`, and `B+Q`. Each is a subset of the four old labels, so target support is present; the character is the obstruction that remains.
+
+Two primitive directions are **axial** when exactly one coordinate is odd, and **diagonal** when both are odd. A primitive vector is one of these two kinds. Horizontal means `(odd, even)` and vertical means `(even, odd)`; both are axial. Write `δ(p,q) = p1 q2 - p2 q1` and `|p|^2 = p1^2+p2^2`.
+
+## 2. The three directions
+
+**Proposition 1.** Let `u,v,w` be pairwise nonparallel. The symmetric matrices `uu^T`, `vv^T`, `ww^T` are linearly independent, and
+
+```
+c uu^T + d vv^T + e ww^T = 2I
+```
+
+holds for exactly one rational triple `(c,d,e)`, namely
+
+```
+c = 2(v·w) / (δ(u,v) δ(u,w)),
+```
+
+and the cyclic formulas for `d` and `e`. In particular every dot product is nonzero, since each scale is nonzero for a genuine three-frame solution.
+
+**Proof.** Let `n = (-u2, u1)`, so `n·u = 0`, `n·v = δ(u,v)`, and `n·w = δ(u,w)`. If `c uu^T + d vv^T + e ww^T = 0`, evaluate the quadratic form on `n`:
+
+```
+d δ(u,v)^2 + e δ(u,w)^2 = 0.
+```
+
+The two cyclic evaluations give the matrix equation `M (c,d,e)^T = 0` with
+
+```
+M = [[0, a, b], [a, 0, c], [b, c, 0]],
+a = δ(u,v)^2, b = δ(u,w)^2, c = δ(v,w)^2.
+```
+
+All three squares are nonzero by the nonparallel hypothesis. The determinant is `2abc ≠ 0`, so `c=d=e=0`. Thus the three matrices are independent, and a representation of `2I` is unique.
+
+The same evaluations applied to `2I` say that the scales satisfy
+
+```
+d δ(u,v)^2 + e δ(u,w)^2 = 2|u|^2
+```
+
+and its cyclic analogues, because `n^T (2I) n = 2|n|^2 = 2|u|^2`. It remains to check the displayed formula. Substitute
+
+```
+d = 2(u·w) / (δ(v,w) δ(v,u)) = -2(u·w) / (δ(v,w) δ(u,v)),
+e = 2(u·v) / (δ(w,u) δ(w,v)) = 2(u·v) / (δ(u,w) δ(v,w)).
+```
+
+The left side of the evaluation becomes
+
+```
+2[(u·v) δ(u,w) - (u·w) δ(u,v)] / δ(v,w).
+```
+
+The bracket equals `|u|^2 δ(v,w)`:
+
+```
+(u·v)(u1 w2 - u2 w1) - (u·w)(u1 v2 - u2 v1)
+  = u1^2 (v1 w2 - w1 v2) + u2^2 (w2 v1 - v2 w1)
+  = |u|^2 δ(v,w).
+```
+
+The cross terms `± u1 u2 v1 w1` and `± u1 u2 v2 w2` cancel, which is a direct expansion. The same identity with the variables cycled shows that the formula satisfies the other two evaluations. Uniqueness gives the proposition. Clearing the common denominator `δ(u,v)δ(u,w)δ(v,w)` turns this check into a polynomial identity; `verify.py` expands that polynomial and finds that every monomial cancels.
+
+**Proposition 2.** If two of the directions are parallel, a solution of `R+S+T = 2I` has the third direction orthogonal to them. After ordering the parallel pair as `u` and `εu` with `ε = ±1`, and writing `w` for a primitive orthogonal partner,
+
+```
+(c+d) uu^T + e ww^T = 2I,  c+d = 2/|u|^2,  e = 2/|w|^2,
+```
+
+with `c,d` nonzero rationals. One such partner is `w = (-u2, u1)`, and then `|w|^2 = |u|^2`.
+
+**Proof.** All three directions parallel would force the sum to have rank at most 1, while `2I` has rank 2. So exactly one direction, `w`, is not parallel to `u`. The sum of the two parallel frames is `ρ uu^T` with `ρ = c+d`. Then `ρ uu^T + e ww^T = 2I`. Apply both sides to `w`:
+
+```
+ρ (u·w) u + e |w|^2 w = 2w.
+```
+
+The left side's `u` component vanishes because `u` and `w` are independent, so `u·w = 0` and `e = 2/|w|^2`. The same argument on `u` gives `ρ = 2/|u|^2`. The vector `(-u2, u1)` is primitive, orthogonal to `u`, and has the same squared length.
+
+## 3. Two families
+
+For an integral coefficient vector `N = (a,b,c)` write
+
+```
+φ_AB(N) = (a+b) mod 2,  φ_PQ(N) = c mod 2.
+```
+
+Let `W = (ZR + ZS) ∩ Z^3`. This is a subgroup of `Z^3`, so the joint map `φ = (φ_AB, φ_PQ): W → F2^2` is a homomorphism and its image is a subspace.
+
+**Family AB.** Integers `p,s,t` give the form
+
+```
+f(a,b,c) = (1+2p)a + (1+2s)b + (2t)c = (a+b) + 2(pa+sb+tc).
+```
+
+**Family PQ.** Integers `p,s,t` give
+
+```
+f(a,b,c) = (2p)a + (2s)b + (1+2t)c = c + 2(pa+sb+tc).
+```
+
+In both families the coefficients of `a` and `b` have one parity and the coefficient of `c` has the other, so `f(A) ≡ f(B) ≢ f(P) (mod 2)`.
+
+**Proposition 3.** Suppose `φ_AB` is identically zero on `W`. Then family AB supplies a `Z`-linear form `f`, integer-valued on `Λ` and even on `2Λ`, with `f(R)` and `f(S)` even. The same holds for family PQ when `φ_PQ` is identically zero, with the second shape of `f`.
+
+**Proof.** Let `θ` be `(a+b)/2` in the AB case and `c/2` in the PQ case. Let `U = ZR + ZS`. If `kR + lS = 0` in `Q^3`, linear independence of the two nonparallel matrices, or the one-direction relation `kc+ld = 0` in the parallel case, gives `k θ(R) + l θ(S) = 0`. So
+
+```
+ψ(kR+lS) = -(k θ(R) + l θ(S))  mod Z
+```
+
+is a well-defined homomorphism `U → Q/Z`. The hypothesis says that whenever `N = kR+lS` lies in `Z^3`, the corresponding `θ` sum is an integer, so `ψ` vanishes on `U ∩ Z^3`.
+
+Let `d` be twice the least common multiple of the denominators of the coordinates of `R` and `S`. Then `dR`, `dS`, `dθ(R)`, and `dθ(S)` are integers. An element `X ∈ Z^3` satisfies `X·R ≡ -θ(R) (mod Z)` and `X·S ≡ -θ(S) (mod Z)` exactly when
+
+```
+X·(dR) ≡ -d θ(R) (mod d),  X·(dS) ≡ -d θ(S) (mod d).
+```
+
+A target in `(Z/dZ)^2` lies in the image of `X ↦ (X·(dR), X·(dS))` if and only if every `(k,l)` that kills the image also kills the target. Such a pair has `kR+lS ∈ Z^3`, and the target condition is then `kθ(R)+lθ(S) ∈ Z`, which is the hypothesis. Hence some `X = (p,s,t)` exists.
+
+The corresponding `f` satisfies `f(R) ∈ 2Z` and `f(S) ∈ 2Z` because `X·R + θ(R)` is an integer. It is `Z`-linear and integer-valued on `Λ = Z^3 + U`, so `f(2λ) = 2f(λ)` is even. Thus `f` descends to `Λ/2Λ`.
+
+Either family produces the character used below. Section 4 shows that at least one hypothesis holds.
+
+## 4. The parity image avoids (1,1)
+
+**Lemma 4.** Let `α,β,γ` be odd integers with `α+β ≡ 0 (mod 4)`. Then `αβ - γ^2 ≡ 2 or 6 (mod 8)`, so its 2-valuation is exactly 1.
+
+**Proof.** Odd squares are `1 mod 8`. Write `β = 4t - α`. Then
+
+```
+αβ - γ^2 = 4tα - α^2 - γ^2 ≡ 4tα - 2 (mod 8).
+```
+
+If `t` is even the first term vanishes mod 8. If `t` is odd it is `4·(odd) ≡ 4 (mod 8)`. The two possibilities are `6` and `2 mod 8`. The verifier checks all 32 residue classes.
+
+For `N = (a,b,c) ∈ W` define `α = 2a+c`, `β = 2b+c`, and `γ = c`. These are the entries of `2M`, where `M` is the symmetric matrix of `N`. If `φ(N) = (1,1)`, then `c` and `a+b` are both odd, so `α,β,γ` are odd and
+
+```
+α+β = 2(a+b+c) ≡ 0 (mod 4),
+```
+
+because `a+b` and `c` odd forces `a+b+c` even and, writing each as `2m+1`, the sum of `α` and `β` is divisible by 4. Lemma 4 applies to this triple.
+
+**Theorem 5.** No vector of `W` has `φ`-image `(1,1)`.
+
+**Proof.** Order the frames so that if two directions are parallel, those two are `R` and `S`. That ordering is Theorem 6. For the rest of this theorem, `u` and `v` are nonparallel, and `N ∈ W` is assumed to have image `(1,1)`. Then `M = k (c_u uu^T) + l (c_v vv^T)` for integers `k,l` and the scales of Proposition 1.
+
+Write `σ = 2k c_u` and `τ = 2l c_v`, so `2M = σ uu^T + τ vv^T` and
+
+```
+σ = 4k (v·w) / (δ(u,v) δ(u,w)),
+τ = 4l (u·w) / (δ(v,w) δ(v,u)).
+```
+
+Set `G = α v2 - γ v1` and `H = α u2 - γ u1`.
+
+*Axis case.* Suppose `u1 = 0`. Primitivity gives `u = (0,ε)` with `ε = ±1`, and `uu^T = [[0,0],[0,1]]`. Then
+
+```
+α = 2λ v1^2,  γ = 2λ v1 v2,  β = 2κ + 2λ v2^2,
+```
+
+where `κ = k c_u` and `λ = l c_v`. Since `α` is odd, `v1 ≠ 0` and `v1` divides `α`, so `v1` is odd. Then `γ = α v2 / v1` is an odd integer. Set `α' = α/v1`, an odd integer, so `γ = α' v2`. Oddness of `γ` forces `v2` odd, and `v` is diagonal. Also
+
+```
+κ = (αβ - γ^2)/(2α).
+```
+
+Lemma 4 gives `κ = (αβ-γ^2)/(2α)`. Here `δ(u,v) = -ε v1` and `δ(u,w) = -ε w1`, so the scale formulas of Proposition 1 are
+
+```
+c_u = 2(v·w)/(v1 w1),  c_v = 2 w2 / (δ(v,w) v1).
+```
+
+Pairwise nonparallel directions force `w1 ≠ 0`. The relations `κ = k c_u` and `λ = l c_v`, together with `α = v1 α'` and `λ = α'/(2 v1)`, become
+
+```
+(αβ-γ^2) w1 = 4k α' (v·w),  δ(v,w) = 4l w2 / α'.
+```
+
+The second forces `w2 ≠ 0`: otherwise `u·w = 0`, hence `c_v = 0` and `α = 0`. Solving the second for `w1` and substituting into the first produces
+
+```
+(αβ-γ^2)(v1 α' - 4l) = 4k α' (α' |v|^2 - 4l v1).
+```
+
+The factor `v1 α' - 4l` is odd, hence nonzero and of valuation 0: `v1 α'` is odd, so it is not divisible by 4. The left side therefore has valuation 1. The right side has valuation at least 2. This contradiction shows `u1 ≠ 0`. Exchanging the two summands shows `v1 ≠ 0`.
+
+*Cramer case.* Both first coordinates are nonzero, and `δ = δ(u,v) ≠ 0`. Eliminating `τ` and `σ` from the entries of `2M` gives
+
+```
+σ = G / (u1 δ),  τ = -H / (v1 δ),
+αβ - γ^2 = -GH / (u1 v1).
+```
+
+Hence `v2(GH) = 1 + v2(u1) + v2(v1)`. Equating the two formulas for `σ` and for `τ` gives the system
+
+```
+4k (v·w) u1 = G δ(u,w),  4l (u·w) v1 = H δ(v,w).
+```
+
+In coordinates `(w1,w2)` the coefficient matrix has determinant
+
+```
+GH δ + 4l G v1 |u|^2 - 4k H u1 |v|^2 - 16kl u1 v1 δ.
+```
+
+The existing direction `w` is a nontrivial kernel vector, so this determinant is zero. The constant term `GH δ` will now be shown to have strictly smaller 2-valuation than the other three terms.
+
+If `u` is axial then `H = α u2 - γ u1` is odd: the odd coordinate of `u` contributes an odd term and the even coordinate an even term. Likewise `G` is odd when `v` is axial. If the direction is diagonal, both coordinates are odd, so `H` or `G` is a difference of odds and is even.
+
+Both directions axial would make `v2(GH) = 0`, while `1+v2(u1)+v2(v1) ≥ 1`. Both diagonal would make `v2(GH) ≥ 2` and `v2(u1)=v2(v1)=0`, so the required valuation is 1. Both alternatives contradict the Cramer valuation. The remaining possibility is one axial direction and one diagonal direction. Different parity classes make `δ` odd.
+
+If `u` is axial and `v` is diagonal, then `v2(H) = 0`, `v1` is odd, and `v2(G) = 1+v2(u1)`. The constant term has valuation `1+v2(u1)`. A diagonal vector has squared length of valuation exactly 1, because both squares are `1 mod 8`. An axial vector has odd squared length. The `l` term therefore has valuation at least
+
+```
+2 + v2(G) + v2(|u|^2) ≥ 3 + v2(u1),
+```
+
+the `k` term at least `2 + v2(u1) + 1 = 3+v2(u1)`, and the `kl` term at least `4+v2(u1)`. Each exceeds the constant valuation by at least 2. The symmetric count applies when `u` is diagonal and `v` is axial. A vanishing coefficient only raises a valuation. The constant term itself is nonzero. Therefore the determinant has valuation `1+v2(u1)` or `1+v2(v1)` and is not zero.
+
+This contradiction proves Theorem 5 for nonparallel directions.
+
+**Corollary.** The image of `φ` is `{0}`, the line spanned by `(1,0)`, or the line spanned by `(0,1)`. In every case at least one coordinate functional is identically zero. Proposition 3 supplies a character with `f(R)` and `f(S)` even.
+
+The value on `T` is even as well: `f(R)+f(S)+f(T) = f(2I) = 2f(I)`, and `f(I) = f(A)+f(B)` is even because those two values are equal modulo 2.
+
+## 5. Parallel summands
+
+**Theorem 6.** If `R` and `S` are both rational multiples of one primitive `uu^T`, then every integral multiple `t uu^T` has even `P`-coefficient when `u` is axial, and even `a+b` when `u` is diagonal. Thus one coordinate functional vanishes on all of `W`.
+
+**Proof.** The coefficient vector of `t uu^T` is
+
+```
+(t u1 Δ, -t u2 Δ, 2 t u1 u2),  Δ = u1-u2.
+```
+
+If `u` is horizontal, `u1` is odd, `u2` is even, and `Δ` is odd, so `t u1 Δ ∈ Z` forces `t ∈ Z`. The `P`-coefficient then contains the even factor `u2`. The vertical case uses the second coordinate instead of the first. If `u` is diagonal, both coordinates are odd and `v2(Δ) ≥ 1`. An odd integer value of `a+b = t Δ^2` would require `v2(t) + v2(Δ^2) = 0`, hence `v2(t) ≤ -2`. Then the `P`-coefficient `2 t u1 u2` has negative valuation and is not an integer.
+
+Proposition 2 puts `W` inside this set of integral multiples, so Proposition 3 applies.
+
+## 6. The seven-call count
+
+**Theorem 7.** The profile `(1,1,1,1,1,1,1)` admits no word in the PR2085/2112 model.
+
+**Proof.** A hypothetical word would give rank-one `R,S,T` with `R+S+T = 2I`, as in Section 1. Corollary to Theorem 5, or Theorem 6 when two directions are parallel, produces a character `f` with `f(R)=f(S)=f(T)=0` in `F2` and `f(A)=f(B) ≠ f(P)`.
+
+In family AB one has `f(A)=f(B)=1` and `f(P)=0`, so `f(Q)=f(I-P)=0`. The detected calls are `A` and `B`, two of them. Each target contains exactly one of `A,B` and therefore has character 1. Four targets are detected.
+
+In family PQ one has `f(A)=f(B)=0` and `f(P)=1`, so `f(Q)=1`. The detected calls are `P` and `Q`. Each target contains exactly one of `P,Q` and has character 1.
+
+Either pattern has two detected calls and four detected targets. The inherited inequality forbids it.
+
+The explicit forms found for the fixtures in `verify.py` are witnesses of this extension. The finite fixture list is not the proof; Theorems 5 and 6 are.
+
+## Open next questions
+
+The other twenty three-frame count profiles in the seven-call census, and every decomposition with four or more added signed rank-one frames, are untouched. A profile whose rational solutions all meet this same character test would close the same way. A profile with a solution on which both `φ_AB` and `φ_PQ` are nonzero would need a different invariant, and that solution would still not by itself be a word.

research/three-signed-old-once/README.md

@@ -0,0 +1,46 @@
+# Three signed frames, all old labels once
+
+**Scoped character proof. No new κ and no word.**
+
+Every rational solution of `R+S+T = 2I` by three nonzero symmetric rank-one matrices admits a first-order character that detects two calls and four targets. In the PR2085/2112 model the seven-call profile
+
+```
+(a,b,p,q,r,s,t) = (1,1,1,1,1,1,1)
+```
+
+therefore admits no word. The selected record stays κ = `781451/250000000`. The argument is written in [PROOF.md](PROOF.md).
+
+## 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 three-frame question left open by [research/bit-two-signed-frame-floor](../bit-two-signed-frame-floor), for the single all-old-once profile released in [discussion comment 19377832](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377832).
+
+The character is an integer form of one of two shapes, `(odd,odd,even)` or `(even,even,odd)` on the coefficient vector `(a,b,c)`. The proof shows that the mod-2 image of the integral relation lattice misses `(1,1)`, so at least one shape extends off that lattice. The extension detects either `{A,B}` or `{P,Q}`, two calls, and all four targets `A+P`, `A+Q`, `B+P`, `B+Q`.
+
+The scale formula is proved by a 3-by-3 evaluation whose determinant is `2abc`, plus a bracket identity. `verify.py` expands the cleared numerator of that formula and checks that it is the zero polynomial. It also exhausts the 32 odd residue classes in the mod-8 discriminant lemma, and it checks explicit characters on nine declared frames: mixed parities, three horizontal directions, a negative-valuation sample, a vertical unit, an off-axis horizontal triple, the quarter-split parallel frame, and three orthogonal parallel splittings. Each witness detects two calls and four targets. Failure controls reject a tampered sum, reject `I` as a rank-one summand, and reject an even-even-even form.
+
+The inherited inequality "detected calls ≥ detected targets" is not reproved. 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/three-signed-old-once --check-only
+python3.12 scripts/research_package.py --package research/three-signed-old-once
+```
+
+The direct check is `python3 -I -W error -B research/three-signed-old-once/verify.py`.
+
+## Open next questions
+
+The other twenty three-frame count profiles from the seven-call census are open. A useful first step is to take one other profile, write its determinant equation, and test the same AB/PQ obstruction on one rational rank-one solution. No reduction of those profiles to `R+S+T = 2I` is supplied.
+
+Four or more added signed rank-one frames are also open. The two-frame sign reduction and this three-frame character both stop at the number of added frames they assume. A useful first step is four primitive directions and the shortest determinant equation that uses each new label once.
+
+## Credit
+
+The register model is Cinna Davis's PR2085/2112 formal model. The determinant and first-order inequality are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR6190. That floor left this three-frame question open and stopped at two added frames. The concrete handoff is discussion comment 19377832, following the census in comment 19377345 and the claim in comment 19377792.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review. New work is Apache-2.0.