From ed127d7ab6067daf8a48def1445da5864ad113df Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 02:36:03 +0000 Subject: [PATCH] Prove the (0,2,1,1) three-frame profile admits no seven-call word. Every rational rank-one solution of R+S+T = 3A+B has an AB or PQ character that detects two calls and four targets. The selected frontier is unchanged. Co-authored-by: unpaidmoon --- research/three-signed-b-twice/PROOF.md | 283 ++++++++++++++ research/three-signed-b-twice/README.md | 46 +++ research/three-signed-b-twice/SOURCES.json | 24 ++ research/three-signed-b-twice/TASK.json | 76 ++++ research/three-signed-b-twice/VERIFY.json | 34 ++ research/three-signed-b-twice/verify.py | 408 +++++++++++++++++++++ 6 files changed, 871 insertions(+) create mode 100644 research/three-signed-b-twice/PROOF.md create mode 100644 research/three-signed-b-twice/README.md create mode 100644 research/three-signed-b-twice/SOURCES.json create mode 100644 research/three-signed-b-twice/TASK.json create mode 100644 research/three-signed-b-twice/VERIFY.json create mode 100644 research/three-signed-b-twice/verify.py diff --git a/research/three-signed-b-twice/PROOF.md b/research/three-signed-b-twice/PROOF.md new file mode 100644 index 0000000000..2e87f46b23 --- /dev/null +++ b/research/three-signed-b-twice/PROOF.md @@ -0,0 +1,283 @@ +# The profile (0,2,1,1)/(1,1,1) is 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) = (0,2,1,1,1,1,1) +``` + +admits no word. Every decomposition of the determinant residual by three nonzero symmetric rational rank-one matrices admits an additive character that detects two calls and four targets. + +This is a scoped proof for that one profile. It is not a multiplication theorem, not a search, and not a certificate that changes the selected κ `781451/250000000`. The other nineteen three-frame census profiles, and every decomposition with four or more added frames, stay open. The settled all-old-once profile `(1,1,1,1)/(1,1,1)` is not reproved. + +The inequality "detected calls ≥ detected targets" is inherited from `research/bit-two-signed-frame-floor/PROOF.md`, Section 1, which records the PR2910 normalization. This file does not reprove it. + +## 1. The determinant equation + +Addresses are rational symmetric 2-by-2 matrices, + +``` +A = diag(1,0), B = diag(0,1), +P = [[1,1],[1,1]]/2, Q = [[1,-1],[-1,1]]/2, +``` + +with `A+B = P+Q = I`. A general element of the rational span has coefficient vector `(a,b,c)` and matrix + +``` +[[a + c/2, c/2], [c/2, b + c/2]]. +``` + +Its determinant is `ab + c(a+b)/2`. The matrix is nonzero and rank one exactly when that determinant vanishes and the vector is nonzero. For a primitive integer direction `u = (u1,u2)` and a nonzero rational scale `t`, + +``` +t uu^T = (t u1(u1-u2), t u2(u2-u1), 2 t u1 u2). +``` + +Every nonzero symmetric rational rank-one matrix arises this way. + +The profile uses two `B` calls, one `P` call, one `Q` call, and three added labels `R,S,T` once each. No `A` call is used. The PR2910 determinant identity gives + +``` +R + S + T = 4I - 2B - P - Q. +``` + +Since `P+Q = I` and `I = A+B`, + +``` +4I - 2B - P - Q = 3I - 2B = 3A + B = diag(3,1). +``` + +Write `H = 3A+B`, with coefficient vector `(3,1,0)`. A hypothetical word produces nonzero symmetric rational rank-one `R,S,T` satisfying `R+S+T = H`. Target support is not required for the exclusion below: the character already rules out every such triple, so it rules out every triple that a word could produce. + +Let `B(x,y) = x1 y1 + 3 x2 y2` and `q(x) = B(x,x) = x1^2 + 3 x2^2`. Let `δ(x,y) = x1 y2 - x2 y1`. + +## 2. Two character shapes + +For an integral coefficient vector `N = (a,b,c)` write + +``` +φ_AB(N) = (a+b) mod 2, φ_PQ(N) = c mod 2. +``` + +**Family AB.** Integers `p,s,t` give + +``` +f(a,b,c) = (1+2p)a + (1+2s)b + (2t)c. +``` + +**Family PQ.** Integers `p,s,t` give + +``` +f(a,b,c) = (2p)a + (2s)b + (1+2t)c. +``` + +In family AB, `f(A)` and `f(B)` are odd and `f(P)` and `f(Q)` are even. In family PQ, `f(A)` and `f(B)` are even and `f(P)` and `f(Q)` are odd. Either evaluation is immediate from `Q = A+B-P`. + +The four targets are `A+P = (1,0,1)`, `A+Q = (2,1,-1)`, `B+P = (0,1,1)`, and `B+Q = (1,2,-1)`. Substituting the forms shows that every integer shift `(p,s,t)` makes all four targets odd. Thus either character detects four targets. + +On this profile the same forms detect the following old calls when they vanish on `R,S,T`: + +- Family AB detects the two `B` calls and no `A` call, because `a = 0` and `b = 2`. +- Family PQ detects the one `P` call and the one `Q` call. + +Either way that is two detected calls. The inherited inequality forbids two detected calls against four detected targets. It remains only to show that one of the two forms extends to a character of the label lattice with `f(R)`, `f(S)`, and `f(T)` even. + +The label lattice is `Λ = Z^3 + ZR + ZS`. It contains `T` because `T = H-R-S` and `H` lies in `Z^3`. A form above is integer-valued on `Z^3`. It descends to a character `Λ → F2` once it is integer-valued on `Λ` and even on `2Λ`, which is automatic for an integer-valued homomorphism into `Z` read modulo 2. + +## 3. Extension from a vanishing coordinate + +Let `U = ZR + ZS` and let `W = U ∩ Z^3`. Let `θ` be `(a+b)/2` in the AB case and `c/2` in the PQ case. + +**Lemma 1.** Suppose `φ_AB` is identically zero on `W`. Then some AB form is an integer on `Λ` and is even on `R` and on `S`. The same holds for a PQ form when `φ_PQ` vanishes on `W`. + +**Proof.** If `kR + lS = 0` in `Q^3`, then `k θ(R) + l θ(S) = 0`. Indeed `θ` is linear, and on a single primitive line it is proportional to the scale: the AB value of `t uu^T` is `t(u1-u2)^2/2` and the PQ value is `t u1 u2`. Two parallel frames are scales of one matrix, so a linear dependence of the frames is a linear dependence of the scales. Two nonparallel frames are linearly independent, because a primitive direction has a nonzero perpendicular and the determinant formula + +``` +det(c uu^T + d vv^T) = c d δ(u,v)^2 +``` + +is nonzero when both scales and `δ(u,v)` are nonzero. Thus + +``` +ψ(kR+lS) = -(k θ(R) + l θ(S)) mod Z +``` + +is a well-defined homomorphism `U → Q/Z`. The hypothesis says that `ψ` vanishes on `W`. + +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 integer vector `X` satisfies `X·R ≡ -θ(R)` and `X·S ≡ -θ(S)` modulo `Z` exactly when + +``` +X·(dR) ≡ -d θ(R), 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 integer pair `(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 form satisfies `f(R) ∈ 2Z` and `f(S) ∈ 2Z`, and it is integer-valued on `Λ = Z^3 + U`. + +**Lemma 2.** Either extension of Lemma 1 is even on `T` as well. + +**Proof.** The AB form takes the value `(1+2p)·3 + (1+2s)·1 = 4 + even` on `H = (3,1,0)`, and the PQ form takes `2p·3 + 2s·1`, which is even. Thus `f(H)` is even. Then `f(T) = f(H) - f(R) - f(S)` is even. + +Consequently, once either coordinate functional vanishes on `W`, the profile's calls and targets give the forbidden count `2 < 4`. + +The image of `φ = (φ_AB, φ_PQ)` on `W` is a subspace of `F2^2`. If it does not contain `(1,1)`, it cannot contain both `(1,0)` and `(0,1)`, so at least one coordinate functional vanishes. The rest of the argument shows that `(1,1)` never occurs. + +## 4. One primitive line never has image (1,1) + +**Lemma 3.** Let `u` be a primitive integer vector and let `t` be rational. If `t uu^T` lies in `Z^3`, then its `φ`-image is not `(1,1)`. An axial `u` forces the `P`-coefficient even and the scale `t` itself to be an integer. A diagonal `u` forces `a+b` even. + +Axial means that exactly one coordinate is odd. Diagonal means that both are odd. Every primitive vector is one of these two kinds. Horizontal means `(odd, even)` and vertical means `(even, odd)`. + +**Proof.** Write `Δ = u1-u2`. The coefficient vector is + +``` +(t u1 Δ, -t u2 Δ, 2 t u1 u2). +``` + +Since `gcd(u1,u2) = 1`, one has `gcd(Δ,u1) = gcd(u2,u1) = 1` and `gcd(Δ,u2) = 1`. + +Suppose `u` is horizontal, so `u1` is odd, `u2` is even, and `Δ` is odd. Integrality of the first and third coordinates gives `Δ | 2 u2 a` after eliminating `t`, where `a` is the first coefficient. Thus `Δ | a`, because `Δ` is coprime to `2` and to `u2`. Writing `a = Δ a1` produces `t = a1/u1`. The second coefficient is then an integer multiple of `Δ/u1` times `u2`. Coprimality of `u1` with both `Δ` and `u2` forces `u1 | a1`, so `t` is an integer. The third coefficient `2 t u1 u2` is divisible by the even integer `u2`. + +The vertical case is the same argument with the two diagonal entries exchanged: the odd coordinate is now the second one, and the third coefficient is divisible by the even first coordinate. + +Suppose `u` is diagonal. Then `Δ` is even. If `Δ = 0`, the direction is parallel to `(1,1)` and the sum of the first two coefficients is `0`, which is even. If `Δ ≠ 0`, then `v2(Δ^2) ≥ 2`. That sum is `t Δ^2`. If it were an odd integer, then `v2(t) ≤ -2`. The third coefficient `2 t u1 u2` would have valuation `1+v2(t) ≤ -1`, because both direction coordinates are odd, and would not be an integer. + +**Corollary.** If `R` and `S` are rational multiples of one primitive `uu^T`, then one coordinate functional vanishes on `W`. Lemmas 1 and 2 supply a character, and the profile is excluded. + +Three parallel directions cannot occur: their sum would have rank at most 1, while `H = diag(3,1)` has rank 2. If exactly two directions are parallel, order the frames so that those two are `R` and `S`. The corollary applies. + +## 5. Scales for three directions + +**Lemma 4.** Let `α,β,γ` be odd integers with `α+β ≡ 0 (mod 4)`. Then `αβ - γ^2 ≡ 2 or 6 (mod 8)`. + +**Proof.** The statement depends only on residues modulo 8. There are exactly 32 eligible classes: each of `α,β,γ` lies in `{1,3,5,7}`, and `α+β ≡ 0 (mod 4)`. `verify.py` evaluates all 32. This finite check is the whole lemma, because every eligible integer triple reduces to one class. The same expansion used for the all-old-once profile explains the count: odd squares are `1 (mod 8)`, and writing `β = 4t-α` leaves `4tα - 2 (mod 8)`. + +**Proposition 5.** Let `u,v,w` be pairwise nonparallel primitive integer vectors, and suppose + +``` +c_u uu^T + c_v vv^T + c_w ww^T = H +``` + +with all three scales nonzero. Then + +``` +c_u = B(v,w) / (δ(u,v) δ(u,w)), +``` + +and the cyclic formulas hold for `c_v` and `c_w`. In particular `B(v,w)`, `B(w,u)`, and `B(u,v)` are nonzero. + +**Proof.** The three matrices `uu^T`, `vv^T`, and `ww^T` are linearly independent. The same perpendicular evaluation used for `2I` gives the system + +``` +c_v δ(u,v)^2 + c_w δ(u,w)^2 = q(u) +``` + +and its cyclic analogues. The coefficient matrix has determinant `2 δ(u,v)^2 δ(u,w)^2 δ(v,w)^2 ≠ 0`, so the scales are unique. It is therefore enough to check the displayed formula. Substituting the cyclic expressions produces the bracket + +``` +δ(u,w) B(u,v) - δ(u,v) B(u,w) - q(u) δ(v,w). +``` + +Expanding in the six coordinates, the terms `±3 u1 u2 v2 w2` and `± u1 u2 v1 w1` cancel, and the rest factors as `q(u) δ(v,w)`. The bracket is identically zero. `verify.py` expands the same polynomial and finds no monomial. The cyclic brackets are the same identity with the variables permuted. + +## 6. The parity image avoids (1,1) + +Let `R = c_u uu^T` and `S = c_v vv^T` be two of the three frames in Proposition 5, and suppose `N = kR + lS` lies in `Z^3` with `φ(N) = (1,1)`. Write `α = 2a+c`, `β = 2b+c`, and `γ = c` for the coefficient vector of `N`. All three are odd, and `α+β = 2(a+b+c) ≡ 0 (mod 4)` because `a+b` and `c` are both odd. Lemma 4 gives `v2(αβ-γ^2) = 1`. The doubled matrix is `[[α,γ],[γ,β]]`. + +**Axis case.** Suppose `u1 = 0`. Primitivity gives `u = (0,ε)` with `ε = ±1`. Nonparallelism forces `v1 ≠ 0` and `w1 ≠ 0`. The scale formulas collapse to + +``` +c_u = 1 + 3 v2 w2 / (v1 w1), c_v = 3 w2 / (δ(v,w) v1). +``` + +The doubled matrix has `α = τ v1^2` and `γ = τ v1 v2`, where `τ = 2 l c_v`. Oddness of `α` forces `v1` and `τ` to be odd, and then oddness of `γ` forces `v2` odd. Thus `v` is diagonal. Also `gcd(v1,v2) = 1`, so `v1` divides `α`, and `τ = α / v1^2` has valuation 0. + +The identity `αβ-γ^2 = σ τ v1^2` with `σ = 2 k c_u` gives `v2(σ) = 1`. Equating the two formulas for `c_v` gives + +``` +δ(v,w) = 6 l v1 w2 / α. +``` + +The right side vanishes only if `w2 = 0` or `l = 0`. The second would make `N` a multiple of `uu^T`, which Lemma 3 forbids. The first makes `w` horizontal, so `δ(v,w) = ∓ v2 ≠ 0`. Thus `w2 ≠ 0`, and solving for `w1` gives + +``` +w1 = v1 w2 (α - 6l) / (α v2). +``` + +The same doubled-matrix identity gives `k c_u = (αβ-γ^2)/(2α)`. Substituting `c_u` and then `w1` produces + +``` +(α-6l) v1^2 (αβ-γ^2 - 2α k) = 6 α^2 k v2^2. +``` + +Here `α`, `v1`, and `v2` are odd, so `α-6l` is odd. The right side has valuation `1 + v2(k)`. + +If `v2(k) ≥ 1`, the left bracket has valuation 1, because `αβ-γ^2` has valuation 1 and `2αk` has valuation at least 2. The left side then has valuation 1 and the right side has valuation at least 2. + +If `v2(k) = 0`, both `αβ-γ^2` and `2αk` are congruent to `2` or `6` modulo 8, by Lemma 4 and the oddness of `α` and `k`. Their difference is congruent to `0` or `4` modulo 8, so its valuation is at least 2. The right side is nonzero and has valuation 1. + +Both alternatives contradict the equation. Therefore `u1 ≠ 0`. Exchanging the two summands gives `v1 ≠ 0`. + +**Cramer case.** Both first coordinates are nonzero, and `δ = δ(u,v) ≠ 0`. Set `G = α v2 - γ v1` and `H_ = α u2 - γ u1`. Entry comparison gives + +``` +σ = G / (u1 δ), τ = -H_ / (v1 δ), +αβ - γ^2 = -G H_ / (u1 v1), +``` + +where `σ = 2 k c_u` and `τ = 2 l c_v`. Hence + +``` +v2(G H_) = 1 + v2(u1) + v2(v1), +``` + +with valuations taken on absolute values. If `u` is axial then `H_` is odd: the odd coordinate of `u` contributes an odd term and the even coordinate an even term. The same holds for `G` when `v` is axial. If the direction is diagonal, the corresponding linear form is a difference of odd integers and is even. + +Both directions axial, and both directions diagonal, are then impossible. Two horizontal directions would require valuation 1 while both forms are odd. Two vertical directions would require valuation at least 3 while both forms are odd. One horizontal and one vertical direction would require valuation at least 2 while both forms are odd. Two diagonal directions would require valuation 1 while both forms are even. The only remaining possibility is one axial direction and one diagonal direction. Different parity classes make `δ` odd. + +Equating the Cramer formulas with Proposition 5 gives the linear system + +``` +2 k u1 B(v,w) = G δ(u,w), 2 l v1 B(u,w) = H_ δ(v,w). +``` + +In coordinates `(w1,w2)` the coefficient matrix is + +``` +| 2 k u1 v1 + G u2 6 k u1 v2 - G u1 | +| 2 l u1 v1 + H_ v2 6 l v1 u2 - H_ v1 |. +``` + +Its determinant expands to + +``` +δ G H_ + 2 l G v1 q(u) - 2 k H_ u1 q(v) - 12 k l u1 v1 δ. +``` + +The grouping is the one checked as a polynomial identity in `verify.py`: the `G H_` terms produce `δ G H_`, the `k H_` terms produce `-2 k H_ u1 q(v)`, the `G l` terms produce `2 l G v1 q(u)`, and the `k l` terms produce `-12 k l u1 v1 δ`. The existing direction `w` is a nontrivial kernel vector, so this determinant is zero. + +A diagonal primitive vector has `q ≡ 4 (mod 8)`, because both squares are `1 (mod 8)`. Thus its quadratic valuation is exactly 2. An axial primitive vector has odd `q`: the odd coordinate contributes an odd square and the even coordinate an even term. Thus its quadratic valuation is 0. + +Suppose `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 exactly `1+v2(u1)`, and it is nonzero. The `l` term has valuation at least `2+v2(u1)`, the `k` term at least `3+v2(u1)`, and the `kl` term at least `2+v2(u1)`. Each is strictly larger than the constant valuation, whether or not `k` or `l` is divisible by 2. The determinant therefore has valuation `1+v2(u1)` and is not zero. + +Suppose `u` is diagonal and `v` is axial. Then `v2(G) = 0` and `v2(H_) = 1+v2(v1)`, while `v2(q(u)) = 2` and `v2(q(v)) = 0`. The constant term has valuation `1+v2(v1)`. The `l` term has valuation at least `3+v2(v1)`, the `k` term at least `2+v2(v1)`, and the `kl` term at least `2+v2(v1)`. Again the constant term is strictly smaller, so the determinant is nonzero. + +This contradiction shows that no vector of `W` has image `(1,1)`. + +The third frame does not enlarge the image. Because `T = H-R-S` and `φ(H) = (0,0)`, an integral combination `kR+lS+mT` lies in `Z^3` only when `(k-m)R+(l-m)S` does, and the two combinations have the same image under `φ`. + +## 7. Conclusion + +**Theorem.** The profile `(0,2,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 = 3A+B`. If two directions are parallel, Section 4 supplies a character. If all three directions are distinct, Section 6 shows that the parity image of `W` avoids `(1,1)`, so one coordinate functional vanishes, and Lemmas 1 and 2 supply a character. In both situations the character detects two calls and four targets. The inherited inequality forbids that pattern. + +The explicit forms found for the fixtures in `verify.py` are witnesses of the extension. The finite fixture list, the single-line box, and the valuation-arithmetic checks are not this theorem. Sections 4 through 6 are. Lemma 4 and the two polynomial identities are exhaustive finite or exact-expansion arguments, as recorded in Section 5 and in the verifier. + +## Open next questions + +Nineteen three-frame count profiles from the census in discussion comment 19377345 remain open, including the twelve siblings of this profile such as `(2,0,1,1)/(1,1,1)`. A useful first step for `(2,0,1,1)` is to repeat the scale formula with the bilinear form `3 x1 y1 + x2 y2`, because the residual there is `diag(1,3)` rather than `diag(3,1)`. The constants 3, 6, and 12 in this file belong to `3A+B` and are not claimed for another residual. + +Four or more added signed rank-one frames are also open. This argument stops at three summands. diff --git a/research/three-signed-b-twice/README.md b/research/three-signed-b-twice/README.md new file mode 100644 index 0000000000..37afae3fd5 --- /dev/null +++ b/research/three-signed-b-twice/README.md @@ -0,0 +1,46 @@ +# Three signed frames, old profile (0,2,1,1) + +**Scoped character proof. No new κ and no word.** + +In the PR2085/2112 model, the seven-call count profile + +``` +(a,b,p,q,r,s,t) = (0,2,1,1,1,1,1) +``` + +admits no word. The determinant equation is `R+S+T = 3A+B = diag(3,1)`. Every rational solution by three nonzero symmetric rank-one matrices admits an AB or PQ character that detects two calls and four targets. The selected record stays κ = `781451/250000000`. The argument is written in [PROOF.md](PROOF.md). + +## Scope and evidence + +This is one named profile from the seven-call census in [discussion comment 19377345](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345): old counts `(0,2,1,1)` with added multiplicities `(1,1,1)`. It is one of the twelve profiles listed there with 24 positive-dimensional spaces. It is not the settled all-old-once profile `(1,1,1,1)/(1,1,1)`. + +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 one profile left open by the all-old-once character proof, which itself answered the three-frame question in [research/bit-two-signed-frame-floor](../bit-two-signed-frame-floor). + +Evidence class: **proof**, for this profile and these hypotheses only. Lemma 4 is an exhaustive check of its 32 residue classes. The scale bracket and the Cramer determinant are polynomial identities, expanded in full by `verify.py`. The single-line box in the verifier is a finite corroboration of Lemma 3 on coordinates and denominators at most 12; the written coprimality argument covers every primitive vector. The five fixtures are witnesses of the character, not a census of solutions. No step is a heuristic search offered as a nonexistence proof. + +The inherited inequality "detected calls ≥ detected targets" is not reproved. Predecessor replays, Lean, Docker, and the selected-result cold replay were not run. The orientation command `scripts/research_selected_baseline.py` was not run in this session. + +Source commits, Git blobs, and SHA256 pins are in [SOURCES.json](SOURCES.json). The selected record and catalogue are historical provenance. Priority revision 8 on this main still quotes an older selected decimal; the frontier value used here is the selected record, not that sentence. Full Git history is needed to resolve the pins. + +## Reproduce + +From the repository root, with Python 3.12: + +```sh +python3 scripts/research_package.py --package research/three-signed-b-twice --check-only +python3.12 scripts/research_package.py --package research/three-signed-b-twice +``` + +The direct check is `python3 -I -W error -B research/three-signed-b-twice/verify.py`. + +## Open next questions + +Which of the other nineteen three-frame count profiles survive the same test? A useful first step is the named sibling `(2,0,1,1)/(1,1,1)`, whose residual is `diag(1,3)` rather than `diag(3,1)`. The bilinear form and the constants 3, 6, and 12 in this proof are special to `3A+B`. + +Can four or more added signed rank-one frames lower the eight-call minimum? This three-summand character does not apply. 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, PR #6190. The census and the released all-old-once handoff are Nick Petalas's discussion comments 19377345 and 19377832. The all-old-once profile was character-excluded separately and is not redone here. + +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-b-twice/SOURCES.json b/research/three-signed-b-twice/SOURCES.json new file mode 100644 index 0000000000..b9dd61be33 --- /dev/null +++ b/research/three-signed-b-twice/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + }, + { + "path": "research/bit-two-signed-frame-floor/PROOF.md", + "usage": "provenance", + "git_blob": "3797e6b8dc196bf5e6d9b5bf5a43c255b435f0bb", + "sha256": "6964115728b748cdb4d52f6e5a626dd3840bb01f254f4c1ce26bc475a25a2420" + } + ] +} diff --git a/research/three-signed-b-twice/TASK.json b/research/three-signed-b-twice/TASK.json new file mode 100644 index 0000000000..0b353b0631 --- /dev/null +++ b/research/three-signed-b-twice/TASK.json @@ -0,0 +1,76 @@ +{ + "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 the seven-call profile (a,b,p,q,r,s,t)=(0,2,1,1,1,1,1) admits no word in the PR2085/2112 model, because every rational rank-one solution of R+S+T=3A+B has an AB or PQ character detecting two calls and four targets.", + "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 one named three-frame census profile left open after the all-old-once character exclusion.", + "bottleneck_link": "Side result on the signed-frame escape. This 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 character proof for the single named profile (0,2,1,1)/(1,1,1). Do not search the other nineteen census profiles or four-or-more frames.", + "outcome": "completed", + "evidence": "Scoped proof that every rational rank-one solution of R+S+T=3A+B has parity image avoiding (1,1), so an AB or PQ form extends and detects two calls against four targets. The scale bracket and Cramer determinant are expanded polynomial identities. Lemma 4 is the exhaustive 32-class mod-8 check. The single-line box and five fixtures in verify.py corroborate the written argument and are not a solution census.", + "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 nineteen three-frame count profiles from the seven-call census survive the same AB/PQ test?", + "why_it_matters": "Only (1,1,1,1)/(1,1,1) and (0,2,1,1)/(1,1,1) are character-excluded. A surviving profile would be the next place a seven-call word could exist.", + "first_step": "Take the named sibling (2,0,1,1)/(1,1,1), whose residual is diag(1,3), and repeat the scale formula with bilinear form 3*x1*y1 + x2*y2.", + "blocked_by": "The constants 3, 6, and 12 in this proof are special to 3A+B and do not transfer unchanged." + }, + { + "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", + "census": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345", + "upstream_checked_utc": "2026-11-10T02:35:54Z", + "priority_revision": 8 + } +} diff --git a/research/three-signed-b-twice/VERIFY.json b/research/three-signed-b-twice/VERIFY.json new file mode 100644 index 0000000000..fdee6b8f70 --- /dev/null +++ b/research/three-signed-b-twice/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-bracket and Cramer-determinant polynomial identities; exhaustive 32-class mod-8 discriminant lemma; axial and diagonal quadratic valuations; strict valuation-gap arithmetic; single-line parity on the declared coordinate box; explicit AB/PQ characters on five frames, each detecting two calls and four targets; failure controls for a tampered sum, the identity matrix, and an even-even-even form." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same identities, lemma, box, fixtures and failure controls under python -O." + } + ] +} diff --git a/research/three-signed-b-twice/verify.py b/research/three-signed-b-twice/verify.py new file mode 100644 index 0000000000..64227851bf --- /dev/null +++ b/research/three-signed-b-twice/verify.py @@ -0,0 +1,408 @@ +"""Character exclusion for the seven-call profile (0,2,1,1)/(1,1,1). + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The proof is PROOF.md. This file checks the polynomial identities, the +exhaustive mod-8 lemmas, the single-line parity lemma on a declared box, +and explicit characters on declared frames. The box is not the proof. +""" + +from fractions import Fraction as F +from itertools import product +from math import gcd, lcm + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Poly: + def __init__(self, terms=None): + self.terms = {} + if terms: + for key, value in terms.items(): + if value: + self.terms[key] = value + + def add(self, other, scale=1): + out = dict(self.terms) + for key, value in other.terms.items(): + out[key] = out.get(key, 0) + scale * value + if out[key] == 0: + del out[key] + return Poly(out) + + def mul(self, other): + out = {} + for left, lval in self.terms.items(): + for right, rval in other.terms.items(): + key = tuple(a + b for a, b in zip(left, right)) + out[key] = out.get(key, 0) + lval * rval + if out[key] == 0: + del out[key] + return Poly(out) + + +def var(index, width): + exponents = [0] * width + exponents[index] = 1 + return Poly({tuple(exponents): 1}) + + +def const(value, width): + if value == 0: + return Poly() + return Poly({tuple([0] * width): value}) + + +def check_bracket_polynomial(): + """δ(u,w) B(u,v) - δ(u,v) B(u,w) - q(u) δ(v,w) is the zero polynomial.""" + width = 6 + u1, u2, v1, v2, w1, w2 = (var(i, width) for i in range(width)) + three = const(3, width) + + def bilinear(x1, x2, y1, y2): + return x1.mul(y1).add(three.mul(x2).mul(y2)) + + def cross(x1, x2, y1, y2): + return x1.mul(y2).add(x2.mul(y1), scale=-1) + + def quad(x1, x2): + return x1.mul(x1).add(three.mul(x2).mul(x2)) + + expression = ( + cross(u1, u2, w1, w2).mul(bilinear(u1, u2, v1, v2)) + .add(cross(u1, u2, v1, v2).mul(bilinear(u1, u2, w1, w2)), scale=-1) + .add(quad(u1, u2).mul(cross(v1, v2, w1, w2)), scale=-1) + ) + require(expression.terms == {}, "scale bracket polynomial is not identically zero") + + +def check_determinant_polynomial(): + """Closed form of the (w1,w2) coefficient determinant.""" + width = 8 + k, l, u1, u2, v1, v2, gee, hhh = (var(i, width) for i in range(width)) + two = const(2, width) + six = const(6, width) + three = const(3, width) + row11 = two.mul(k).mul(u1).mul(v1).add(gee.mul(u2)) + row12 = six.mul(k).mul(u1).mul(v2).add(gee.mul(u1), scale=-1) + row21 = two.mul(l).mul(u1).mul(v1).add(hhh.mul(v2)) + row22 = six.mul(l).mul(v1).mul(u2).add(hhh.mul(v1), scale=-1) + matrix_det = row11.mul(row22).add(row12.mul(row21), scale=-1) + delta = u1.mul(v2).add(u2.mul(v1), scale=-1) + quad_u = u1.mul(u1).add(three.mul(u2).mul(u2)) + quad_v = v1.mul(v1).add(three.mul(v2).mul(v2)) + closed = ( + delta.mul(gee).mul(hhh) + .add(two.mul(l).mul(gee).mul(v1).mul(quad_u)) + .add(two.mul(k).mul(hhh).mul(u1).mul(quad_v), scale=-1) + .add(const(12, width).mul(k).mul(l).mul(u1).mul(v1).mul(delta), scale=-1) + ) + require(matrix_det.terms == closed.terms, "determinant polynomial mismatch") + + +def check_lemma4(): + """Every eligible odd residue has αβ-γ^2 ≡ 2 or 6 (mod 8). Exhaustive.""" + odds = (1, 3, 5, 7) + seen = 0 + for alpha in odds: + for beta in odds: + if (alpha + beta) % 4 != 0: + continue + for gamma in odds: + seen += 1 + value = (alpha * beta - gamma * gamma) % 8 + require(value in (2, 6), "lemma 4 residue " + str((alpha, beta, gamma, value))) + require(seen == 32, "expected 32 odd residue classes, found " + str(seen)) + + +def check_axis_mod8(): + """2αk and αβ-γ^2 are each 2 or 6 mod 8, so their difference is not.""" + odds = (1, 3, 5, 7) + for alpha in odds: + for kay in odds: + product = (2 * alpha * kay) % 8 + require(product in (2, 6), "2αk residue") + for gap in (2, 6): + difference = (gap - product) % 8 + require(difference in (0, 4), "axis difference residue") + for second in odds: + right = (6 * alpha * alpha * kay * second * second) % 8 + require(right in (2, 6), "axis right-hand residue") + + +def check_quadratic_valuations(): + """Diagonal q has 2-valuation 2; an axial primitive vector has odd q.""" + odds = (1, 3, 5, 7) + for first in odds: + for second in odds: + square_sum = (first * first + 3 * second * second) % 8 + require(square_sum == 4, "diagonal quadratic residue") + for u1, u2 in product(range(-12, 13), repeat=2): + if gcd(abs(u1), abs(u2)) != 1: + continue + axial = (u1 % 2 == 0) ^ (u2 % 2 == 0) + if not axial: + continue + value = u1 * u1 + 3 * u2 * u2 + require(value % 2 == 1, "axial quadratic parity " + str((u1, u2))) + + +def valuation_gap(v2_u1): + constant = 1 + v2_u1 + l_term = 1 + (1 + v2_u1) # v2(2) + v2(G), with q(u) and v1 odd + k_term = 1 + v2_u1 + 2 # v2(2) + v2(u1) + v2(q(v)) + kl_term = 2 + v2_u1 # v2(12) + v2(u1) + require(l_term > constant and k_term > constant and kl_term > constant, + "valuation gap collapsed at " + str(v2_u1)) + + +def check_valuation_gaps(): + for shift in range(0, 12): + valuation_gap(shift) + + +def coeffs(direction, scale): + first, second = direction + scale = F(scale) + return ( + scale * first * (first - second), + scale * second * (second - first), + 2 * scale * first * second, + ) + + +def matrix_det(vector): + first, second, off = vector + return first * second + off * (first + second) / 2 + + +def primitive_directions(bound): + directions = [] + for first, second in product(range(-bound, bound + 1), repeat=2): + if (first, second) == (0, 0): + continue + if second < 0 or (second == 0 and first < 0): + continue + if gcd(abs(first), abs(second)) != 1: + continue + directions.append((first, second)) + return directions + + +def check_single_line_box(): + """Corroborate the single-line lemma on a finite box. Not the proof.""" + checked = 0 + for direction in primitive_directions(12): + first, second = direction + diagonal = first % 2 == 1 and second % 2 == 1 + axial = (first % 2 == 0) ^ (second % 2 == 0) + require(diagonal or axial, "primitive vector is axial or diagonal") + for numerator in range(-12, 13): + if numerator == 0: + continue + for denominator in range(1, 13): + scale = F(numerator, denominator) + vector = coeffs(direction, scale) + if any(entry.denominator != 1 for entry in vector): + continue + checked += 1 + parity_ab = (vector[0] + vector[1]) % 2 + parity_pq = vector[2] % 2 + require((parity_ab, parity_pq) != (1, 1), "single line hit (1,1)") + if diagonal: + require(parity_ab == 0, "diagonal line has odd a+b") + if axial: + require(parity_pq == 0, "axial line has odd c") + require(scale.denominator == 1, "axial integral scale is not integral") + require(checked > 100, "single-line box checked too little") + + +def bilinear(left, right): + return F(left[0] * right[0] + 3 * left[1] * right[1]) + + +def cross(left, right): + return F(left[0] * right[1] - left[1] * right[0]) + + +def solve_scales(first, second, third): + return ( + bilinear(second, third) / (cross(first, second) * cross(first, third)), + bilinear(third, first) / (cross(second, third) * cross(second, first)), + bilinear(first, second) / (cross(third, first) * cross(third, second)), + ) + + +def parity_image(left, right): + modulus = 1 + for entry in left + right: + modulus = lcm(modulus, entry.denominator) + require(modulus <= 48, "fixture denominator too large for the direct image") + left_int = [int(entry * modulus) for entry in left] + right_int = [int(entry * modulus) for entry in right] + seen = set() + span = 2 * modulus + for coef_l in range(span): + for coef_r in range(span): + combined = [coef_l * left_int[i] + coef_r * right_int[i] for i in range(3)] + if any(entry % modulus != 0 for entry in combined): + continue + reduced = tuple((entry // modulus) % 2 for entry in combined) + seen.add(((reduced[0] + reduced[1]) & 1, reduced[2])) + require(seen, "empty parity image") + return seen + + +def form_value(family, shift, vector): + first, second, off = vector + p_shift, s_shift, t_shift = shift + if family == "AB": + return (1 + 2 * p_shift) * first + (1 + 2 * s_shift) * second + (2 * t_shift) * off + return (2 * p_shift) * first + (2 * s_shift) * second + (1 + 2 * t_shift) * off + + +def even_integer(value): + return value.denominator == 1 and value.numerator % 2 == 0 + + +def odd_integer(value): + return value.denominator == 1 and value.numerator % 2 == 1 + + +def find_extension(family, frames): + modulus = 2 + for vector in frames: + for entry in vector: + modulus = lcm(modulus, entry.denominator) + require(modulus <= 18, "extension search modulus too large") + for shift in product(range(modulus), repeat=3): + if all(even_integer(form_value(family, shift, vector)) for vector in frames): + return shift + return None + + +A = (F(1), F(0), F(0)) +B = (F(0), F(1), F(0)) +P = (F(0), F(0), F(1)) +Q = (F(1), F(1), F(-1)) +H = (F(3), F(1), F(0)) +TARGETS = ( + (F(1), F(0), F(1)), # A+P + (F(2), F(1), F(-1)), # A+Q + (F(0), F(1), F(1)), # B+P + (F(1), F(2), F(-1)), # B+Q +) +CALLS = ( + (0, A), + (2, B), + (1, P), + (1, Q), +) + + +def detected_counts(family, shift, frames): + calls = 0 + for multiplicity, vector in CALLS: + if odd_integer(form_value(family, shift, vector)): + calls += multiplicity + for vector in frames: + if odd_integer(form_value(family, shift, vector)): + calls += 1 + targets = sum(1 for vector in TARGETS if odd_integer(form_value(family, shift, vector))) + return calls, targets + + +def check_solution(frames, label): + require(len(frames) == 3, label) + total = tuple(sum(frame[i] for frame in frames) for i in range(3)) + require(total == H, label + " does not solve R+S+T=3A+B") + for frame in frames: + require(frame != (F(0), F(0), F(0)), label + " has a zero frame") + require(matrix_det(frame) == 0, label + " frame is not rank one") + image = parity_image(frames[0], frames[1]) + require((1, 1) not in image, label + " parity image contains (1,1)") + vanished = [] + if all(bit[0] == 0 for bit in image): + vanished.append("AB") + if all(bit[1] == 0 for bit in image): + vanished.append("PQ") + require(vanished, label + " loses both coordinate functionals") + for family in ("AB", "PQ"): + shift = find_extension(family, frames) + if family in vanished: + require(shift is not None, label + " missing " + family + " extension") + require(even_integer(form_value(family, shift, H)), label + " residual not even") + calls, targets = detected_counts(family, shift, frames) + require(calls == 2 and targets == 4, + label + " " + family + " detects " + str((calls, targets))) + else: + require(shift is None, label + " " + family + " extended without vanishing") + + +def explicit_frames(): + solutions = [] + # Integral nonparallel: 2A + P + Q = 3A+B. + solutions.append(( + "integral-nonparallel", + (coeffs((1, 0), 2), coeffs((1, 1), F(1, 2)), coeffs((1, -1), F(1, 2))), + )) + # Negative third frame: 5A + 2 vv^T - ww^T. + directions = ((1, 0), (1, 1), (2, 1)) + scales = solve_scales(*directions) + solutions.append(("negative-frame", tuple(coeffs(direction, scale) + for direction, scale in zip(directions, scales)))) + # Denominator in the coefficient vector. + directions = ((2, 1), (1, 1), (1, -1)) + scales = solve_scales(*directions) + solutions.append(("fractional-frame", tuple(coeffs(direction, scale) + for direction, scale in zip(directions, scales)))) + # Parallel opposite scales on A, with T = B. + solutions.append(("parallel-negative", (coeffs((1, 0), 4), coeffs((1, 0), -1), B))) + # One added label equal to the old matrix B. + solutions.append(("old-label-duplicate", (B, A, coeffs((1, 0), 2)))) + return solutions + + +def check_failures(): + good = explicit_frames()[0][1] + tampered = (good[0], good[1], tuple(good[2][i] + A[i] for i in range(3))) + total = tuple(sum(frame[i] for frame in tampered) for i in range(3)) + require(total != H, "tampered sum still equals the residual") + require(matrix_det((F(1), F(1), F(0))) != 0, "I was accepted as rank one") + identity = (F(1), F(1), F(0)) + require(matrix_det(identity) == 1, "det I changed") + # (2a+2b+2c) is even on A, B and P, so it is neither the AB nor the PQ shape. + def even_form(vector): + return 2 * vector[0] + 2 * vector[1] + 2 * vector[2] + require(even_integer(even_form(A)) and even_integer(even_form(B)) + and even_integer(even_form(P)), + "even-even-even form was not rejected by shape") + + +def main(): + check_bracket_polynomial() + check_determinant_polynomial() + check_lemma4() + check_axis_mod8() + check_quadratic_valuations() + check_valuation_gaps() + check_single_line_box() + labels = [] + for label, frames in explicit_frames(): + check_solution(frames, label) + labels.append(label) + require(labels == [ + "integral-nonparallel", + "negative-frame", + "fractional-frame", + "parallel-negative", + "old-label-duplicate", + ], "fixture list changed") + check_failures() + print("PASS three-signed-b-twice character checks") + + +if __name__ == "__main__": + main()