diff --git a/research/three-frame-profile-orbits/PROOF.md b/research/three-frame-profile-orbits/PROOF.md new file mode 100644 index 0000000000..f7d18f721b --- /dev/null +++ b/research/three-frame-profile-orbits/PROOF.md @@ -0,0 +1,333 @@ +# Count-profile symmetry of the three-frame character test + +Produced by Nick Petalas. Apache-2.0. + +## Claims + +All statements are in the PR2085/2112 formal register model with three added +signed rank-one frames, as used by the census in discussion comment 19377345 +and by PRs #6942, #7013, #7035 and #7051. No new κ is claimed and no word is +built. The selected record is unchanged. + +1. **Transport lemma (proof).** Eight linear symmetries of the address space + permute the old labels `A, B, P, Q` and the four targets. They carry the + complete character table of a decomposition of one count profile to the + table of its image. Character exclusion and target support are therefore + constant on orbits of count profiles. +2. **Corollary (scoped proof, conditional).** The profile `(1,1,2,0)/(1,1,1)` + admits no seven-call word. It is the image of `(2,0,1,1)/(1,1,1)`. The + corollary depends on the exclusion theorem of open PR #7035 and on the + inherited inequality of Section 1. Neither is reproved here. +3. **Survivors (finite certificate).** Twelve of the sixteen census profiles + still open have an explicit rank-one decomposition on which every additive + character detects at least as many calls as targets. For those twelve the + statement "every decomposition admits a character that detects fewer calls + than targets" is false, so the argument of #7013, #7035 and #7051 cannot + be repeated for them. Both witnesses fail target support, so they are not + candidate words. +4. **Box counts (bounded search, not a proof).** Section 6 records an + enumeration on a finite set of directions for the three open orbits. + +## 1. Setting and cited premises + +Addresses are rational symmetric 2-by-2 matrices. Write + +``` +A = diag(1,0), B = diag(0,1), +P = [[1,1],[1,1]]/2, Q = [[1,-1],[-1,1]]/2, A+B = P+Q = I. +``` + +`L0 = ZA + ZB + ZP` contains `Q` and `I`. The targets are `A+P`, `A+Q`, `B+P` +and `B+Q`. A count profile is `π = (a,b,p,q)`, the numbers of old calls with +labels `A, B, P, Q`, together with multiplicities `m = (m1,m2,m3)` of three +added labels `R, S, T`. The frames are nonzero symmetric rational rank-one +matrices of either sign. The residual of `π` is + +``` +M(π) = 4I - aA - bB - pP - qQ. +``` + +A **decomposition** of `(π, m)` is a triple of frames with +`m1 R + m2 S + m3 T = M(π)`. Its label lattice is +`Λ = L0 + ZR + ZS + ZT`. For an additive character `χ: Λ → F2`, + +``` +calls(χ) = a χ(A) + b χ(B) + p χ(P) + q χ(Q) + m1 χ(R) + m2 χ(S) + m3 χ(T), +targets(χ) = χ(A+P) + χ(A+Q) + χ(B+P) + χ(B+Q), +``` + +with the values of `χ` read as the integers 0 and 1. The **table** of the +decomposition is the multiset of pairs `(calls(χ), targets(χ))` over the +eight characters of `Λ`. `Λ` is free of rank 3, so there are exactly eight. + +The profile `(π, m)` is **character-excluded** if every decomposition has a +character with `calls(χ) < targets(χ)`. + +Three premises are cited and not reproved. They are the statements of +`research/bit-two-signed-frame-floor/PROOF.md`, Section 1 (PR #6190, which +records the PR2910 normalization). That file states them for two added +labels. PR #6942 (merged) and open PRs #7013, #7035 and #7051 use them for +three added labels, and this note uses them in the same way. + +- **(P1) Determinant.** The labels of a word with profile `(π, m)` form a + decomposition of `(π, m)`. +- **(P2) Characters.** For the labels of a word, every additive character of + `Λ` has `calls(χ) ≥ targets(χ)`. +- **(P3) Support.** For the labels of a word, each target is a sum of a + sub-multiset of the paid labels. + +By (P1) and (P2), a character-excluded profile admits no word. + +## 2. Eight symmetries + +Define three linear maps on symmetric matrices `M = [[x,y],[y,z]]`: + +``` +s(M) = D M D, D = diag(1,-1): (x, y, z) -> (x, -y, z), +t(M) = K M K, K = [[0,1],[1,0]]: (x, y, z) -> (z, y, x), +h(M) = W M W^T / 2, W = [[1,1],[1,-1]]: (x, y, z) -> ((x+2y+z)/2, (x-z)/2, (x-2y+z)/2). +``` + +**Lemma 1.** Let `G` be the group generated by `s`, `t` and `h`. Then `G` has +order 8, and every `g` in `G` + +1. is a rational linear bijection of the address space that fixes `I` and + preserves the determinant, +2. sends nonzero symmetric rational rank-one matrices to matrices of the same + kind, +3. permutes `{A, B, P, Q}` and preserves the partition `{{A,B},{P,Q}}`, +4. satisfies `g(L0) = L0` and permutes the four targets, +5. satisfies `g(M(π)) = M(gπ)`, where `gπ` is the profile with + `(gπ)(gX) = π(X)` for each old label `X`. + +**Proof.** `D` and `K` are integer matrices of determinant `±1` with +`D D^T = K K^T = I`. `W` is an integer matrix with `W W^T = 2I` and +`det W = -2`. Hence each generator is rational and linear, fixes `I`, and +multiplies the determinant by `1`: for `h`, +`det(W M W^T / 2) = (det W)^2 det M / 4 = det M`. Each generator is an +involution, since `D^2 = K^2 = I` and `W^2 = 2I`. This gives item 1 for the +generators, hence for `G`. + +A nonzero symmetric 2-by-2 matrix has rank one exactly when its determinant +is zero. Item 2 follows from item 1. + +Direct evaluation gives + +``` +s: A -> A, B -> B, P <-> Q, +t: A <-> B, P -> P, Q -> Q, +h: A <-> P, B <-> Q. +``` + +For `h`, use `h(uu^T) = (Wu)(Wu)^T / 2`: `W(1,0) = (1,1)`, `W(0,1) = (1,-1)`, +`W(1,1) = (2,0)` and `W(1,-1) = (0,2)`. The permutations `(P Q)`, `(A B)` and +`(A P)(B Q)` generate the group of the eight permutations that preserve the +partition `{{A,B},{P,Q}}`. A linear map is determined by its values on the +basis `A, B, P`, so `G` acts faithfully on the labels and has order 8. This +is item 3. + +`L0` is spanned by the four labels, so item 3 gives `g(L0) = L0`. A target is +`X + Y` with `X` in `{A,B}` and `Y` in `{P,Q}`, and `g` preserves that +partition, so `g` permutes the targets. Item 5 is linearity together with +`g(I) = I`. ∎ + +**Remark.** No other permutation of the labels helps. The four labels span a +space of dimension 3 with the single relation `A + B = P + Q`. A label +permutation extends to a linear map only if it preserves that relation, which +means that it preserves the partition. Exactly 8 of the 24 permutations do, +and they are the elements of `G`. `verify.py` enumerates all 24. + +## 3. Transport + +**Lemma 2.** Let `F = (R, S, T)` be a decomposition of `(π, m)` and let `g` +be in `G`. Then `gF = (gR, gS, gT)` is a decomposition of `(gπ, m)`, and the +two decompositions have the same table. Moreover `F` satisfies (P3) for `π` +exactly when `gF` satisfies (P3) for `gπ`. + +**Proof.** By Lemma 1, items 2 and 5, the frames `gR, gS, gT` are nonzero +symmetric rational rank-one matrices and +`m1 gR + m2 gS + m3 gT = g(M(π)) = M(gπ)`. + +Let `Λ` and `Λ'` be the label lattices of `F` and `gF`. By item 4, +`g(Λ) = g(L0) + Z gR + Z gS + Z gT = Λ'`. So `χ -> χ∘g^{-1}` is a bijection +from the characters of `Λ` to the characters of `Λ'`. Put `χ' = χ∘g^{-1}`. +Then `χ'(gX) = χ(X)` for every old label and every frame, and + +``` +calls(χ') = sum over old X of (gπ)(gX) χ'(gX) + sum of m_i χ'(g F_i) + = sum over old X of π(X) χ(X) + sum of m_i χ(F_i) = calls(χ). +``` + +The targets of `Λ'` are the images of the targets of `Λ` in some order, so +`targets(χ') = targets(χ)`. The tables agree. + +For (P3), `g` is linear and sends the multiset of paid labels of `(π, F)` to +the multiset of paid labels of `(gπ, gF)`. It sends sub-multiset sums to +sub-multiset sums and targets to targets. ∎ + +**Corollary 3.** `(π, m)` is character-excluded if and only if `(gπ, m)` is. +A decomposition of `(π, m)` on which no character has `calls < targets` +transports to such a decomposition of `(gπ, m)`. + +## 4. Orbits of the census + +The census of comment 19377345 lists 21 profiles with untested +positive-dimensional solution spaces. `G` acts on the old counts and leaves +the multiplicities alone. The orbits are: + +| Orbit | Profiles | Residual of the representative | Status | +|---|---|---|---| +| `O1` | `(1,1,1,1)/(1,1,1)` | `2I` | excluded by #6942 | +| `O2` | `(2,0,1,1)`, `(0,2,1,1)`, `(1,1,2,0)`, `(1,1,0,2)`, all `/(1,1,1)` | `diag(1,3)` | excluded: #7035, #7013, **this note**, #7051 | +| `O3` | the eight arrangements of `0,1,1,2` with the `0` and the `2` in different pairs, `/(1,1,1)` | `[[3/2,-1/2],[-1/2,5/2]]` at `(2,1,1,0)` | open; not character-excluded (Section 5) | +| `O4` | `(0,1,1,1)`, `(1,0,1,1)`, `(1,1,0,1)`, `(1,1,1,0)`, all `/(1,1,2)` | `diag(3,2)` | open; not character-excluded (Section 5) | +| `O5` | the same four old profiles, `/(1,1,1)` (six calls) | `diag(3,2)` | open | + +The pairs are `{A,B}` and `{P,Q}`. `O3` is +`(0,1,1,2), (0,1,2,1), (1,0,1,2), (1,0,2,1), (1,2,0,1), (1,2,1,0), (2,1,0,1), (2,1,1,0)`. + +**Corollary 4.** Assume the theorem of PR #7035: every decomposition of +`(2,0,1,1)/(1,1,1)` admits an additive character that detects two calls and +four targets. Then the same holds for `(1,1,2,0)/(1,1,1)`, and under (P1) and +(P2) that profile admits no seven-call word. + +**Proof.** `h` exchanges `A` with `P` and `B` with `Q`, so +`h(2,0,1,1) = (1,1,2,0)`. Indeed `h(diag(1,3)) = h(A + 3B) = P + 3Q = I + 2Q += [[2,-1],[-1,2]]`, which is `M(1,1,2,0) = 4I - A - B - 2P`. Apply +Corollary 3 with `g = h`. ∎ + +The same conclusion follows from the theorem of PR #7051 with `g = s`, +because `s(1,1,0,2) = (1,1,2,0)`. Either predecessor suffices. In the same +way the three exclusions of #7013, #7035 and #7051 are transports of one +another. + +For example, #7035 names the decomposition `2B + P + Q` of `diag(1,3)`. Its +image under `h` is `2Q + A + B`, a decomposition of `I + 2Q`. The character +with `χ(A) = χ(B) = 0` and `χ(P) = χ(Q) = 1` is even on the three frames. It +detects the two `P` calls and all four targets. + +Before this note 17 census profiles were open. After Corollary 4, 16 remain, +in the three orbits `O3`, `O4` and `O5`. One argument for one representative +of an orbit covers the whole orbit. + +## 5. Survivors in `O3` and `O4` + +**Proposition 5.** No profile of `O3` or `O4` is character-excluded. + +By Corollary 3 it is enough to give one decomposition for one representative +of each orbit. Coordinates `(a,b,c)` below mean `aA + bB + cP`. + +**`O3`, profile `(2,1,1,0)/(1,1,1)`.** The residual is +`4I - 2A - B - P = [[3/2,-1/2],[-1/2,5/2]]`. Take + +``` +R = -B = [[0,0],[0,-1]], +S = (5/2) Q = [[5/4,-5/4],[-5/4,5/4]], +T = (1/4) (1,3)(1,3)^T = [[1/4,3/4],[3/4,9/4]]. +``` + +Each frame is nonzero of rank one, and the entries add to +`(3/2, -1/2, 5/2)`. In coordinates `R = (0,-1,0)`, `S = (5/2,5/2,-5/2)` and +`T = (-1/2,3/2,3/2)`. Both `S` and `T` are congruent to `w = (1/2,1/2,1/2)` +modulo `Z^3`, so `Λ = Z^3 + Zw`, with basis `A, B, w`. A character is given +by `(α, β, ω) = (χ(A), χ(B), χ(w))`. Since `P = 2w - A - B`, + +``` +χ(P) = α+β, χ(Q) = 0, χ(R) = β, χ(S) = α+β+ω, χ(T) = ω, +calls = 2α + β + [α+β] + [β] + [α+β+ω] + [ω], +targets = 2α + 2β, +``` + +where brackets are reductions modulo 2. The eight characters give + +``` +(α,β,ω): 000 001 100 101 010 011 110 111 +(calls, targets): (0,0) (2,0) (4,2) (4,2) (4,2) (4,2) (4,4) (6,4) +``` + +Every character has `calls ≥ targets`. + +**`O4`, profile `(0,1,1,1)/(1,1,2)`.** The residual is +`4I - B - P - Q = diag(3,2)`. Take + +``` +R = (1/2) B = [[0,0],[0,1/2]], +S = (1/2) (2,1)(2,1)^T = [[2,1],[1,1/2]], +T = Q, used twice. +``` + +Then `R + S + 2T = diag(3,2)`. In coordinates `R = (0,1/2,0)`, +`S = (1,-1/2,2)` and `T = (1,1,-1)`, so `Λ = Z^3 + Z(0,1/2,0)` with basis +`A, R, P`. A character is `(α, ω, γ) = (χ(A), χ(R), χ(P))`, with `χ(B) = 0`: + +``` +χ(Q) = α+γ, χ(S) = α+ω, χ(T) = α+γ, +calls = [γ] + [α+γ] + [ω] + [α+ω] + 2[α+γ], +targets = 2[γ] + 2[α+γ]. +``` + +``` +(α,ω,γ): 000 010 100 110 001 011 101 111 +(calls, targets): (0,0) (2,0) (4,2) (4,2) (4,4) (6,4) (2,2) (2,2) +``` + +Again every character has `calls ≥ targets`. ∎ + +`verify.py` recomputes both tables from the matrices, transports the two +witnesses by all eight elements of `G`, and checks the result on each of the +twelve profiles of `O3` and `O4`. + +Neither witness is a candidate word. The first has no sub-multiset sum equal +to `A+Q` or to `B+Q`. The second has none equal to `A+P` or to `A+Q`. Both +fail (P3). The meaning of Proposition 5 is about the method: an exclusion of +`O3` or `O4` has to use target support, or another invariant, together with +the characters. + +## 6. Box counts + +This section is a bounded enumeration. It proves nothing beyond the listed +finite set. + +A box triple of `(π, m)` is a decomposition whose three frames lie on three +different lines spanned by primitive integer vectors with entries of absolute +value at most 4. There are 24 such lines. For three different lines and an +assignment of the multiplicities the scales are unique, and the triple is +kept when all three are nonzero. + +| Profile | Box triples | Character-excluded | Pass (P3) | Pass both tests | +|---|---:|---:|---:|---:| +| `(1,1,2,0)/(1,1,1)` | 1914 | 1914 | not counted | not counted | +| `(2,1,1,0)/(1,1,1)` (`O3`) | 1936 | 1854 | 8 | 0 | +| `(0,1,1,1)/(1,1,2)` (`O4`) | 5610 | 5225 | 41 | 0 | +| `(0,1,1,1)/(1,1,1)` (`O5`) | 1870 | 1870 | 11 | 0 | + +The first row agrees with Corollary 4 on the box. In the `O5` row every box +triple is character-excluded, so `O5` may be character-excluded. In the `O3` +and `O4` rows no box triple passes both the character test and (P3). + +A second finite check supports Lemma 2. For every census profile, every +element of `G` and every box triple at bound 2, the transported triple is a +decomposition of the transported profile with the same table. That is +11,264 comparisons. + +## 7. What this does not prove + +- It does not reprove the exclusions of #6942, #7013, #7035 or #7051, or the + premises (P1) to (P3). Corollary 4 is conditional on them. +- It does not settle `O3`, `O4` or `O5`. Sixteen census profiles stay open. +- Proposition 5 does not produce a word. Both witnesses fail (P3). +- The box counts are a search on 24 lines. They are not a classification of + all rational decompositions. +- Decompositions with two parallel frames are outside the box. +- Four or more added frames are not treated. + +## 8. Credit + +The register model is Cinna Davis's PR2085/2112 formal model. The +determinant, support and character premises are the PR2910 package as +recorded by apoursh in PR #6190. The census is discussion comment 19377345. +The exclusions of `(1,1,1,1)`, `(0,2,1,1)`, `(2,0,1,1)` and `(1,1,0,2)` are +unpaidmoon's PRs #6942, #7013, #7035 and #7051, and the question answered +here is the open question of #7051. The symmetry lemma, the transported +exclusion, the two surviving witnesses and the checker are produced by Nick +Petalas. diff --git a/research/three-frame-profile-orbits/README.md b/research/three-frame-profile-orbits/README.md new file mode 100644 index 0000000000..e11bbe2f60 --- /dev/null +++ b/research/three-frame-profile-orbits/README.md @@ -0,0 +1,126 @@ +# Count-profile symmetry of the three-frame character test + +**No new κ and no word.** The selected record is unchanged. + +In the PR2085/2112 register model with three added signed rank-one frames, +eight linear symmetries of the address space permute the old labels +`A, B, P, Q` and the four targets. They carry the whole character table of a +decomposition of one old-count profile to its image. This gives three +results about the census of discussion comment 19377345. + +1. **`(1,1,2,0)/(1,1,1)` admits no seven-call word.** It is the image of + `(2,0,1,1)/(1,1,1)` under the map that exchanges `A` with `P` and `B` with + `Q`. This is a scoped proof, conditional on the exclusion theorem of open + PR #7035 (or of open PR #7051) and on the inherited first-order + inequality. PR #7051 names this profile as not settled. +2. **The sixteen profiles still open are three orbits**, of sizes 8, 4 and 4. + One argument per orbit is enough. +3. **Twelve of those sixteen are not character-excluded.** For the 8-orbit + and for the `(1,1,2)` 4-orbit an explicit rank-one decomposition passes + every additive character. The argument of #7013, #7035 and #7051 cannot + be repeated there. Both witnesses fail target support, so an exclusion of + those orbits has to combine characters with target support or another + invariant. + +The statements, proofs and limits are in [PROOF.md](PROOF.md). + +| Orbit | Profiles | Status | +|---|---|---| +| `O1` | `(1,1,1,1)/(1,1,1)` | excluded by #6942 | +| `O2` | `(2,0,1,1)`, `(0,2,1,1)`, `(1,1,2,0)`, `(1,1,0,2)`, all `/(1,1,1)` | excluded; `(1,1,2,0)` is new here | +| `O3` | eight profiles such as `(2,1,1,0)/(1,1,1)` | open; a character-surviving decomposition exists | +| `O4` | `(0,1,1,1)` and its three images, `/(1,1,2)` | open; a character-surviving decomposition exists | +| `O5` | the same four old profiles, `/(1,1,1)` | open; every box triple is character-excluded | + +The surviving decomposition for `(2,1,1,0)/(1,1,1)` is +`-B + (5/2)Q + (1/4)(1,3)(1,3)^T`. For `(0,1,1,1)/(1,1,2)` it is +`(1/2)B + (1/2)(2,1)(2,1)^T + 2Q`. + +## Scope and evidence + +Original card: `bit-new-register-model`, with `scope_status: changed`. The +card asks for a larger or nonabelian native alphabet. This package stays in +the abelian symmetric 2-by-2 model and answers the open question of PR #7051 +about the remaining three-frame count profiles. See [TASK.json](TASK.json). + +Four kinds of evidence are kept apart. + +- **Proof:** the symmetry lemma and the transport lemma (PROOF.md, Sections 2 + and 3). +- **Scoped proof, conditional:** the exclusion of `(1,1,2,0)/(1,1,1)`. It + uses the theorem of #7035 or #7051 and the premises of PR #6190, Section 1. + None of them is reproved or replayed here. #7035 and #7051 are open and + unreviewed. +- **Finite certificate:** the two surviving decompositions, with their full + tables of eight characters, transported to all twelve profiles of `O3` and + `O4`. +- **Bounded search:** the box counts of PROOF.md, Section 6. They cover + frames on 24 lines and are not a classification. + +`verify.py` checks the eight maps exactly, enumerates all 24 label +permutations, checks residual equivariance on all 35 four-call profiles, +computes the census orbits, recomputes both survivor tables on twelve +profiles, runs 11,264 transport comparisons, and reproduces the box counts. +It has six failure controls. + +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record, the catalogue and the two predecessor proofs on `main` +are historical provenance. PRs #7013, #7035 and #7051 are open and are cited +by number and head commit; their bytes are not vendored: + +- #7013 `research/three-signed-b-twice`, head `ed127d7ab6067daf8a48def1445da5864ad113df` +- #7035 `research/three-signed-a-twice`, head `e0026d8fd0d8c3eef46391e3e3e540c15279eec5` +- #7051 `research/three-signed-q-twice`, head `7af3a03dade6bd166ad08d7afc6879b0726fe100` + +Full Git history is needed to resolve the provenance pins. + +## Reproduce + +CPython 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/three-frame-profile-orbits +python3.12 -I -W error -B research/three-frame-profile-orbits/verify.py +python3.12 -I -O -W error -B research/three-frame-profile-orbits/verify.py +``` + +The last line of the verifier output is + +```text +PASS_THREE_FRAME_PROFILE_ORBITS group=8 compositions=35 census_orbits=5 open_profiles=16 open_orbits=3 four_call_orbits=8 new_profile_box=1914 transport_checks=11264 survivor_profiles=12 controls=6 +``` + +Each run takes about four seconds. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +1. Is the six-call orbit `O5`, represented by `(0,1,1,1)/(1,1,1)` with + `R+S+T = diag(3,2)`, character-excluded? All 1870 box triples are. A proof + would close four profiles at once. First step: run the parity-image + argument of #7035 with the form `3 x1^2 + 2 x2^2` in place of + `3 x1^2 + x2^2`. Blocker: the constants of #7035 belong to `diag(1,3)`, + of determinant 3. `diag(3,2)` has determinant 6, so the 2-adic case split + has to be redone. It was not attempted here. +2. Does every decomposition of `(2,1,1,0)/(1,1,1)` fail a character or + target support? In the box none of 1936 triples passes both. First step: + describe the decompositions that pass every character, starting from the + lattice `Z^3 + Z(1/2,1/2,1/2)` of the witness, and test the subset sums + for `A+Q` on that family. Blocker: the character-surviving set is not yet + parametrized. +3. The same question for `(0,1,1,1)/(1,1,2)`, where 385 box triples survive + the characters and none of them passes target support. + +## Credit + +The register model is Cinna Davis's PR2085/2112 formal model. The +determinant, support and character premises are the PR2910 package as +recorded by apoursh in PR #6190. The census is discussion comment 19377345. +The exclusions of `(1,1,1,1)`, `(0,2,1,1)`, `(2,0,1,1)` and `(1,1,0,2)` are +unpaidmoon's PRs #6942, #7013, #7035 and #7051; the question answered here +is the open question of #7051. + +The symmetry lemma, the transported exclusion, the two surviving witnesses +and the checker are produced by Nick Petalas. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/three-frame-profile-orbits/SOURCES.json b/research/three-frame-profile-orbits/SOURCES.json new file mode 100644 index 0000000000..af832d2b85 --- /dev/null +++ b/research/three-frame-profile-orbits/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-two-signed-frame-floor/PROOF.md", + "usage": "provenance", + "git_blob": "3797e6b8dc196bf5e6d9b5bf5a43c255b435f0bb", + "sha256": "6964115728b748cdb4d52f6e5a626dd3840bb01f254f4c1ce26bc475a25a2420" + }, + { + "path": "research/three-signed-old-once/PROOF.md", + "usage": "provenance", + "git_blob": "d852f1e1e177abb8980c6e2bc466cb7926ffce10", + "sha256": "558efb53c52fd4cc9cb3d284f01b484aaba417cb996f3ecc58604d21b28f63ac" + } + ] +} diff --git a/research/three-frame-profile-orbits/TASK.json b/research/three-frame-profile-orbits/TASK.json new file mode 100644 index 0000000000..236d432eed --- /dev/null +++ b/research/three-frame-profile-orbits/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "In the abelian symmetric 2-by-2 register model with three added signed rank-one frames, prove that the eight linear symmetries permuting A, B, P, Q transport the full character table between old-count profiles; derive the exclusion of (1,1,2,0)/(1,1,1) from the cited exclusion of (2,0,1,1)/(1,1,1); reduce the sixteen census profiles still open to three orbits; and exhibit, for twelve of them, a rank-one decomposition that passes every additive character.", + "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 open question of open PR #7051 about the remaining three-frame count profiles of the census in discussion comment 19377345.", + "bottleneck_link": "Side result on the signed-frame escape from the eight-call minimum. One more seven-call profile is excluded and no word is found, so there is no call-count saving and no selected-frontier change. The orbit reduction and the character-surviving witnesses change which argument the remaining profiles need.", + "budget_minutes": 60, + "stop_rule": "Stop after the transport lemma, the orbit table, the transported exclusion and one character-surviving witness per orbit where one exists. Do not attempt the remaining three orbits.", + "outcome": "partial", + "evidence": "PROOF.md proves the symmetry and transport lemmas. The exclusion of (1,1,2,0)/(1,1,1) is conditional on the theorem of open PR #7035 or #7051 and on the premises of PR #6190 Section 1, none replayed. verify.py checks the eight maps exactly, all 24 label permutations, residual equivariance on 35 profiles, the census orbits, both survivor tables on twelve profiles, 11264 transport comparisons, bounded box counts and six failure controls. It prints PASS_THREE_FRAME_PROFILE_ORBITS. CPython 3.12, standard library only.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the six-call orbit of (0,1,1,1)/(1,1,1), with R+S+T = diag(3,2), character-excluded?", + "why_it_matters": "One proof would close four census profiles. All 1870 box triples on 24 lines are character-excluded.", + "first_step": "Run the parity-image argument of PR #7035 with the form 3 x1^2 + 2 x2^2 in place of 3 x1^2 + x2^2.", + "blocked_by": "The constants of PR #7035 belong to diag(1,3), of determinant 3; diag(3,2) has determinant 6, so the 2-adic case split has to be redone. It was not attempted here." + }, + { + "question": "Does every rank-one decomposition of (2,1,1,0)/(1,1,1) fail a character or target support?", + "why_it_matters": "A yes answer closes the eight-profile orbit. The witness -B + (5/2)Q + (1/4)(1,3)(1,3)^T shows that characters alone cannot.", + "first_step": "Describe the decompositions that pass every character, starting from the lattice Z^3 + Z(1/2,1/2,1/2) of the witness, and test the subset sums for A+Q on that family.", + "blocked_by": "The character-surviving set is not parametrized; the box shows 82 of 1936 triples and none passes target support." + }, + { + "question": "Does every rank-one decomposition of (0,1,1,1)/(1,1,2) fail a character or target support?", + "why_it_matters": "A yes answer closes the four-profile orbit with one doubled frame. The witness (1/2)B + (1/2)(2,1)(2,1)^T + 2Q passes every character.", + "first_step": "Classify the index-two lattices that give a character-surviving table for R+S+2T = diag(3,2), then test the subset sums for A+P and A+Q.", + "blocked_by": "The doubled frame changes the call count of each character, so the three-frame argument of the predecessors does not apply as written." + } + ] +} diff --git a/research/three-frame-profile-orbits/VERIFY.json b/research/three-frame-profile-orbits/VERIFY.json new file mode 100644 index 0000000000..3c4d2df057 --- /dev/null +++ b/research/three-frame-profile-orbits/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": "Exact symmetry facts for the eight maps; all 24 label permutations; residual equivariance on 35 profiles; census orbits; transported named witness; both character-surviving witnesses on twelve profiles; 11264 transport comparisons; bounded box counts; six failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks under python -O; every check raises SystemExit." + } + ] +} diff --git a/research/three-frame-profile-orbits/verify.py b/research/three-frame-profile-orbits/verify.py new file mode 100644 index 0000000000..cced91f120 --- /dev/null +++ b/research/three-frame-profile-orbits/verify.py @@ -0,0 +1,565 @@ +#!/usr/bin/env python3 +"""Exact checks for the count-profile symmetry of the three-frame character test. + +Addresses are rational symmetric 2-by-2 matrices, stored as (x, y, z) for +[[x, y], [y, z]]. Every check raises SystemExit, so python -O keeps them. +Standard library only. +""" + +from __future__ import annotations + +from fractions import Fraction as Fr +from itertools import combinations, permutations, product +from math import gcd + +Sym = tuple[Fr, Fr, Fr] +Profile = tuple[int, int, int, int] +LinearMap = tuple[Sym, Sym, Sym] # images of the unit vectors of (x, y, z) + +A: Sym = (Fr(1), Fr(0), Fr(0)) +B: Sym = (Fr(0), Fr(0), Fr(1)) +P: Sym = (Fr(1, 2), Fr(1, 2), Fr(1, 2)) +Q: Sym = (Fr(1, 2), Fr(-1, 2), Fr(1, 2)) +IDENTITY: Sym = (Fr(1), Fr(0), Fr(1)) +LABELS: tuple[Sym, Sym, Sym, Sym] = (A, B, P, Q) + +CENSUS_FOUR_OLD: tuple[Profile, ...] = ( + (0, 1, 1, 2), (0, 1, 2, 1), (0, 2, 1, 1), (1, 0, 1, 2), + (1, 0, 2, 1), (1, 1, 0, 2), (1, 1, 2, 0), (1, 2, 0, 1), + (1, 2, 1, 0), (2, 0, 1, 1), (2, 1, 0, 1), (2, 1, 1, 0), +) +CENSUS_THREE_OLD: tuple[Profile, ...] = ( + (0, 1, 1, 1), (1, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0), +) +ONCE = (1, 1, 1) +TWICE = (1, 1, 2) +# Settled before this package: #6942, #7013, #7035, #7051 (all multiplicity (1,1,1)). +SETTLED_BEFORE: frozenset[Profile] = frozenset( + {(1, 1, 1, 1), (0, 2, 1, 1), (2, 0, 1, 1), (1, 1, 0, 2)} +) +NEW_PROFILE: Profile = (1, 1, 2, 0) +BOX = 4 +SMALL_BOX = 2 +EUCLID_CAP = 4096 + +# Finite box observations for the three orbits left open, as +# (triples, character-excluded, target-support passes, passes of both tests). +# They are counts of a bounded enumeration, not proofs; see PROOF.md section 6. +EXPECTED_OPEN_BOX: dict[str, tuple[int, int, int, int]] = { + "(2,1,1,0)/(1,1,1)": (1936, 1854, 8, 0), + "(0,1,1,1)/(1,1,2)": (5610, 5225, 41, 0), + "(0,1,1,1)/(1,1,1)": (1870, 1870, 11, 0), +} +# Character tables of the two surviving witnesses of PROOF.md section 5. +SURVIVOR_TABLES: dict[str, list[tuple[int, int]]] = { + "adjacent": [(0, 0), (2, 0), (4, 2), (4, 2), (4, 2), (4, 2), (4, 4), (6, 4)], + "three-old-twice": [(0, 0), (2, 0), (2, 2), (2, 2), (4, 2), (4, 2), (4, 4), (6, 4)], +} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise SystemExit(f"FAIL: {message}") + + +def add(u: Sym, v: Sym) -> Sym: + return (u[0] + v[0], u[1] + v[1], u[2] + v[2]) + + +def scale(c: Fr | int, u: Sym) -> Sym: + return (c * u[0], c * u[1], c * u[2]) + + +def det(u: Sym) -> Fr: + return u[0] * u[2] - u[1] * u[1] + + +def apply(g: LinearMap, u: Sym) -> Sym: + out = (Fr(0), Fr(0), Fr(0)) + for coefficient, column in zip(u, g): + out = add(out, scale(coefficient, column)) + return out + + +def compose(g: LinearMap, f: LinearMap) -> LinearMap: + return (apply(g, f[0]), apply(g, f[1]), apply(g, f[2])) + + +def from_formula(formula) -> LinearMap: + units = ((Fr(1), Fr(0), Fr(0)), (Fr(0), Fr(1), Fr(0)), (Fr(0), Fr(0), Fr(1))) + return (formula(*units[0]), formula(*units[1]), formula(*units[2])) + + +# The three generators. h is M -> W M W^T / 2 with the integer W = [[1,1],[1,-1]]. +FLIP = from_formula(lambda x, y, z: (x, -y, z)) +SWAP = from_formula(lambda x, y, z: (z, y, x)) +HADAMARD = from_formula( + lambda x, y, z: ((x + 2 * y + z) / 2, (x - z) / 2, (x - 2 * y + z) / 2) +) + + +def generate_group() -> list[LinearMap]: + identity = from_formula(lambda x, y, z: (x, y, z)) + group = [identity] + for _ in range(8): + grown = list(group) + for g, f in product(group, (FLIP, SWAP, HADAMARD)): + candidate = compose(f, g) + if candidate not in grown: + grown.append(candidate) + if len(grown) == len(group): + return group + group = grown + raise SystemExit("FAIL: group closure did not stabilise") + + +def label_permutation(g: LinearMap) -> tuple[int, int, int, int] | None: + images = [] + for label in LABELS: + image = apply(g, label) + if image not in LABELS: + return None + images.append(LABELS.index(image)) + if sorted(images) != [0, 1, 2, 3]: + return None + return (images[0], images[1], images[2], images[3]) + + +def abc_coordinates(u: Sym) -> Sym: + """Coefficients of u on the basis (A, B, P).""" + return (u[0] - u[1], u[2] - u[1], 2 * u[1]) + + +def preserves_determinant(g: LinearMap) -> bool: + # Both sides have degree at most 2 in each variable, so a 3x3x3 grid decides. + grid = [Fr(k) for k in range(3)] + return all(det(apply(g, u)) == det(u) for u in product(grid, repeat=3)) + + +def targets() -> list[Sym]: + return [add(A, P), add(A, Q), add(B, P), add(B, Q)] + + +def check_symmetry(g: LinearMap) -> tuple[int, int, int, int]: + """Lemma 1 for one map; returns its label permutation.""" + require(apply(g, IDENTITY) == IDENTITY, "identity matrix is not fixed") + require(preserves_determinant(g), "determinant is not preserved") + perm = label_permutation(g) + require(perm is not None, "labels are not permuted") + assert perm is not None + rows = [abc_coordinates(apply(g, label)) for label in (A, B, P)] + require(all(c.denominator == 1 for row in rows for c in row), "lattice not integral") + d = ( + rows[0][0] * (rows[1][1] * rows[2][2] - rows[1][2] * rows[2][1]) + - rows[0][1] * (rows[1][0] * rows[2][2] - rows[1][2] * rows[2][0]) + + rows[0][2] * (rows[1][0] * rows[2][1] - rows[1][1] * rows[2][0]) + ) + require(d in (1, -1), "lattice map is not unimodular") + moved = [apply(g, target) for target in targets()] + require(sorted(moved) == sorted(targets()), "targets are not permuted") + return perm + + +def move_profile(perm: tuple[int, int, int, int], profile: Profile) -> Profile: + moved = [0, 0, 0, 0] + for index, count in enumerate(profile): + moved[perm[index]] = count + return (moved[0], moved[1], moved[2], moved[3]) + + +def residual(profile: Profile) -> Sym: + out = scale(4, IDENTITY) + for count, label in zip(profile, LABELS): + out = add(out, scale(-count, label)) + return out + + +def linear_label_permutations() -> list[tuple[int, int, int, int]]: + """Label permutations that extend to a linear map of the address space.""" + extending = [] + for perm in permutations(range(4)): + # A, B, P is a basis and Q = A + B - P, so linearity is one equation. + image_q = add(add(LABELS[perm[0]], LABELS[perm[1]]), scale(-1, LABELS[perm[2]])) + if image_q == LABELS[perm[3]]: + extending.append(perm) + return extending + + +def lattice_basis(vectors: list[tuple[int, int, int]]) -> list[tuple[int, int, int]]: + """Echelon basis of the rank-3 integer row lattice spanned by vectors.""" + rows = [list(v) for v in vectors] + basis: list[tuple[int, int, int]] = [] + for column in range(3): + for _ in range(EUCLID_CAP): + live = sorted((r for r in rows if r[column] != 0), key=lambda r: abs(r[column])) + if len(live) <= 1: + break + pivot = live[0] + for row in live[1:]: + factor = row[column] // pivot[column] + for k in range(3): + row[k] -= factor * pivot[k] + else: + raise SystemExit("FAIL: Euclid cap reached") + live = [r for r in rows if r[column] != 0] + require(len(live) == 1, "lattice does not have rank 3") + basis.append((live[0][0], live[0][1], live[0][2])) + rows = [r for r in rows if r is not live[0]] + require(all(not any(r) for r in rows), "lattice reduction left a remainder") + return basis + + +def basis_parities(basis: list[tuple[int, int, int]], vector: tuple[int, int, int]) -> tuple[int, int, int]: + """Coordinates of vector on the echelon basis, reduced modulo 2.""" + rest = list(vector) + coords = [] + for index, row in enumerate(basis): + quotient, remainder = divmod(rest[index], row[index]) + require(remainder == 0, "vector is outside the lattice") + for k in range(3): + rest[k] -= quotient * row[k] + coords.append(quotient % 2) + require(not any(rest), "vector is outside the lattice") + return (coords[0], coords[1], coords[2]) + + +def character_table(profile: Profile, multiplicity: tuple[int, ...], frames: tuple[Sym, ...]) -> list[tuple[int, int]]: + """(calls detected, targets detected) for all 8 characters of the label lattice.""" + require(len(multiplicity) == len(frames), "multiplicity does not match frames") + frame_coords = [abc_coordinates(f) for f in frames] + denominator = 1 + for coords in frame_coords: + for c in coords: + denominator = denominator * c.denominator // gcd(denominator, c.denominator) + + def integral(u: Sym) -> tuple[int, int, int]: + scaled = [c * denominator for c in abc_coordinates(u)] + return (int(scaled[0]), int(scaled[1]), int(scaled[2])) + + generators = [integral(label) for label in (A, B, P)] + [integral(f) for f in frames] + basis = lattice_basis(generators) + call_bits = [(count, basis_parities(basis, integral(label))) for count, label in zip(profile, LABELS)] + call_bits += [(m, basis_parities(basis, integral(f))) for m, f in zip(multiplicity, frames)] + target_bits = [basis_parities(basis, integral(t)) for t in targets()] + table = [] + for chi in product((0, 1), repeat=3): + def value(bits: tuple[int, int, int]) -> int: + return (chi[0] * bits[0] + chi[1] * bits[1] + chi[2] * bits[2]) % 2 + calls = sum(count * value(bits) for count, bits in call_bits) + hit = sum(value(bits) for bits in target_bits) + table.append((calls, hit)) + return sorted(table) + + +def excluded(table: list[tuple[int, int]]) -> bool: + return any(calls < hit for calls, hit in table) + + +def support_ok(profile: Profile, multiplicity: tuple[int, ...], frames: tuple[Sym, ...]) -> bool: + """Every target is a subset sum of the paid labels, each occurrence used once.""" + calls: list[Sym] = [] + for count, label in zip(profile, LABELS): + calls += [label] * count + for m, frame in zip(multiplicity, frames): + calls += [frame] * m + require(len(calls) <= 8, "support check is sized for at most eight calls") + sums = {(Fr(0), Fr(0), Fr(0))} + for call in calls: + sums |= {add(partial, call) for partial in sums} + return all(target in sums for target in targets()) + + +def directions(bound: int) -> list[tuple[int, int]]: + """Primitive integer directions in the box, one per line.""" + found = [] + for u1, u2 in product(range(-bound, bound + 1), repeat=2): + if gcd(u1, u2) != 1: + continue + if u1 < 0 or (u1 == 0 and u2 < 0): + continue + found.append((u1, u2)) + return found + + +def outer(u: tuple[int, int]) -> Sym: + return (Fr(u[0] * u[0]), Fr(u[0] * u[1]), Fr(u[1] * u[1])) + + +def solve_scales(columns: tuple[Sym, Sym, Sym], rhs: Sym) -> tuple[Fr, Fr, Fr] | None: + """Cramer solution of c0*col0 + c1*col1 + c2*col2 = rhs, or None if singular.""" + def det3(c0: Sym, c1: Sym, c2: Sym) -> Fr: + return ( + c0[0] * (c1[1] * c2[2] - c1[2] * c2[1]) + - c1[0] * (c0[1] * c2[2] - c0[2] * c2[1]) + + c2[0] * (c0[1] * c1[2] - c0[2] * c1[1]) + ) + d = det3(*columns) + if d == 0: + return None + return ( + det3(rhs, columns[1], columns[2]) / d, + det3(columns[0], rhs, columns[2]) / d, + det3(columns[0], columns[1], rhs) / d, + ) + + +def box_decompositions(target: Sym, multiplicity: tuple[int, int, int], bound: int) -> list[tuple[Sym, Sym, Sym]]: + """Three nonzero rank-one frames on distinct box lines with m.R = target.""" + found = [] + slots = sorted(set(permutations(multiplicity))) + for triple in combinations(directions(bound), 3): + outers = (outer(triple[0]), outer(triple[1]), outer(triple[2])) + for slot in slots: + columns = (scale(slot[0], outers[0]), scale(slot[1], outers[1]), scale(slot[2], outers[2])) + scales = solve_scales(columns, target) + if scales is None or 0 in scales: + continue + frames = [(m, scale(c, o)) for m, c, o in zip(slot, scales, outers)] + frames.sort(key=lambda item: item[0]) + require(tuple(m for m, _ in frames) == multiplicity, "slot order") + found.append((frames[0][1], frames[1][1], frames[2][1])) + return found + + +def check_decomposition(target: Sym, multiplicity: tuple[int, ...], frames: tuple[Sym, ...]) -> None: + total = (Fr(0), Fr(0), Fr(0)) + for m, frame in zip(multiplicity, frames): + require(frame != (0, 0, 0) and det(frame) == 0, "frame is not nonzero rank one") + total = add(total, scale(m, frame)) + require(total == target, "frames do not sum to the residual") + + +def check_group() -> dict[tuple[int, int, int, int], LinearMap]: + group = generate_group() + require(len(group) == 8, "group order is not 8") + by_perm = {} + for g in group: + by_perm[check_symmetry(g)] = g + require(len(by_perm) == 8, "label action is not faithful") + require(sorted(by_perm) == sorted(linear_label_permutations()), "not every linear label permutation") + require(len(linear_label_permutations()) == 8, "linear label permutations are not 8 of 24") + require(label_permutation(FLIP) == (0, 1, 3, 2), "flip is not (P Q)") + require(label_permutation(SWAP) == (1, 0, 2, 3), "swap is not (A B)") + require(label_permutation(HADAMARD) == (2, 3, 0, 1), "Hadamard is not (A P)(B Q)") + for u in product([Fr(k, 2) for k in range(-2, 3)], repeat=3): + require(apply(HADAMARD, apply(HADAMARD, u)) == u, "Hadamard is not an involution") + for u1, u2 in product(range(-3, 4), repeat=2): + image = scale(Fr(1, 2), outer((u1 + u2, u1 - u2))) + require(apply(HADAMARD, outer((u1, u2))) == image, "Hadamard rank-one formula") + return by_perm + + +def check_residuals(by_perm: dict[tuple[int, int, int, int], LinearMap]) -> int: + compositions = [p for p in product(range(5), repeat=4) if sum(p) == 4] + require(len(compositions) == 35, "composition count") + for perm, g in by_perm.items(): + for profile in compositions + list(CENSUS_THREE_OLD): + require(apply(g, residual(profile)) == residual(move_profile(perm, profile)), "residual equivariance") + return len(compositions) + + +def orbits(profiles: list[tuple[Profile, tuple[int, ...]]], perms: list[tuple[int, int, int, int]]) -> list[list[tuple[Profile, tuple[int, ...]]]]: + remaining = list(profiles) + found = [] + for _ in range(len(profiles)): + if not remaining: + break + seed_profile, seed_mult = remaining[0] + orbit = sorted({(move_profile(perm, seed_profile), seed_mult) for perm in perms}) + require(all(item in remaining for item in orbit), "census is not closed under the group") + remaining = [item for item in remaining if item not in orbit] + found.append(orbit) + require(not remaining, "orbit enumeration incomplete") + return found + + +def check_orbits(by_perm: dict[tuple[int, int, int, int], LinearMap]) -> dict[str, int]: + census = [((1, 1, 1, 1), ONCE)] + census += [(p, ONCE) for p in CENSUS_FOUR_OLD] + census += [(p, TWICE) for p in CENSUS_THREE_OLD] + census += [(p, ONCE) for p in CENSUS_THREE_OLD] + require(len(census) == 21 and len(set(census)) == 21, "census size") + perms = list(by_perm) + classes = orbits(census, perms) + require(sorted(len(c) for c in classes) == [1, 4, 4, 4, 8], "census orbit sizes") + settled = {(p, ONCE) for p in SETTLED_BEFORE} + require(len(census) - len(settled) == 17, "open count before transport") + new_orbit = next(c for c in classes if (NEW_PROFILE, ONCE) in c) + require( + new_orbit == sorted([((0, 2, 1, 1), ONCE), ((1, 1, 0, 2), ONCE), ((1, 1, 2, 0), ONCE), ((2, 0, 1, 1), ONCE)]), + "orbit of the new profile", + ) + require(move_profile(label_permutation(HADAMARD), (2, 0, 1, 1)) == NEW_PROFILE, "Hadamard image of (2,0,1,1)") + require(move_profile(label_permutation(FLIP), (1, 1, 0, 2)) == NEW_PROFILE, "flip image of (1,1,0,2)") + transported = {item for c in classes if settled & set(c) for item in c} + require(transported - settled == {(NEW_PROFILE, ONCE)}, "transport settles exactly one new profile") + open_classes = [c for c in classes if not (settled & set(c))] + require(sorted(len(c) for c in open_classes) == [4, 4, 8], "open orbit sizes") + require(sum(len(c) for c in open_classes) == 16, "open count after transport") + all_profiles = [(p, ONCE) for p in product(range(5), repeat=4) if sum(p) == 4] + return { + "census_orbits": len(classes), + "open_orbits": len(open_classes), + "open_profiles": sum(len(c) for c in open_classes), + "all_four_call_orbits": len(orbits(all_profiles, perms)), + } + + +def check_named_witness() -> None: + """#7035's named solution 2B+P+Q and its Hadamard image A+B+2Q.""" + source = (scale(2, B), P, Q) + check_decomposition(residual((2, 0, 1, 1)), ONCE, source) + image = tuple(apply(HADAMARD, f) for f in source) + require(image == (scale(2, Q), A, B), "image of the named solution") + require(residual(NEW_PROFILE) == add(IDENTITY, scale(2, Q)), "residual of (1,1,2,0) is I+2Q") + require(residual(NEW_PROFILE) == (Fr(2), Fr(-1), Fr(2)), "residual matrix [[2,-1],[-1,2]]") + check_decomposition(residual(NEW_PROFILE), ONCE, image) + source_table = character_table((2, 0, 1, 1), ONCE, source) + image_table = character_table(NEW_PROFILE, ONCE, image) + require(source_table == image_table, "named witness tables differ") + require((2, 4) in image_table and excluded(image_table), "named witness is not excluded by 2 < 4") + + +def check_new_profile_box() -> int: + """Direct finite corroboration on the new profile: every box triple is excluded.""" + found = box_decompositions(residual(NEW_PROFILE), ONCE, BOX) + require(len(found) > 0, "empty box for the new profile") + for frames in found: + check_decomposition(residual(NEW_PROFILE), ONCE, frames) + require(excluded(character_table(NEW_PROFILE, ONCE, frames)), "box triple of (1,1,2,0) is not excluded") + return len(found) + + +def check_transport_box(by_perm: dict[tuple[int, int, int, int], LinearMap]) -> int: + """Lemma 2 on a box: tables agree for every census profile and group element.""" + checked = 0 + census = [((1, 1, 1, 1), ONCE)] + census += [(p, ONCE) for p in CENSUS_FOUR_OLD] + census += [(p, TWICE) for p in CENSUS_THREE_OLD] + census += [(p, ONCE) for p in CENSUS_THREE_OLD] + for profile, multiplicity in census: + found = box_decompositions(residual(profile), multiplicity, SMALL_BOX) + tables = [character_table(profile, multiplicity, frames) for frames in found] + for perm, g in by_perm.items(): + moved_profile = move_profile(perm, profile) + for frames, table in zip(found, tables): + moved = tuple(apply(g, f) for f in frames) + check_decomposition(residual(moved_profile), multiplicity, moved) + require(character_table(moved_profile, multiplicity, moved) == table, "transported table differs") + checked += 1 + return checked + + +def check_survivors(by_perm: dict[tuple[int, int, int, int], LinearMap]) -> int: + """Section 5: explicit triples that pass every character, on twelve profiles.""" + witnesses = ( + ("adjacent", (2, 1, 1, 0), ONCE, (scale(-1, B), scale(Fr(5, 2), Q), scale(Fr(1, 4), outer((1, 3))))), + ("three-old-twice", (0, 1, 1, 1), TWICE, (scale(Fr(1, 2), B), scale(Fr(1, 2), outer((2, 1))), Q)), + ) + reached = set() + for name, profile, multiplicity, frames in witnesses: + for perm, g in by_perm.items(): + moved_profile = move_profile(perm, profile) + moved = tuple(apply(g, f) for f in frames) + check_decomposition(residual(moved_profile), multiplicity, moved) + table = character_table(moved_profile, multiplicity, moved) + require(table == SURVIVOR_TABLES[name], f"survivor table changed for {name}") + require(all(calls >= hit for calls, hit in table), "survivor is excluded by a character") + require(not excluded(table), "survivor is excluded") + require(not support_ok(moved_profile, multiplicity, moved), "survivor passes target support") + reached.add((moved_profile, multiplicity)) + closed = SETTLED_BEFORE | {NEW_PROFILE} + expected = {(p, ONCE) for p in CENSUS_FOUR_OLD if p not in closed} + expected |= {(p, TWICE) for p in CENSUS_THREE_OLD} + require(reached == expected and len(reached) == 12, "survivors do not cover the twelve profiles") + return len(reached) + + +def open_orbit_box() -> dict[str, tuple[int, int, int, int]]: + """Bounded observation on each open orbit: excluded, support and joint counts.""" + representatives = { + "(2,1,1,0)/(1,1,1)": ((2, 1, 1, 0), ONCE), + "(0,1,1,1)/(1,1,2)": ((0, 1, 1, 1), TWICE), + "(0,1,1,1)/(1,1,1)": ((0, 1, 1, 1), ONCE), + } + observed = {} + for name, (profile, multiplicity) in representatives.items(): + found = box_decompositions(residual(profile), multiplicity, BOX) + hit = 0 + supported = 0 + both = 0 + for frames in found: + is_excluded = excluded(character_table(profile, multiplicity, frames)) + is_supported = support_ok(profile, multiplicity, frames) + hit += is_excluded + supported += is_supported + both += (not is_excluded) and is_supported + observed[name] = (len(found), hit, supported, both) + return observed + + +def check_controls(by_perm: dict[tuple[int, int, int, int], LinearMap]) -> int: + controls = 0 + # A label permutation outside the eight does not extend linearly. + require((2, 1, 0, 3) not in by_perm, "transposition (A P) wrongly accepted") + controls += 1 + # A rescaling changes the determinant and is rejected. + doubled = from_formula(lambda x, y, z: (2 * x, 2 * y, 2 * z)) + require(not preserves_determinant(doubled), "rescaling wrongly preserves det") + controls += 1 + # Congruence by the shear [[1,0],[1,1]] keeps det but moves the labels off the set. + shear = from_formula(lambda x, y, z: (x, y + x, z + 2 * y + x)) + require(preserves_determinant(shear), "congruence by a unimodular shear keeps det") + require(label_permutation(shear) is None, "shear wrongly permutes labels") + controls += 1 + # Pairing the Hadamard image with the wrong profile breaks the residual. + image = tuple(apply(HADAMARD, f) for f in (scale(2, B), P, Q)) + total = add(add(image[0], image[1]), image[2]) + require(total != residual((1, 1, 0, 2)), "wrong profile wrongly matched") + controls += 1 + # The character table is not trivially excluding: all-old twice passes, once fails. + require(not excluded(character_table((2, 2, 2, 2), (), ())), "eight old calls wrongly excluded") + require(excluded(character_table((1, 1, 1, 1), (), ())), "four old calls not excluded") + controls += 1 + # A tampered frame is rejected by the decomposition check. + try: + check_decomposition(residual(NEW_PROFILE), ONCE, (scale(2, Q), A, add(B, A))) + except SystemExit: + controls += 1 + else: + raise SystemExit("FAIL: tampered decomposition accepted") + return controls + + +def main() -> None: + by_perm = check_group() + compositions = check_residuals(by_perm) + summary = check_orbits(by_perm) + check_named_witness() + new_box = check_new_profile_box() + transport_checks = check_transport_box(by_perm) + survivor_profiles = check_survivors(by_perm) + observed = open_orbit_box() + require(observed == EXPECTED_OPEN_BOX, f"open-orbit box counts changed: {observed}") + controls = check_controls(by_perm) + for name, (total, hit, supported, both) in observed.items(): + print( + f"OPEN_ORBIT_BOX {name} triples={total} character_excluded={hit}" + f" character_surviving={total - hit} support_passing={supported} passing_both={both}" + ) + print( + "PASS_THREE_FRAME_PROFILE_ORBITS" + f" group=8 compositions={compositions}" + f" census_orbits={summary['census_orbits']}" + f" open_profiles={summary['open_profiles']}" + f" open_orbits={summary['open_orbits']}" + f" four_call_orbits={summary['all_four_call_orbits']}" + f" new_profile_box={new_box}" + f" transport_checks={transport_checks}" + f" survivor_profiles={survivor_profiles}" + f" controls={controls}" + ) + + +if __name__ == "__main__": + main()