Transport three-frame character exclusions across count profiles: (1,1,2,0) excluded, twelve profiles not character-excludable (no κ)

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.