From e0026d8fd0d8c3eef46391e3e3e540c15279eec5 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 08:54:22 +0000 Subject: [PATCH] Prove the (2,0,1,1) three-frame profile admits no seven-call word. The residual is A+3B = diag(1,3). Every rational rank-one solution admits an AB or PQ character detecting two calls and four targets. No selected-frontier change. Co-authored-by: unpaidmoon --- research/three-signed-a-twice/PROOF.md | 300 ++++++++++++ research/three-signed-a-twice/README.md | 48 ++ research/three-signed-a-twice/SOURCES.json | 18 + research/three-signed-a-twice/TASK.json | 71 +++ research/three-signed-a-twice/VERIFY.json | 34 ++ research/three-signed-a-twice/verify.py | 501 +++++++++++++++++++++ 6 files changed, 972 insertions(+) create mode 100644 research/three-signed-a-twice/PROOF.md create mode 100644 research/three-signed-a-twice/README.md create mode 100644 research/three-signed-a-twice/SOURCES.json create mode 100644 research/three-signed-a-twice/TASK.json create mode 100644 research/three-signed-a-twice/VERIFY.json create mode 100644 research/three-signed-a-twice/verify.py diff --git a/research/three-signed-a-twice/PROOF.md b/research/three-signed-a-twice/PROOF.md new file mode 100644 index 0000000000..4f87ed97c7 --- /dev/null +++ b/research/three-signed-a-twice/PROOF.md @@ -0,0 +1,300 @@ +# The profile (2,0,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) = (2,0,1,1,1,1,1) +``` + +admits no word. The determinant equation is `R+S+T = A+3B = diag(1,3)`. Every decomposition of that residual by three nonzero symmetric rational rank-one matrices admits an additive character that detects two calls and four targets. + +Evidence class: **proof**, for this profile and these hypotheses only. It is not a multiplication theorem, not a search, and not a certificate that changes the selected κ `781451/250000000`. Rational solutions of the matrix equation exist; the named solution `2B+P+Q` is one. The obstruction is the character, not the absence of a rank-one decomposition. The other eighteen three-frame census profiles, and every decomposition with four or more added frames, stay open. The settled profiles `(1,1,1,1)/(1,1,1)` and `(0,2,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. + +The bilinear form used below is `B(x,y) = 3 x1 y1 + x2 y2`. The constants 3, 6, and 12 of the `(0,2,1,1)` argument belonged to `3A+B = diag(3,1)` and are not reused. Where a 3, a 6, or a 12 appears here, it is recomputed from `diag(1,3)`. + +## 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 `A` calls, no `B` call, one `P` call, one `Q` call, and three added labels `R,S,T` once each. The PR2910 determinant identity gives + +``` +R + S + T = 4I - 2A - P - Q. +``` + +Since `P+Q = I` and `I = A+B`, + +``` +4I - 2A - P - Q = 3I - 2A = A + 3B = diag(1,3). +``` + +Write `H = A+3B`, with coefficient vector `(1,3,0)`. A hypothetical word produces nonzero symmetric rational rank-one `R,S,T` satisfying `R+S+T = H`. One such decomposition is `2B + P + Q`, since `P+Q = A+B`. The character below rules out every such triple, including this one, so it rules out every triple that a word could produce. + +Let `B(x,y) = 3 x1 y1 + x2 y2` and `q(x) = B(x,x) = 3 x1^2 + x2^2`. Let `δ(x,y) = x1 y2 - x2 y1`. For the perpendicular `n = (-u2, u1)` one has `n^T H n = q(u)`. + +## 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 parities are reversed. Either evaluation uses `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 `A` calls and no `B` call, because `a = 2` and `b = 0`. +- 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 follows 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 + +``` +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)·1 + (1+2s)·3 = 4 + even` on `H = (1,3,0)`. The PQ form takes `2p·1 + 2s·3`, 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) = 1`. + +Suppose `u` is horizontal, so `u1` is odd, `u2` is even, and `Δ` is odd. The first coefficient is `a = t u1 Δ` and the third is `c = 2 t u1 u2`, so `c = 2 a u2 / Δ` once `a` is an integer. Thus `Δ` divides `2 a u2`. The divisor `Δ` is coprime to `2` and to `u2`, so `Δ` divides `a`. Writing `a = Δ a1` produces `t = a1/u1`. The second coefficient is then `-a1 u2 Δ / u1`. Coprimality of `u1` with both `Δ` and `u2` forces `u1 | a1`, so `t` is an integer. The third coefficient is divisible by the even integer `u2`. + +The vertical case exchanges the two diagonal entries. The odd coordinate is the second one, and the third coefficient is divisible by the even first coordinate. + +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`, then `v2(Δ^2) ≥ 2`. An odd value of the sum would force `v2(t) ≤ -2`. The third coefficient `2 t u1 u2` would then 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(1,3)` 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. Odd squares are `1 (mod 8)`, and writing `β = 4t-α` leaves `4tα - 2 (mod 8)`, which is `2` or `6`. + +**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. 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 for `c_v` and `c_w` produces the bracket + +``` +δ(u,w) B(u,v) - δ(u,v) B(u,w) - q(u) δ(v,w). +``` + +Expand the first two products. With `B(u,v) = 3 u1 v1 + u2 v2`, + +``` +δ(u,w) B(u,v) = 3 u1^2 v1 w2 + u1 u2 v2 w2 - 3 u1 u2 v1 w1 - u2^2 v2 w1, +δ(u,v) B(u,w) = 3 u1^2 v2 w1 + u1 u2 v2 w2 - 3 u1 u2 v1 w1 - u2^2 v1 w2. +``` + +The terms `± u1 u2 v2 w2` and `± 3 u1 u2 v1 w1` cancel. The remainder is + +``` +3 u1^2 (v1 w2 - v2 w1) + u2^2 (v1 w2 - v2 w1) = 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 `[[α,γ],[γ,β]]` 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`. The determinant identity is `αβ-γ^2 = σ τ δ^2`, and the two formulas agree because `G H_ = -σ τ u1 v1 δ^2`. + +**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 = 3 + v2 w2 / (v1 w1), c_v = w2 / (δ(v,w) v1). +``` + +The factor `3` is `q(u)/u2^2` for this vertical `u`, and the second formula has no extra factor of `3`: `B(w,u) = ε w2` and `δ(v,u) = ε v1`. The doubled matrix has `α = τ v1^2` and `γ = τ v1 v2`. 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` gives `v2(σ) = 1`. Equating the two formulas for `c_v` gives + +``` +δ(v,w) = 2 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`. Here `v2` is odd, so that cross product is nonzero and the right side cannot vanish. Thus `w2 ≠ 0`. Solving for `w1` gives + +``` +w1 = v1 w2 (α - 2l) / (α v2). +``` + +The same doubled-matrix identity gives `k c_u = (αβ-γ^2)/(2α)`. Substituting `c_u` and then `w1` produces + +``` +(α-2l) v1^2 (αβ-γ^2 - 6α k) = 2 α^2 k v2^2. +``` + +The `6` is `2·3`, from the leading `3` in `c_u` together with the factor `2` in `σ = 2 k c_u`. It is not the `6` of the `diag(3,1)` axis equation. Since `α` is odd, `α-2l` is odd, hence nonzero. Here `α`, `v1`, and `v2` are odd. + +If `v2(k) ≥ 1`, then `v2(6αk) ≥ 2` while `v2(αβ-γ^2) = 1`, so the bracket has valuation 1. The left side has valuation 1 and the right side has valuation at least 2. + +If `v2(k) = 0`, both `αβ-γ^2` and `6αk` are congruent to `2` or `6` modulo 8. Their difference is congruent to `0` or `4` modulo 8, so its valuation is at least 2. The right side is `2·(odd)` and has valuation exactly 1. In particular `k ≠ 0`, so the right side is not zero. + +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`. The entry comparison above gives + +``` +v2(G H_) = 1 + v2(u1) + v2(v1). +``` + +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 two 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 + +``` +2 k u1 B(v,w) = G δ(u,w), 2 l v1 B(u,w) = H_ δ(v,w). +``` + +In coordinates `(w1,w2)`, and with this residual's bilinear form, the coefficient matrix is + +``` +| 6 k u1 v1 + G u2 2 k u1 v2 - G u1 | +| 6 l u1 v1 + H_ v2 2 l v1 u2 - H_ v1 |. +``` + +The `6` multiplies the first-coordinate part of `B` and the `2` multiplies the second-coordinate part. Its determinant expands to + +``` +δ G H_ + 2 l G v1 q(u) - 2 k H_ u1 q(v) - 12 k l u1 v1 δ, +``` + +where `q(u) = 3 u1^2 + u2^2` and `q(v) = 3 v1^2 + v2^2`. The grouping checked as a polynomial identity in `verify.py` is: 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)` and `3·1+1 = 4`. 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, whether the odd coordinate is the first one, carrying the coefficient 3, or the second. Thus its quadratic valuation is 0. Neither value is zero, because both squares are nonnegative and a primitive vector is nonzero. + +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 `(2,0,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 = A+3B`. 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 named rational solution `2B+P+Q` is the fixture `rational-rank-one`: its AB character detects two calls and four targets. The finite fixture list, the single-line box, the axis-reduction box, and the valuation-arithmetic checks are not this theorem. Sections 4 through 6 are. Lemma 4 and the polynomial identities are exhaustive finite or exact-expansion arguments. + +## Open next questions + +Eighteen three-frame count profiles from the census in discussion comment 19377345 remain open. This file does not name one. A useful first step is to read one tuple that comment already prints, other than `(1,1,1,1)`, `(0,2,1,1)`, and `(2,0,1,1)`, and to compute that tuple's own residual before choosing a bilinear form. + +Four or more added frames are outside this three-summand argument and are not given a profile here. diff --git a/research/three-signed-a-twice/README.md b/research/three-signed-a-twice/README.md new file mode 100644 index 0000000000..42028bcfe0 --- /dev/null +++ b/research/three-signed-a-twice/README.md @@ -0,0 +1,48 @@ +# Three signed frames, old profile (2,0,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) = (2,0,1,1,1,1,1) +``` + +admits no word. The determinant equation is `R+S+T = A+3B = diag(1,3)`. 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 the named sibling of the `(0,2,1,1)/(1,1,1)` exclusion: old counts `(2,0,1,1)` with added multiplicities `(1,1,1)`. The census is [discussion comment 19377345](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345). The question was left open by [PR #7013](https://github.com/CrocSwap/integer-mult-bounds/pull/7013) and its finding, [discussion comment 19507678](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507678). It is not the settled all-old-once profile `(1,1,1,1)/(1,1,1)`, and it does not redo `(0,2,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 `(0,2,1,1)` character proof. That proof itself followed the all-old-once exclusion of the three-frame question in [research/bit-two-signed-frame-floor](../bit-two-signed-frame-floor). No further construction round is opened. + +Evidence class: **proof**, for this profile and these hypotheses only. The scale bracket, the Cramer determinant, and the axis rearrangement are polynomial identities, expanded in full by `verify.py`. Lemma 4 is an exhaustive check of its 32 residue classes. The single-line box is a finite corroboration of Lemma 3 on coordinates and denominators at most 12. The axis-reduction box checks the collapsed scale formulas for `u1 = 0` on primitive coordinates at most 8. Neither box is the proof. The five fixtures are witnesses of the character, not a census of solutions. One of them is the rational solution `2B+P+Q`. No step is a heuristic search offered as a nonexistence proof. + +The bilinear form is `3 x1 y1 + x2 y2`. The constants 3, 6, and 12 used for `3A+B` in the `(0,2,1,1)` argument do not appear here unchanged: the axis equation is `(α-2l) v1^2 (αβ-γ^2 - 6α k) = 2 α^2 k v2^2`, and the Cramer matrix carries 6 on the first coordinate of the new form and 2 on the second. A failure control solves one triple with the old form and checks that the sum is `diag(3,1)`, not `diag(1,3)`. + +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 `781451/250000000`, 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-a-twice --check-only +python3.12 scripts/research_package.py --package research/three-signed-a-twice +``` + +The direct check is `python3 -I -W error -B research/three-signed-a-twice/verify.py`. + +## Open next questions + +Which of the other eighteen three-frame count profiles survive the same AB/PQ test? A useful first step is to read one tuple that [discussion comment 19377345](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345) already prints, other than `(1,1,1,1)`, `(0,2,1,1)`, and `(2,0,1,1)`, write that tuple's own determinant residual, and test one rational rank-one solution with the bilinear form of that residual. This package does not name another tuple. The forms `3 x1 y1 + x2 y2` and `x1 y1 + 3 x2 y2` are special to `diag(1,3)` and `diag(3,1)`. + +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 and the released all-old-once handoff are Nick Petalas's discussion comments 19377345 and 19377832. The `(0,2,1,1)` exclusion and the question answered here are unpaidmoon PR #7013. 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-a-twice/SOURCES.json b/research/three-signed-a-twice/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/three-signed-a-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-a-twice/TASK.json b/research/three-signed-a-twice/TASK.json new file mode 100644 index 0000000000..a362a25774 --- /dev/null +++ b/research/three-signed-a-twice/TASK.json @@ -0,0 +1,71 @@ +{ + "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 the seven-call profile (a,b,p,q,r,s,t)=(2,0,1,1,1,1,1) admits no word in the PR2085/2112 model, because every rational rank-one solution of R+S+T=A+3B=diag(1,3) 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 the named three-frame census profile (2,0,1,1)/(1,1,1) left open by the (0,2,1,1) 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 (2,0,1,1)/(1,1,1). Do not search the other eighteen census profiles, do not redo (0,2,1,1) or (1,1,1,1), and do not take four-or-more frames.", + "outcome": "completed", + "evidence": "Scoped proof that every rational rank-one solution of R+S+T=A+3B has parity image avoiding (1,1), so an AB or PQ form extends and detects two calls against four targets. The scale bracket, Cramer determinant, and axis rearrangement are expanded polynomial identities for bilinear form 3*x1*y1+x2*y2. Lemma 4 is the exhaustive 32-class mod-8 check. The boxes 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 eighteen 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), (0,2,1,1)/(1,1,1), and now (2,0,1,1)/(1,1,1) are character-excluded. A surviving profile would be the next place a seven-call three-frame word could exist.", + "first_step": "Read one tuple that discussion comment 19377345 already prints, other than (1,1,1,1), (0,2,1,1), and (2,0,1,1). Write that tuple's own residual 4I-aA-bB-pP-qQ and test one rational rank-one solution with the bilinear form of that residual.", + "blocked_by": "The forms 3*x1*y1+x2*y2 and x1*y1+3*x2*y2 are special to diag(1,3) and diag(3,1). This package does not name or compute another residual." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507678", + "census": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377345", + "predecessor": "https://github.com/CrocSwap/integer-mult-bounds/pull/7013", + "upstream_checked_utc": "2026-11-10T08:36:00Z", + "priority_revision": 8 + } +} diff --git a/research/three-signed-a-twice/VERIFY.json b/research/three-signed-a-twice/VERIFY.json new file mode 100644 index 0000000000..91d5fe1407 --- /dev/null +++ b/research/three-signed-a-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, Cramer-determinant and axis-rearrangement polynomial identities for residual diag(1,3); mod-8 discriminant lemma; axis residue arithmetic; explicit characters on the named solution 2B+P+Q and four other declared frames, each detecting two calls and four targets; failure controls for a non-rank-one summand, a broken sum, a wrong-parity form, and the diag(3,1) bilinear form." + }, + { + "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-a-twice/verify.py b/research/three-signed-a-twice/verify.py new file mode 100644 index 0000000000..2017436b05 --- /dev/null +++ b/research/three-signed-a-twice/verify.py @@ -0,0 +1,501 @@ +"""Character exclusion for the seven-call profile (2,0,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 axis-reduction box, the single-line parity +lemma on a declared box, and explicit characters on declared frames. +The boxes are 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. + + B(x,y) = 3 x1 y1 + x2 y2 and q(x) = 3 x1^2 + x2^2. These belong to + the residual diag(1,3), not to diag(3,1). + """ + 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 three.mul(x1).mul(y1).add(x2.mul(y2)) + + def cross(x1, x2, y1, y2): + return x1.mul(y2).add(x2.mul(y1), scale=-1) + + def quad(x1, x2): + return three.mul(x1).mul(x1).add(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) + six = const(6, width) + three = const(3, width) + row11 = six.mul(kay).mul(u1).mul(v1).add(gee.mul(u2)) + row12 = two.mul(kay).mul(u1).mul(v2).add(gee.mul(u1), scale=-1) + row21 = six.mul(ell).mul(u1).mul(v1).add(hhh.mul(v2)) + row22 = two.mul(ell).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 = three.mul(u1).mul(u1).add(u2.mul(u2)) + quad_v = three.mul(v1).mul(v1).add(v2.mul(v2)) + closed = ( + delta.mul(gee).mul(hhh) + .add(two.mul(ell).mul(gee).mul(v1).mul(quad_u)) + .add(two.mul(kay).mul(hhh).mul(u1).mul(quad_v), 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_rearrangement(): + """The cleared axis equation is the scale condition, as polynomials. + + With D = α-2l and c_u = 3 + α v2^2 / (v1^2 D), the condition + k c_u = (αβ-γ^2)/(2α) rearranges to + (α-2l) v1^2 (αβ-γ^2 - 6α k) = 2 α^2 k v2^2. + """ + width = 7 + alpha, beta, gamma, kay, ell, vv1, vv2 = (var(i, width) for i in range(width)) + two = const(2, width) + three = const(3, width) + six = const(6, width) + gap = alpha.add(two.mul(ell), scale=-1) + v1sq = vv1.mul(vv1) + v2sq = vv2.mul(vv2) + discriminant = alpha.mul(beta).add(gamma.mul(gamma), scale=-1) + scale_condition = two.mul(alpha).mul(kay).mul( + three.mul(v1sq).mul(gap).add(alpha.mul(v2sq)) + ).add(discriminant.mul(v1sq).mul(gap), scale=-1) + displayed = gap.mul(v1sq).mul( + discriminant.add(six.mul(alpha).mul(kay), scale=-1) + ).add(two.mul(alpha).mul(alpha).mul(kay).mul(v2sq), scale=-1) + require(scale_condition.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_mod8(): + """6αk and the right-hand side are 2 or 6 mod 8 when every factor is odd.""" + odds = (1, 3, 5, 7) + for alpha in odds: + for kay in odds: + product = (6 * alpha * kay) % 8 + require(product in (2, 6), "6αk residue") + for gap in (2, 6): + difference = (gap - product) % 8 + require(difference in (0, 4), "axis difference residue") + for second in odds: + right = (2 * alpha * alpha * kay * second * second) % 8 + require(right in (2, 6), "axis right-hand residue") + for ell in range(8): + require((alpha - 2 * ell) % 2 == 1, "α-2l became even") + + +def check_quadratic_valuations(): + """Diagonal q ≡ 4 (mod 8); an axial primitive vector has odd q.""" + odds = (1, 3, 5, 7) + for first in odds: + for second in odds: + square_sum = (3 * first * first + 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 = 3 * u1 * u1 + u2 * u2 + require(value % 2 == 1, "axial quadratic parity " + str((u1, u2))) + require(value != 0, "axial quadratic vanished") + + +def valuation_gap(shift, orientation): + """Lower bounds used in Section 6 are strictly above the constant term.""" + if orientation == "axial-diagonal": + constant = 1 + shift + l_term = 2 + shift + k_term = 3 + shift + kl_term = 2 + shift + elif orientation == "diagonal-axial": + constant = 1 + shift + l_term = 3 + shift + k_term = 2 + 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 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 bilinear(left, right): + return F(3 * left[0] * right[0] + left[1] * right[1]) + + +def old_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 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 check_axis_reduction_box(): + """On a finite box, the u1=0 scale formulas match the general formula.""" + checked = 0 + for sign in (1, -1): + vertical = (0, sign) + for left in primitive_directions(8): + if left[0] == 0: + continue + for right in primitive_directions(8): + if right[0] == 0 or cross(left, right) == 0: + continue + if cross(vertical, left) == 0 or cross(vertical, right) == 0: + continue + scales = solve_scales(vertical, left, right) + reduced_u = 3 + F(left[1] * right[1], left[0] * right[0]) + reduced_v = F(right[1], cross(left, right) * left[0]) + 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 = 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) + 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(3), F(0)) +OLD_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 = ( + (2, A), + (0, 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=A+3B") + require(total != OLD_H, label + " solved the sibling residual instead") + 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 = [] + # One rational solution named by the question: 2B + P + Q = A+3B. + solutions.append(( + "rational-rank-one", + (coeffs((0, 1), 2), coeffs((1, 1), F(1, 2)), coeffs((1, -1), F(1, 2))), + )) + 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)))) + 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 B, with the third frame equal to A. + solutions.append(("parallel-negative", (coeffs((0, 1), 4), coeffs((0, 1), -1), A))) + # One added label equal to the old matrix A. + solutions.append(("old-label-duplicate", (A, B, coeffs((0, 1), 2)))) + 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") + 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") + + 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") + directions = ((1, 0), (1, 1), (2, 1)) + old_scales = solve_scales(*directions, form=old_bilinear) + old_frames = tuple(coeffs(direction, scale) + for direction, scale in zip(directions, old_scales)) + old_total = tuple(sum(frame[i] for frame in old_frames) for i in range(3)) + require(old_total == OLD_H, "old bilinear form stopped solving diag(3,1)") + require(old_total != H, "old bilinear form solved this residual") + + +def main(): + check_bracket_polynomial() + check_determinant_polynomial() + check_axis_rearrangement() + check_lemma4() + check_axis_mod8() + check_quadratic_valuations() + check_valuation_gaps() + 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-negative", + "old-label-duplicate", + ], "fixture list changed") + check_failures() + print("PASS three-signed-a-twice character checks") + + +if __name__ == "__main__": + main()