From fc9a5f6b59803904782ecbd2c00c61db4aa18dca Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 9 Nov 2026 13:58:18 +0000 Subject: [PATCH 1/2] Prove the all-old-once three signed frames are character-excluded. Every rational decomposition of 2I into three nonzero symmetric rank-one matrices admits an AB or PQ character detecting two calls and four targets, so the seven-call profile (1,1,1,1,1,1,1) has no word. The selected kappa is unchanged. Co-authored-by: unpaidmoon --- research/three-signed-old-once/PROOF.md | 312 ++++++++++++++++++ research/three-signed-old-once/README.md | 46 +++ research/three-signed-old-once/SOURCES.json | 18 ++ research/three-signed-old-once/TASK.json | 75 +++++ research/three-signed-old-once/VERIFY.json | 34 ++ research/three-signed-old-once/verify.py | 330 ++++++++++++++++++++ 6 files changed, 815 insertions(+) create mode 100644 research/three-signed-old-once/PROOF.md create mode 100644 research/three-signed-old-once/README.md create mode 100644 research/three-signed-old-once/SOURCES.json create mode 100644 research/three-signed-old-once/TASK.json create mode 100644 research/three-signed-old-once/VERIFY.json create mode 100644 research/three-signed-old-once/verify.py diff --git a/research/three-signed-old-once/PROOF.md b/research/three-signed-old-once/PROOF.md new file mode 100644 index 0000000000..d852f1e1e1 --- /dev/null +++ b/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. diff --git a/research/three-signed-old-once/README.md b/research/three-signed-old-once/README.md new file mode 100644 index 0000000000..6f87dfad86 --- /dev/null +++ b/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. diff --git a/research/three-signed-old-once/SOURCES.json b/research/three-signed-old-once/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/three-signed-old-once/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/three-signed-old-once/TASK.json b/research/three-signed-old-once/TASK.json new file mode 100644 index 0000000000..c9cb3f570e --- /dev/null +++ b/research/three-signed-old-once/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that every rational decomposition 2I = R+S+T into nonzero symmetric rank-one matrices is first-order character-excluded, and therefore the all-old-once seven-call profile (a,b,p,q,r,s,t)=(1,1,1,1,1,1,1) admits no word.", + "scope_change_reason": "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 the two-signed-frame floor, for the single all-old-once count profile.", + "bottleneck_link": "Side result on the signed-frame escape. The profile still needs eight paid calls, so there is no local call-count saving and no selected-frontier change.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-old-once three-frame character proof or an explicit rational survivor. Do not search the other twenty census profiles or four-or-more frames.", + "outcome": "completed", + "evidence": "Elementary character proof for every rational rank-one solution of R+S+T=2I: the parity image in F2^2 avoids (1,1), so an AB or PQ form extends, and that form detects two calls and four targets. The scale formula is an expanded polynomial identity. Finite fixtures and the mod-8 discriminant check are in verify.py. The inherited first-order call inequality is not reproved.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the proof and verifier. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Which of the other twenty three-frame count profiles from the seven-call census survive the first-order character test?", + "why_it_matters": "Only (1,1,1,1) with three added labels used once is settled here. A surviving profile would be the next place a seven-call word could exist.", + "first_step": "Take one other census profile, write its determinant equation, and test the same AB/PQ obstruction on one rational rank-one solution.", + "blocked_by": "No uniform reduction from those profiles to R+S+T=2I is supplied." + }, + { + "question": "Can four or more added signed rank-one frames lower the eight-call minimum?", + "why_it_matters": "The two-summand sign reduction and this three-summand character both stop at the number of added frames they assume.", + "first_step": "Fix four primitive directions and the shortest determinant equation that uses each new label once, then repeat the parity-image test.", + "blocked_by": "No four-frame support or character reduction is supplied." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377832", + "upstream_checked_utc": "2026-11-09T13:54:56Z", + "priority_revision": 8 + } +} diff --git a/research/three-signed-old-once/VERIFY.json b/research/three-signed-old-once/VERIFY.json new file mode 100644 index 0000000000..a047b1d9d0 --- /dev/null +++ b/research/three-signed-old-once/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Scale-formula polynomial identity; mod-8 discriminant lemma; explicit characters on declared nonparallel and orthogonal-parallel fixtures, each detecting two calls and four targets; failure controls for a non-rank-one summand, a broken sum, and a wrong-parity form." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same identity, lemma, fixtures and failure controls under python -O." + } + ] +} diff --git a/research/three-signed-old-once/verify.py b/research/three-signed-old-once/verify.py new file mode 100644 index 0000000000..4ba3281976 --- /dev/null +++ b/research/three-signed-old-once/verify.py @@ -0,0 +1,330 @@ +#!/usr/bin/env python3 +"""Finite checks for the all-old-once three-frame character proof. + +The case analysis lives in PROOF.md. This program checks the polynomial +identity used for the scale formula, the mod-8 discriminant lemma, and +explicit characters on a declared finite fixture list. +""" + +from collections import Counter +from fractions import Fraction +import math + + +def egcd(a, b): + if b == 0: + if a == 0: + return 0, 1, 0 + sign = 1 if a > 0 else -1 + return abs(a), sign, 0 + g, x, y = egcd(b, a % b) + return g, y, x - (a // b) * y + + +def bezout(coeffs): + g = 0 + coef = [0] * len(coeffs) + for i, value in enumerate(coeffs): + g2, x, y = egcd(g, value) + coef = [c * x for c in coef] + coef[i] += y + g = g2 + return g, coef + + +def kernel_row(row): + n = len(row) + transform = [[1 if i == j else 0 for j in range(n)] for i in range(n)] + reduced = list(row) + pivot = next((i for i in range(n) if reduced[i] != 0), None) + if pivot is None: + return [[transform[k][j] for k in range(n)] for j in range(n)] + if pivot != 0: + for k in range(n): + transform[k][0], transform[k][pivot] = transform[k][pivot], transform[k][0] + reduced[0], reduced[pivot] = reduced[pivot], reduced[0] + for i in range(1, n): + if reduced[i] == 0: + continue + g, s, t = egcd(reduced[0], reduced[i]) + old0, oldi = reduced[0], reduced[i] + new0 = [s * transform[k][0] + t * transform[k][i] for k in range(n)] + newi = [(oldi // g) * transform[k][0] - (old0 // g) * transform[k][i] for k in range(n)] + for k in range(n): + transform[k][0] = new0[k] + transform[k][i] = newi[k] + reduced[0] = g + reduced[i] = 0 + return [[transform[k][j] for k in range(n)] for j in range(1, n)] + + +def solve_one(coeffs, target): + g, coef = bezout(list(coeffs)) + if target % g: + return None + scale = target // g + return [c * scale for c in coef] + + +def solve_two(c1, t1, c2, t2, modulus): + particular4 = solve_one(list(c1) + [-modulus], t1) + if particular4 is None: + return None + point = particular4[:3] + generators = [vector[:3] for vector in kernel_row(list(c1) + [-modulus])] + rhs = t2 - sum(c2[i] * point[i] for i in range(3)) + columns = [sum(c2[i] * gen[i] for i in range(3)) for gen in generators] + coeffs = solve_one(columns + [-modulus], rhs) + if coeffs is None: + return None + solution = point[:] + for weight, gen in zip(coeffs, generators): + for i in range(3): + solution[i] += weight * gen[i] + return solution + + +def dot(p, q): + return p[0] * q[0] + p[1] * q[1] + + +def delta(p, q): + return p[0] * q[1] - p[1] * q[0] + + +def coefficient(direction, scale): + x, y = direction + return tuple(scale * value for value in (x * (x - y), y * (y - x), 2 * x * y)) + + +def nonparallel_frames(u, v, w): + dirs = (u, v, w) + frames = [] + for i, direction in enumerate(dirs): + a = dirs[(i + 1) % 3] + b = dirs[(i + 2) % 3] + scale = Fraction(2 * dot(a, b), delta(direction, a) * delta(direction, b)) + frames.append(coefficient(direction, scale)) + return frames + + +def parallel_frames(u, w, scale_u): + length_u = dot(u, u) + length_w = dot(w, w) + rho = Fraction(2, length_u) + scale_w = Fraction(2, length_w) + other = rho - scale_u + return [ + coefficient(u, scale_u), + coefficient(u, other), + coefficient(w, scale_w), + ] + + +def frame_sum(frames): + return tuple(sum(frame[i] for frame in frames) for i in range(3)) + + +def rank_one_nonzero(frame): + a, b, c = frame + if a == 0 and b == 0 and c == 0: + return False + det = a * b + c * (a + b) / 2 + return det == 0 + + +def accepts(frames, form): + x, y, z = form + if (x - y) % 2 or (x - z) % 2 == 0: + return False + for frame in frames: + value = x * frame[0] + y * frame[1] + z * frame[2] + if value.denominator != 1 or int(value) % 2: + return False + return True + + +def character(frames): + den = 2 + for frame in frames[:2]: + for coordinate in frame: + den = math.lcm(den, coordinate.denominator) + + def pack(frame, theta): + row = [int(den * coordinate) for coordinate in frame] + target = int((-den * theta) % den) + return row, target + + for family, theta_of in ( + ("AB", lambda frame: (frame[0] + frame[1]) / 2), + ("PQ", lambda frame: frame[2] / 2), + ): + c1, t1 = pack(frames[0], theta_of(frames[0])) + c2, t2 = pack(frames[1], theta_of(frames[1])) + solution = solve_two(c1, t1, c2, t2, den) + if solution is None: + continue + p, s, t = solution + if family == "AB": + form = (1 + 2 * p, 1 + 2 * s, 2 * t) + else: + form = (2 * p, 2 * s, 1 + 2 * t) + if accepts(frames, form): + return family, form + return None + + +def evaluate(form, vector): + return form[0] * vector[0] + form[1] * vector[1] + form[2] * vector[2] + + +def detection_counts(form, frames): + A = (1, 0, 0) + B = (0, 1, 0) + P = (0, 0, 1) + Q = (1, 1, -1) + calls = (A, B, P, Q, frames[0], frames[1], frames[2]) + targets = ( + (A[0] + P[0], A[1] + P[1], A[2] + P[2]), + (A[0] + Q[0], A[1] + Q[1], A[2] + Q[2]), + (B[0] + P[0], B[1] + P[1], B[2] + P[2]), + (B[0] + Q[0], B[1] + Q[1], B[2] + Q[2]), + ) + detected_calls = sum(int(evaluate(form, label)) % 2 for label in calls) + detected_targets = sum(int(evaluate(form, label)) % 2 for label in targets) + return detected_calls, detected_targets + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def polynomial_zero(diff, label): + leftover = {key: value for key, value in diff.items() if value} + require(not leftover, label + " has " + str(len(leftover)) + " nonzero monomials") + + +def scale_identity(): + def mul(left, right): + out = Counter() + for left_key, left_value in left.items(): + for right_key, right_value in right.items(): + key = tuple(a + b for a, b in zip(left_key, right_key)) + out[key] = out.get(key, 0) + left_value * right_value + if out[key] == 0: + del out[key] + return out + + def add(*parts): + out = Counter() + for part in parts: + for key, value in part.items(): + out[key] = out.get(key, 0) + value + if out[key] == 0: + del out[key] + return out + + def constant(value): + return Counter({(0, 0, 0, 0, 0, 0): value}) + + def variable(index): + exponents = [0] * 6 + exponents[index] = 1 + return Counter({tuple(exponents): 1}) + + u1, u2, v1, v2, w1, w2 = (variable(i) for i in range(6)) + + def dot_poly(a1, a2, b1, b2): + return add(mul(a1, b1), mul(a2, b2)) + + def delta_poly(a1, a2, b1, b2): + return add(mul(a1, b2), {key: -value for key, value in mul(a2, b1).items()}) + + duv = delta_poly(u1, u2, v1, v2) + dvw = delta_poly(v1, v2, w1, w2) + duw = delta_poly(u1, u2, w1, w2) + vw = dot_poly(v1, v2, w1, w2) + wu = dot_poly(w1, w2, u1, u2) + uv = dot_poly(u1, u2, v1, v2) + + def cleared(quad_u, quad_v, quad_w, diagonal): + numerator = add( + mul(constant(2), mul(vw, mul(quad_u, dvw))), + {key: -value for key, value in mul(constant(2), mul(wu, mul(quad_v, duw))).items()}, + mul(constant(2), mul(uv, mul(quad_w, duv))), + ) + if diagonal: + two_d = mul(constant(2), mul(duv, mul(duw, dvw))) + numerator = add(numerator, {key: -value for key, value in two_d.items()}) + return numerator + + polynomial_zero(cleared(mul(u1, u1), mul(v1, v1), mul(w1, w1), True), "entry 00") + polynomial_zero(cleared(mul(u2, u2), mul(v2, v2), mul(w2, w2), True), "entry 11") + polynomial_zero(cleared(mul(u1, u2), mul(v1, v2), mul(w1, w2), False), "entry 01") + + # (u·v)δ(u,w) - (u·w)δ(u,v) - |u|^2 δ(v,w) = 0 + identity = add( + mul(uv, duw), + {key: -value for key, value in mul(wu, duv).items()}, + {key: -value for key, value in mul(add(mul(u1, u1), mul(u2, u2)), dvw).items()}, + ) + polynomial_zero(identity, "bracket identity") + + +def discriminant_lemma(): + checked = 0 + for alpha in (1, 3, 5, 7): + for beta in (1, 3, 5, 7): + if (alpha + beta) % 4: + continue + for gamma in (1, 3, 5, 7): + residue = (alpha * beta - gamma * gamma) % 8 + require(residue in (2, 6), "discriminant residue " + str(residue)) + checked += 1 + require(checked == 32, "discriminant residue count " + str(checked)) + + +def certify(frames, label): + require(frame_sum(frames) == (2, 2, 0), label + " does not sum to 2I") + for frame in frames: + require(rank_one_nonzero(frame), label + " has a summand that is not nonzero rank one") + found = character(frames) + require(found is not None, label + " has no AB or PQ character") + family, form = found + calls, targets = detection_counts(form, frames) + require(calls == 2 and targets == 4, label + " detects " + str(calls) + " calls and " + str(targets) + " targets") + return family, form + + +def fixtures(): + certify(nonparallel_frames((1, 0), (2, 1), (1, 1)), "mixed parities") + certify(nonparallel_frames((1, 0), (1, 2), (3, 2)), "three horizontal") + certify(nonparallel_frames((-5, -4), (-5, -3), (-3, -5)), "negative valuation sample") + certify(nonparallel_frames((0, 1), (1, 1), (-3, 1)), "vertical unit") + certify(nonparallel_frames((1, 2), (3, 4), (5, 2)), "horizontal off axis") + quarter = parallel_frames((1, -1), (1, 1), Fraction(1, 4)) + certify(quarter, "quarter split") + require(accepts(quarter, (1, 1, 2)), "quarter split rejects a+b+2c") + certify(parallel_frames((1, 0), (0, 1), Fraction(1, 3)), "orthogonal horizontal") + certify(parallel_frames((2, 1), (-1, 2), Fraction(1, 5)), "orthogonal vertical") + certify(parallel_frames((3, 1), (-1, 3), Fraction(1, 10)), "orthogonal diagonal") + + broken = list(nonparallel_frames((1, 0), (2, 1), (1, 1))) + broken[2] = (broken[2][0] + 1, broken[2][1], broken[2][2]) + require(frame_sum(broken) != (2, 2, 0), "tampered triple still sums to 2I") + identity = ((1, 0, 0), (0, 1, 0), (1, 1, 0)) + require(frame_sum(identity) == (2, 2, 0), "A+B+I setup") + require(not rank_one_nonzero(identity[2]), "I was treated as rank one") + require(not accepts(quarter, (2, 2, 2)), "even-even-even form was accepted") + + +def main(): + scale_identity() + discriminant_lemma() + fixtures() + print("PASS three-signed-old-once character checks") + + +if __name__ == "__main__": + main() From 84f70e14432a975bcdaeae37fcfecbf3890bda67 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 9 Nov 2026 13:58:43 +0000 Subject: [PATCH 2/2] Record the pre-push handoff recheck for the three-frame package. Discussion 1166 still ends at comment 19481299, so the all-old-once handoff remains unclaimed. Co-authored-by: unpaidmoon --- research/three-signed-old-once/TASK.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/three-signed-old-once/TASK.json b/research/three-signed-old-once/TASK.json index c9cb3f570e..03939e7776 100644 --- a/research/three-signed-old-once/TASK.json +++ b/research/three-signed-old-once/TASK.json @@ -69,7 +69,7 @@ ], "selection": { "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377832", - "upstream_checked_utc": "2026-11-09T13:54:56Z", + "upstream_checked_utc": "2026-11-09T13:58:36Z", "priority_revision": 8 } }