From 7af3a03dade6bd166ad08d7afc6879b0726fe100 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:17:57 +0000 Subject: [PATCH] Prove the (1,1,0,2) three-frame profile admits no seven-call word. The residual is I+2P, with matrix [[2,1],[1,2]]. Every rational rank-one decomposition admits an AB or PQ character detecting two calls and four targets. No selected-frontier change. Co-authored-by: unpaidmoon --- research/three-signed-q-twice/PROOF.md | 280 +++++++++ research/three-signed-q-twice/README.md | 48 ++ research/three-signed-q-twice/SOURCES.json | 18 + research/three-signed-q-twice/TASK.json | 69 +++ research/three-signed-q-twice/VERIFY.json | 34 ++ research/three-signed-q-twice/verify.py | 628 +++++++++++++++++++++ 6 files changed, 1077 insertions(+) create mode 100644 research/three-signed-q-twice/PROOF.md create mode 100644 research/three-signed-q-twice/README.md create mode 100644 research/three-signed-q-twice/SOURCES.json create mode 100644 research/three-signed-q-twice/TASK.json create mode 100644 research/three-signed-q-twice/VERIFY.json create mode 100644 research/three-signed-q-twice/verify.py diff --git a/research/three-signed-q-twice/PROOF.md b/research/three-signed-q-twice/PROOF.md new file mode 100644 index 0000000000..8f030506c5 --- /dev/null +++ b/research/three-signed-q-twice/PROOF.md @@ -0,0 +1,280 @@ +# The profile (1,1,0,2)/(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) = (1,1,0,2,1,1,1) +``` + +admits no word. Every decomposition of its 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 seventeen three-frame census profiles, including the sign-flipped profile `(1,1,2,0)/(1,1,1)`, stay open. The settled profiles `(1,1,1,1)/(1,1,1)`, `(0,2,1,1)/(1,1,1)`, and `(2,0,1,1)/(1,1,1)` are 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 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 one `A`, one `B`, no `P`, two `Q`, and three added labels `R,S,T` once each. The PR2910 determinant identity gives + +``` +R + S + T = 4I - A - B - 2Q. +``` + +Since `Q = I - P` and `I = A+B`, + +``` +4I - A - B - 2Q = I + 2P. +``` + +In coefficients that is `H = (1,1,2)`, with matrix `[[2,1],[1,2]]`. Its determinant is `3`, so `H` has rank 2. A hypothetical word produces nonzero symmetric rational rank-one `R,S,T` with `R+S+T = H`. + +One such solution is `A + B + 2P`. Section 7 excludes it by the same character that excludes every other solution. It is a witness of the test, not a census. + +Let `B(x,y) = 2 x1 y1 - x1 y2 - x2 y1 + 2 x2 y2` and `q(x) = B(x,x) = 2(x1^2 - x1 x2 + x2^2)`. Let `δ(x,y) = x1 y2 - x2 y1`. If `n = (-u2,u1)`, then `n^T H n = q(u)`, because `J^T H J` is the adjugate `[[2,-1],[-1,2]]` for the rotation `J(u1,u2) = (-u2,u1)`. The forms `3 x1 y1 + x2 y2` and `x1 y1 + 3 x2 y2` are the adjoints of `diag(1,3)` and `diag(3,1)`. Neither is this `B`: here `q(1,0) = q(0,1) = 2` and `B((1,0),(0,1)) = -1`. + +## 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 the four parities are reversed. The four targets `A+P`, `A+Q`, `B+P`, and `B+Q` all have odd `a+b` and odd `c`, so every integer shift makes all four targets odd under either family. + +On this profile, a form that is even on `R`, `S`, and `T` detects the following old calls: + +- Family AB detects the one `A` call and the one `B` call, and neither `Q` call. +- Family PQ detects both `Q` calls and the absent `P` call, hence two calls. + +Either way that is two detected calls against four detected targets. The inherited inequality forbids the pattern. It remains 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 = H - R - S` because `H` lies in `Z^3`. Here `φ(H) = (0,0)`: both `a+b = 2` and `c = 2` are even. Consequently both families are even on `H` for every integer shift. + +## 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`. On one primitive line, `θ` is proportional to the scale. Two nonparallel frames are linearly independent, because + +``` +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 homomorphism `U → Q/Z`, and 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`. An integer vector `X` satisfies `X·R ≡ -θ(R)` and `X·S ≡ -θ(S)` modulo `Z` exactly when the same congruences hold after clearing `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 the hypothesis. Hence some `X = (p,s,t)` exists. The corresponding form is even on `R` and on `S` and integer-valued on `Λ`. + +**Lemma 2.** Either extension of Lemma 1 is even on `T` as well. + +**Proof.** Both families are even on `H`, as recorded in Section 2. Then `f(T) = f(H) - f(R) - f(S)` is even. + +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. Lemmas 1 and 2 then supply a character, and Section 2 gives the forbidden count `2 < 4`. + +Because `φ(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. The third frame does not enlarge the image of a pair. + +## 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. + +**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) = 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. + +Suppose `u` is diagonal. Then `Δ` is even. The sum of the first two coefficients is `t Δ^2`. If `Δ = 0`, that sum is `0`. If `Δ ≠ 0` and the sum were an odd integer, then `v2(t) ≤ -2`, and the third coefficient `2 t u1 u2` would have valuation at most `-1`, because both direction coordinates are odd, so it would not be an integer. + +**Corollary.** If two of `R,S,T` are rational multiples of one primitive `uu^T`, then one coordinate functional vanishes on their `W`. Lemmas 1 and 2 supply a character. + +Three parallel directions cannot occur: their sum would have rank at most 1, while `det H = 3`. If exactly two directions are parallel, order those two as `R` and `S`. The corollary applies, whether or not the third direction is orthogonal to them. + +## 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. `verify.py` evaluates all 32. Odd squares are `1 (mod 8)`, and writing `β = 4t - α` leaves `4tα - 2 (mod 8)`. + +**Lemma 5.** For every primitive integer vector `u`, `v2(q(u)) = 1`. + +**Proof.** Modulo 2, squares equal the bits and `-1 ≡ 1`, so + +``` +x1^2 - x1 x2 + x2^2 ≡ x1 + x1 x2 + x2 (mod 2). +``` + +The right side is `1` for each of the three primitive classes `(1,0)`, `(0,1)`, and `(1,1)`, and those classes exhaust primitive vectors. Thus the parenthesis is odd and `q(u) = 2 · (odd)` has valuation exactly 1. + +**Proposition 6.** 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.** Evaluating the quadratic form on the perpendicular `n = (-u2,u1)` gives + +``` +c_v δ(u,v)^2 + c_w δ(u,w)^2 = q(u), +``` + +because `n·v = δ(u,v)` and `n^T H n = q(u)`. The cyclic analogues complete a linear system whose coefficient matrix has determinant `2 δ(u,v)^2 δ(u,w)^2 δ(v,w)^2 ≠ 0`, so the scales are unique. Substituting the cyclic expressions produces the bracket + +``` +δ(u,w) B(u,v) - δ(u,v) B(u,w) - q(u) δ(v,w). +``` + +This bracket vanishes for every symmetric bilinear form on a 2-dimensional space. If `ℓ(y) = B(u,y)`, the vector identity `δ(u,w) v - δ(u,v) w = δ(v,w) u` gives `δ(u,w) ℓ(v) - δ(u,v) ℓ(w) = q(u) δ(v,w)` after applying `ℓ`, since `ℓ(u) = q(u)`. `verify.py` expands the same polynomial for this particular `B` and finds no monomial. + +## 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 6, and suppose `N = kR + lS` lies in `Z^3` with `φ(N) = (1,1)`. Write `α = 2a+c`, `β = 2b+c`, and `γ = c`. All three are odd, and `α+β = 2(a+b+c) ≡ 0 (mod 4)`. Lemma 4 gives `v2(αβ-γ^2) = 1`. + +The doubled matrix `[[α,γ],[γ,β]]` equals `σ uu^T + τ vv^T`, where `σ = 2 k c_u` and `τ = 2 l c_v`. Entry comparison gives, whenever the relevant first coordinates and `δ = δ(u,v)` are nonzero, + +``` +σ = G / (u1 δ), τ = -H_ / (v1 δ), +αβ - γ^2 = -G H_ / (u1 v1), +``` + +with `G = α v2 - γ v1` and `H_ = α u2 - γ u1`. Hence `v2(G H_) = 1 + v2(u1) + v2(v1)`. + +If a direction is axial, the corresponding linear form is odd: the odd coordinate contributes an odd term and the even coordinate an even term. If the direction is diagonal, the form is a difference of two odd integers and is even. + +**Axis case.** Suppose `u1 = 0`. Primitivity gives `u = (0,ε)` with `ε = ±1`, and `q(u) = 2`. Nonparallelism forces `v1 ≠ 0` and `w1 ≠ 0`. The scale formulas collapse to + +``` +c_u = B(v,w) / (v1 w1), c_v = (2 w2 - w1) / (v1 δ(v,w)). +``` + +Both signs `ε = ±1` give the same expressions: the factors of `ε` in `B(w,u)` and in `δ(v,u)` cancel, and `δ(u,v) δ(u,w) = v1 w1`. The doubled matrix has `α = τ v1^2` and `γ = τ v1 v2`. Oddness of `α` forces `v1` odd and `v2(τ) = 0`, and then oddness of `γ` forces `v2` odd. Thus `v` is diagonal. Also `l ≠ 0`: otherwise `N` would be a multiple of `uu^T`, which Lemma 3 forbids. Equating the two formulas for `c_v` gives + +``` +(v1 w2 - v2 w1) α = 2 l v1 (2 w2 - w1). +``` + +The coefficient of `w1` on the rearranged equation is `2 l v1 - α v2`, which is even minus odd, hence odd and nonzero. If `w2 = 0`, that equation forces `w1 = 0`, which is impossible. Thus `w2 ≠ 0`, and + +``` +w1 = v1 w2 (4l - α) / (2 l v1 - α v2). +``` + +Here `4l - α` is even minus odd, hence odd and nonzero, so `w1 ≠ 0` as well. Substituting `r = w2/w1` into `c_u = 2 - r - v2/v1 + 2 v2 r / v1` and clearing the denominator `v1^2 (4l-α)` produces the numerator identity + +``` +(2 v1 - v2) v1 (4l - α) + (2 l v1 - α v2)(2 v2 - v1) + = 2(-α Q + 3 l v1^2), +``` + +where `Q = v1^2 - v1 v2 + v2^2`. Thus + +``` +c_u = 2(-α Q + 3 l v1^2) / (v1^2 (4l - α)). +``` + +`verify.py` expands this six-factor polynomial and finds that the two sides agree. The relation `αβ-γ^2 = σ α`, coming from `α = τ v1^2` and `αβ-γ^2 = σ τ v1^2`, rearranges `k c_u = (αβ-γ^2)/(2α)` into + +``` +v1^2 (4l - α)(αβ - γ^2) + 4 α k (α Q - 3 l v1^2) = 0. +``` + +The factor `4` is `2` from `σ = 2 k c_u` times the `2` in the numerator of `c_u`. It is not the constant `6` of the `diag(1,3)` axis equation. `verify.py` checks that this display is the cleared scale condition. + +Under the oddness hypotheses, `v1` is odd, `4l-α` is odd, and `αβ-γ^2` has valuation exactly 1, so the first summand has valuation exactly 1. The second summand is divisible by `4`, so its valuation is at least 2. Their sum cannot be zero. Therefore `u1 ≠ 0`. Exchanging the two summands gives `v1 ≠ 0`. + +**Cramer case.** Both first coordinates are nonzero, and `δ ≠ 0`. The entry comparison above gives `v2(G H_) = 1 + v2(u1) + v2(v1)`. + +Both directions axial, and both directions diagonal, are 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: an axial-diagonal cross product is odd minus even, or even minus odd. + +Equating the Cramer formulas with Proposition 6 gives + +``` +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 (2 v1 - v2) + G u2 2 k u1 (2 v2 - v1) - G u1 | +| 2 l v1 (2 u1 - u2) + H_ v2 2 l v1 (2 u2 - u1) - 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 δ, +``` + +with this residual's `q`. `verify.py` expands both polynomials and finds that they agree. The existing direction `w` is a nontrivial kernel vector, so the determinant is zero. + +Suppose `u` is axial and `v` is diagonal. Then `v2(H_) = 0`, `v1` is odd, `v2(δ) = 0`, and `v2(G) = 1 + v2(u1)`. The constant term has valuation exactly `1 + v2(u1)`. The `l` term has valuation at least `3 + v2(u1)`, because it carries a factor `2`, the factor `G`, and `q(u)` of valuation 1. The `k` term has valuation at least `2 + v2(u1)`, from the factor `2` and `q(v)`. The `kl` term has valuation at least `2 + v2(u1)`, from the factor `12`. Each is strictly larger than the constant valuation, whether or not `k` or `l` is divisible by 2. The determinant is nonzero. + +Suppose `u` is diagonal and `v` is axial. Then `v2(G) = 0` and `v2(H_) = 1 + v2(v1)`. The constant term has valuation `1 + v2(v1)`. The `l` term has valuation at least `2 + v2(v1)`, the `k` term at least `3 + v2(v1)`, and the `kl` term at least `2 + v2(v1)`. Again the constant term is strictly smaller. + +This contradiction shows that no vector of `W` has image `(1,1)`. + +## 7. Conclusion + +**Theorem.** The profile `(1,1,0,2,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 = I+2P`. If two directions are parallel, Section 4 supplies a character. If all three directions are distinct, Section 6 shows that the parity image of every pair 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 rational solution `A+B+2P` is the fixture `rational-rank-one`. Its PQ character, the unshifted form `f(a,b,c) = c`, is even on all three frames, odd on both `Q` calls, and odd on all four targets. The finite fixture list, the single-line box, the axis-reduction box, and the residue checks are not this theorem. Sections 4 through 6 are. Lemma 4, Lemma 5, and the polynomial identities are exhaustive finite or exact-expansion arguments. + +## Open next questions + +Seventeen three-frame count profiles from the census in discussion comment 19377345 remain open. This file settles only `(1,1,0,2)/(1,1,1)`. The sign-flipped tuple `(1,1,2,0)/(1,1,1)` has residual `[[2,-1],[-1,2]]` and is not implied by the calculation above. A useful first step for any one of the seventeen is to read that printed tuple, write its own determinant residual, and test one rational rank-one solution with that residual's bilinear form. The form in Section 1 does not transfer. + +Four or more added frames are outside this three-summand argument. diff --git a/research/three-signed-q-twice/README.md b/research/three-signed-q-twice/README.md new file mode 100644 index 0000000000..9a83d6ec46 --- /dev/null +++ b/research/three-signed-q-twice/README.md @@ -0,0 +1,48 @@ +# Three signed frames, old profile (1,1,0,2) + +**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) = (1,1,0,2,1,1,1) +``` + +admits no word. The determinant equation is `R+S+T = I+2P`, with matrix `[[2,1],[1,2]]` and coefficient vector `(1,1,2)`. 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 `(1,1,0,2)` with added multiplicities `(1,1,1)`. It is one of the twelve profiles listed there with 24 positive-dimensional spaces. It is not `(1,1,1,1)`, `(0,2,1,1)`, or `(2,0,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 `(2,0,1,1)` exclusion. + +Evidence class: **proof**, for this profile and these hypotheses only. Lemma 4 is an exhaustive check of its 32 residue classes. Lemma 5 is the three primitive classes modulo 2. The scale bracket, the axis numerator, the axis rearrangement, and the Cramer determinant are polynomial identities, expanded in full by `verify.py`. The single-line box and the axis-reduction box are finite corroborations. 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 rational solution tested with this residual's bilinear form is `A+B+2P`. Its unshifted PQ character detects two calls and four targets. The same character covers every other rational solution. + +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-q-twice --check-only +python3 scripts/research_package.py --package research/three-signed-q-twice +``` + +The direct check is `python3 -I -W error -B research/three-signed-q-twice/verify.py`. + +## Open next questions + +Which of the other seventeen three-frame count profiles survive the same test? A useful first step is to read one tuple that discussion comment 19377345 already prints, other than `(1,1,1,1)`, `(0,2,1,1)`, `(2,0,1,1)`, and `(1,1,0,2)`, write that tuple's own determinant residual, and test one rational rank-one solution with the bilinear form of that residual. The sign-flipped tuple `(1,1,2,0)/(1,1,1)` has residual `[[2,-1],[-1,2]]` and is not settled here. The form `2 x1 y1 - x1 y2 - x2 y1 + 2 x2 y2` belongs to `[[2,1],[1,2]]` and does not transfer. No uniform reduction among the remaining profiles is supplied. + +Four or more added signed rank-one frames are outside this three-summand character and are not a next question of this package. + +## 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 is Nick Petalas's discussion comment 19377345. The released all-old-once handoff is comment 19377832. The `(0,2,1,1)` and `(2,0,1,1)` exclusions are unpaidmoon PRs #7013 and #7035. Those three profiles are 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-q-twice/SOURCES.json b/research/three-signed-q-twice/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/three-signed-q-twice/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/three-signed-q-twice/TASK.json b/research/three-signed-q-twice/TASK.json new file mode 100644 index 0000000000..cdbed32850 --- /dev/null +++ b/research/three-signed-q-twice/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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 I+2P = R+S+T into nonzero symmetric rank-one matrices is first-order character-excluded, and therefore the seven-call profile (a,b,p,q,r,s,t)=(1,1,0,2,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 one three-frame census profile left open by the (2,0,1,1) exclusion.", + "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 character proof for the single printed profile (1,1,0,2)/(1,1,1), or after one explicit rational solution of that profile whose parity image contains (1,1). Do not survey the other printed profiles and do not take four or more added frames.", + "outcome": "completed", + "evidence": "Elementary character proof for every rational rank-one solution of R+S+T=I+2P: 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 bracket, axis numerator, axis rearrangement, and Cramer determinant are expanded polynomial identities. Lemma 4 exhausts 32 residue classes and Lemma 5 exhausts the three primitive classes modulo 2. Finite fixtures 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 seventeen three-frame count profiles printed in discussion comment 19377345 survive the same AB/PQ test?", + "why_it_matters": "Only (1,1,1,1), (0,2,1,1), (2,0,1,1), and (1,1,0,2), each with added multiplicities (1,1,1), are character-excluded. A surviving profile would be the next place a seven-call word could exist.", + "first_step": "Read one tuple that comment 19377345 already prints, other than those four, write that tuple's own determinant residual, and test one rational rank-one solution with the bilinear form of that residual. The sign-flipped tuple (1,1,2,0)/(1,1,1) has residual [[2,-1],[-1,2]] and is not settled here.", + "blocked_by": "No uniform reduction among the remaining profiles is supplied, and the bilinear form 2 x1 y1 - x1 y2 - x2 y1 + 2 x2 y2 does not transfer off [[2,1],[1,2]]." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345", + "upstream_checked_utc": "2026-11-10T10:14:20Z", + "priority_revision": 8 + } +} diff --git a/research/three-signed-q-twice/VERIFY.json b/research/three-signed-q-twice/VERIFY.json new file mode 100644 index 0000000000..693fea98da --- /dev/null +++ b/research/three-signed-q-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, axis-numerator, axis-rearrangement, and Cramer-determinant polynomial identities; mod-8 discriminant lemma; mod-4 axis obstruction; primitive quadratic valuation; explicit characters on five declared frames, each detecting two calls and four targets; failure controls for a tampered sum, I as a summand, an even-even-even form, and the diag(1,3) and diag(3,1) bilinear forms." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same identities, lemmas, fixtures, and failure controls under python -O." + } + ] +} diff --git a/research/three-signed-q-twice/verify.py b/research/three-signed-q-twice/verify.py new file mode 100644 index 0000000000..f3c29bee30 --- /dev/null +++ b/research/three-signed-q-twice/verify.py @@ -0,0 +1,628 @@ +"""Character exclusion for the seven-call profile (1,1,0,2)/(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 discriminant lemma, the mod-4 axis obstruction, the +quadratic valuation of this residual, explicit characters on declared +frames, and failure controls. The finite boxes are not the proof. +""" + +from fractions import Fraction as F +from itertools import product +from math import gcd + + +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 scale(self, factor): + return Poly({key: factor * value for key, value in self.terms.items()}) + + +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. + + B(x,y) = 2 x1 y1 - x1 y2 - x2 y1 + 2 x2 y2 and + q(x) = 2 x1^2 - 2 x1 x2 + 2 x2^2. These belong to the residual + [[2,1],[1,2]], not to diag(1,3) or diag(3,1). + """ + width = 6 + u1, u2, v1, v2, w1, w2 = (var(i, width) for i in range(width)) + two = const(2, width) + + def bilinear(x1, x2, y1, y2): + return ( + two.mul(x1).mul(y1) + .add(x1.mul(y2), scale=-1) + .add(x2.mul(y1), scale=-1) + .add(two.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 ( + two.mul(x1).mul(x1) + .add(two.mul(x1).mul(x2), scale=-1) + .add(two.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 for this residual.""" + width = 8 + kay, ell, u1, u2, v1, v2, gee, hhh = (var(i, width) for i in range(width)) + two = const(2, width) + + def quad(x1, x2): + return ( + two.mul(x1).mul(x1) + .add(two.mul(x1).mul(x2), scale=-1) + .add(two.mul(x2).mul(x2)) + ) + + row11 = two.mul(kay).mul(u1).mul(two.mul(v1).add(v2, scale=-1)).add(gee.mul(u2)) + row12 = two.mul(kay).mul(u1).mul(two.mul(v2).add(v1, scale=-1)).add(gee.mul(u1), scale=-1) + row21 = two.mul(ell).mul(v1).mul(two.mul(u1).add(u2, scale=-1)).add(hhh.mul(v2)) + row22 = two.mul(ell).mul(v1).mul(two.mul(u2).add(u1, scale=-1)).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) + closed = ( + delta.mul(gee).mul(hhh) + .add(two.mul(ell).mul(gee).mul(v1).mul(quad(u1, u2))) + .add(two.mul(kay).mul(hhh).mul(u1).mul(quad(v1, v2)), scale=-1) + .add(const(12, width).mul(kay).mul(ell).mul(u1).mul(v1).mul(delta), scale=-1) + ) + require(matrix_det.terms == closed.terms, "determinant polynomial mismatch") + + +def check_axis_numerator(): + """Clearing w from the vertical scale formulas gives the displayed numerator. + + c_u = 2(-α Q + 3 l v1^2) / (v1^2 (4l-α)), with Q = v1^2 - v1 v2 + v2^2. + """ + width = 4 + alpha, ell, v1, v2 = (var(i, width) for i in range(width)) + two = const(2, width) + four = const(4, width) + gap = four.mul(ell).add(alpha, scale=-1) + den_w = two.mul(ell).mul(v1).add(alpha.mul(v2), scale=-1) + left = two.mul(v1).add(v2, scale=-1).mul(v1).mul(gap).add( + den_w.mul(two.mul(v2).add(v1, scale=-1)) + ) + quad = v1.mul(v1).add(v1.mul(v2), scale=-1).add(v2.mul(v2)) + right = two.mul(alpha).mul(quad).add( + two.mul(const(3, width)).mul(ell).mul(v1).mul(v1), scale=-1 + ) + # right was built as 2αQ - 6 l v1^2; the displayed numerator is the negative. + require(left.add(right).terms == {}, "axis numerator identity failed") + + +def check_axis_rearrangement(): + """k c_u = (αβ-γ^2)/(2α) rearranges to the displayed axis equation.""" + width = 7 + alpha, beta, gamma, kay, ell, v1, v2 = (var(i, width) for i in range(width)) + two = const(2, width) + four = const(4, width) + three = const(3, width) + quad = v1.mul(v1).add(v1.mul(v2), scale=-1).add(v2.mul(v2)) + numer = two.mul(alpha).mul(quad).add(two.mul(three).mul(ell).mul(v1).mul(v1), scale=-1).scale(-1) + gap = four.mul(ell).add(alpha, scale=-1) + den = v1.mul(v1).mul(gap) + disc = alpha.mul(beta).add(gamma.mul(gamma), scale=-1) + scale_cleared = two.mul(alpha).mul(kay).mul(numer).add(disc.mul(den), scale=-1) + displayed = den.mul(disc).add(four.mul(alpha).mul(kay).mul(alpha.mul(quad).add(three.mul(ell).mul(v1).mul(v1), scale=-1))) + require(scale_cleared.add(displayed).terms == {}, "axis rearrangement is not an identity") + + +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_mod4(): + """The cleared axis sides cannot agree: left is 2 mod 4, right is 0 mod 4.""" + odds = (1, 3, 5, 7) + seen = 0 + for alpha in odds: + for four_l in (0, 4): + gap = (four_l - alpha) % 8 + require(gap % 2 == 1, "4l-α became even") + for det_mod in (2, 6): + for v1 in odds: + seen += 1 + left = (v1 * v1 * gap * det_mod) % 8 + require(left in (2, 6), "axis left residue " + str(left)) + require(left % 4 == 2, "axis left lost exact valuation 1") + require(seen == 64, "expected 64 axis residue classes, found " + str(seen)) + for kay in range(-6, 7): + for block in range(-6, 7): + right = 4 * kay * block + require(right % 4 == 0, "factor 4 failed to clear mod 4") + + +def check_quadratic_valuation(): + """Every primitive vector has q ≡ 2 (mod 4). The mod-2 classes are exhaustive.""" + seen = 0 + for u1 in (0, 1): + for u2 in (0, 1): + if (u1, u2) == (0, 0): + continue + seen += 1 + parenthesis = u1 * u1 - u1 * u2 + u2 * u2 + require(parenthesis % 2 == 1, "primitive parenthesis even " + str((u1, u2))) + require((2 * parenthesis) % 4 == 2, "q lost valuation 1") + require(seen == 3, "expected 3 primitive mod-2 classes") + for u1, u2 in product(range(-8, 9), repeat=2): + if gcd(abs(u1), abs(u2)) != 1: + continue + value = 2 * (u1 * u1 - u1 * u2 + u2 * u2) + require(value % 4 == 2, "primitive q not 2 mod 4 " + str((u1, u2, value))) + require(value != 0, "primitive q vanished") + + +def valuation_gap(shift, orientation): + """Lower bounds in the Cramer case stay strictly above the constant term.""" + if orientation == "axial-diagonal": + constant = 1 + shift + l_term = 3 + shift + k_term = 2 + shift + kl_term = 2 + shift + elif orientation == "diagonal-axial": + constant = 1 + shift + l_term = 2 + shift + k_term = 3 + shift + kl_term = 2 + shift + else: + raise ValueError("unknown orientation") + require(l_term > constant and k_term > constant and kl_term > constant, + "valuation gap collapsed at " + orientation + " " + str(shift)) + + +def check_valuation_gaps(): + for shift in range(0, 12): + valuation_gap(shift, "axial-diagonal") + valuation_gap(shift, "diagonal-axial") + + +def egcd(a, b): + if b == 0: + if a >= 0: + return 1, 0, a + return -1, 0, -a + x, y, g = egcd(b, a % b) + return y, x - (a // b) * y, g + + +def cong_basis(c1, c2, modulus): + """Z-basis of {(z1,z2): c1 z1 + c2 z2 ≡ 0 mod modulus}.""" + if modulus == 1: + return [(1, 0), (0, 1)] + c1 %= modulus + c2 %= modulus + g = gcd(gcd(c1, c2), modulus) + c1 //= g + c2 //= g + modulus //= g + if modulus == 1: + return [(1, 0), (0, 1)] + g2 = gcd(c1, c2) + require(g2 != 0, "congruence basis divided by zero") + c1 //= g2 + c2 //= g2 + x_bez, y_bez, g_bez = egcd(c1, c2) + require(g_bez == 1, "bezout failed") + return [(c2, -c1), (modulus * x_bez, modulus * y_bez)] + + +def intersect_congruence(basis, c1, c2, modulus): + b1, b2 = basis + d1 = c1 * b1[0] + c2 * b1[1] + d2 = c1 * b2[0] + c2 * b2[1] + z_basis = cong_basis(d1, d2, modulus) + return [ + (z1 * b1[0] + z2 * b2[0], z1 * b1[1] + z2 * b2[1]) + for z1, z2 in z_basis + ] + + +def check_congruence_basis(): + """The congruence basis matches brute force on a finite rectangle.""" + checked = 0 + for modulus in range(1, 7): + for c1 in range(0, 9): + for c2 in range(0, 9): + basis = cong_basis(c1, c2, modulus) + g = gcd(gcd(c1, c2), modulus) + det = basis[0][0] * basis[1][1] - basis[0][1] * basis[1][0] + require(abs(det) == modulus // g, "congruence index " + str((c1, c2, modulus))) + for vector in basis: + require((c1 * vector[0] + c2 * vector[1]) % modulus == 0, "generator misses congruence") + for kay in range(modulus): + for ell in range(modulus): + if (c1 * kay + c2 * ell) % modulus: + continue + checked += 1 + z1 = kay * basis[1][1] - ell * basis[1][0] + z2 = -kay * basis[0][1] + ell * basis[0][0] + require(z1 % det == 0 and z2 % det == 0, + "brute solution outside the basis") + require(checked > 100, "congruence self-test checked too little") + + +def bilinear(left, right): + return F( + 2 * left[0] * right[0] + - left[0] * right[1] + - left[1] * right[0] + + 2 * left[1] * right[1] + ) + + +def diag13_bilinear(left, right): + return F(3 * left[0] * right[0] + left[1] * right[1]) + + +def diag31_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, form=bilinear): + return ( + form(second, third) / (cross(first, second) * cross(first, third)), + form(third, first) / (cross(second, third) * cross(second, first)), + form(first, second) / (cross(third, first) * cross(third, second)), + ) + + +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(8): + 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(-8, 9): + if numerator == 0: + continue + for denominator in range(1, 9): + 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 check_axis_reduction_box(): + """On a finite box, the vertical scale formulas match the general formula.""" + checked = 0 + for sign in (1, -1): + vertical = (0, sign) + for left in primitive_directions(6): + if left[0] == 0: + continue + for right in primitive_directions(6): + if right[0] == 0 or cross(left, right) == 0: + continue + if cross(vertical, left) == 0 or cross(vertical, right) == 0: + continue + if bilinear(left, right) == 0 or bilinear(vertical, left) == 0 or bilinear(vertical, right) == 0: + continue + scales = solve_scales(vertical, left, right) + reduced_u = bilinear(left, right) / (F(left[0]) * F(right[0])) + reduced_v = (2 * right[1] - right[0]) / (F(left[0]) * cross(left, right)) + require(scales[0] == reduced_u, "axis c_u reduction " + str((left, right, sign))) + require(scales[1] == reduced_v, "axis c_v reduction " + str((left, right, sign))) + checked += 1 + require(checked > 100, "axis-reduction box checked too little") + + +def parity_image(left, right): + modulus = 1 + for entry in left + right: + modulus = modulus // gcd(modulus, entry.denominator) * entry.denominator + numer_left = [entry.numerator * (modulus // entry.denominator) for entry in left] + numer_right = [entry.numerator * (modulus // entry.denominator) for entry in right] + basis = [(1, 0), (0, 1)] + for a_coef, b_coef in zip(numer_left, numer_right): + basis = intersect_congruence(basis, a_coef, b_coef, modulus) + images = {(0, 0)} + phis = [] + for kay, ell in basis: + combined = tuple(kay * left[i] + ell * right[i] for i in range(3)) + require(all(entry.denominator == 1 for entry in combined), "lattice generator was not integral") + parity = ((int(combined[0]) + int(combined[1])) & 1, int(combined[2]) & 1) + phis.append(parity) + images.add(parity) + images.add(((phis[0][0] + phis[1][0]) & 1, (phis[0][1] + phis[1][1]) & 1)) + return images + + +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 = modulus // gcd(modulus, entry.denominator) * entry.denominator + modulus *= 2 + require(modulus <= 36, "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(1), F(1), F(2)) +DIAG13 = (F(1), F(3), F(0)) +DIAG31 = (F(3), F(1), F(0)) +TARGETS = ( + (F(1), F(0), F(1)), + (F(2), F(1), F(-1)), + (F(0), F(1), F(1)), + (F(1), F(2), F(-1)), +) +CALLS = ( + (1, A), + (1, B), + (0, P), + (2, 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=(1,1,2)") + require(total != DIAG13 and total != DIAG31, label + " solved a diagonal sibling residual") + 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 = [] + directions = ((1, 0), (0, 1), (1, 1)) + scales = solve_scales(*directions) + require(scales == (F(1), F(1), F(1)), "rational solution scales changed " + str(scales)) + solutions.append(("rational-rank-one", tuple( + coeffs(direction, scale) for direction, scale in zip(directions, scales) + ))) + directions = ((0, 1), (1, -3), (1, -2)) + scales = solve_scales(*directions) + require(any(scale < 0 for scale in scales), "negative fixture has no negative scale") + solutions.append(("negative-frame", tuple( + coeffs(direction, scale) for direction, scale in zip(directions, scales) + ))) + directions = ((0, 1), (1, -3), (1, -1)) + scales = solve_scales(*directions) + require(any(scale.denominator != 1 for scale in scales), "fractional fixture is integral") + solutions.append(("fractional-frame", tuple( + coeffs(direction, scale) for direction, scale in zip(directions, scales) + ))) + solutions.append(( + "parallel-opposite", + (coeffs((1, 1), 2), coeffs((1, 1), F(-1, 2)), coeffs((1, -1), F(1, 2))), + )) + solutions.append(("old-label-duplicate", (P, coeffs((1, 1), 1), Q))) + return solutions + + +def check_label_counts(): + """Every integer shift detects two old calls and four targets, before frames.""" + for shift in product(range(4), repeat=3): + for family, expected in (("AB", 2), ("PQ", 2)): + calls, targets = detected_counts(family, shift, ()) + require(calls == expected and targets == 4, + "old-label count " + family + " " + str((shift, calls, targets))) + require(even_integer(form_value(family, shift, H)), + "residual parity depends on the shift") + + +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") + identity = (F(1), F(1), F(0)) + require(matrix_det(identity) == 1, "det I changed") + require(matrix_det(H) == 3, "residual determinant changed") + + 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)) and even_integer(even_form(Q)), + "even-even-even form was not rejected by shape") + directions = ((1, 0), (0, 1), (1, 1)) + for form, sibling in ((diag13_bilinear, DIAG13), (diag31_bilinear, DIAG31)): + sibling_frames = tuple( + coeffs(direction, scale) + for direction, scale in zip(directions, solve_scales(*directions, form=form)) + ) + sibling_total = tuple(sum(frame[i] for frame in sibling_frames) for i in range(3)) + require(sibling_total == sibling, "diagonal form stopped solving its own residual") + require(sibling_total != H, "diagonal form solved this residual") + require(bilinear((1, 0), (0, 1)) == -1, "cross term of this residual vanished") + require(bilinear((1, 0), (1, 0)) == 2 and bilinear((0, 1), (0, 1)) == 2, + "diagonal values of q changed") + + +def main(): + check_bracket_polynomial() + check_determinant_polynomial() + check_axis_numerator() + check_axis_rearrangement() + check_lemma4() + check_axis_mod4() + check_quadratic_valuation() + check_valuation_gaps() + check_congruence_basis() + check_single_line_box() + check_axis_reduction_box() + check_label_counts() + labels = [] + for label, frames in explicit_frames(): + check_solution(frames, label) + labels.append(label) + require(labels == [ + "rational-rank-one", + "negative-frame", + "fractional-frame", + "parallel-opposite", + "old-label-duplicate", + ], "fixture list changed") + check_failures() + print("PASS three-signed-q-twice character checks") + + +if __name__ == "__main__": + main()