Record that c=1 movers miss the 8-dimensional dihedral summand.

research/c1-mover-8-summand/PROOF.md

@@ -0,0 +1,166 @@
+# Movers miss the 8-dimensional dihedral summand
+
+This is an exhaustive finite census, together with an exact rank computation
+over `Q`, for one subspace of the historical one-slot doubled centre block at
+Bell label `c=1`. It is not a characteristic polynomial, not an annihilator of
+the full one-slot operator, and not a multiplication bound.
+
+The selected conditional kappa stays `781451/250000000`.
+
+## Operators and the group
+
+The input is the 8-by-112 query retained by
+`research/centre-polynomial-cache-limits/`. Its columns lie in `{-1,0,1}^8`,
+each has weight 4, and `R R^T = 56 I_8`. The 112 port labels are distinct odd
+vectors in `F_2^9`.
+
+A signed coordinate permutation acts by `(S v)_k = eps[k] v[inv[k]]` and by
+the linear port map `T` that carries each port to the port of its image
+column. On `R^8 ⊗ R[F_2^9]`, of dimension 4096, the operator is `S ⊗ U_T`.
+Both factors are monomial with nonzero entries `±1`, so the operator is
+orthogonal for the standard Euclidean product. Its trace is
+
+    tr(S) · 2^{nullity(T - I)}.
+
+Let `W` be the hyperoctahedral group of signed permutations of the eight
+coordinates, of order `8! · 2^8 = 10321920`. Let `A` be the subset that sends
+every query column to a scalar multiple of a query column. The 13 signed
+permutations used as generators in `research/exact-one-slot-gram/` lie in
+`A`. Their generated subgroup has order `344064`. The left cosets of this
+subgroup in `W` number 30, and `344064 · 30 = 10321920`. Exactly one coset
+preserves the column lines, namely the subgroup itself. Therefore the
+subgroup is all of `A`.
+
+The stabilizer `A(c=1) = {s ∈ A : T_s(1) = 1}` has order 3072. These are
+exactly the signed coordinate permutations that preserve sector `c=1`. The
+completeness argument is this coset decomposition, not a search that stopped
+early.
+
+## The 216-space and the 8-dimensional summand
+
+Let `H` be the group of coordinate sign patterns in `A(c=1)` with positive
+sign on coordinate 0. It has order 16. PR #6944 fixes the commuting
+involutions
+
+| name | permutation | output signs |
+|---|---|---|
+| `g` | `(1 2)(5 6)` | minus on coordinates 4 and 7 |
+| `t` | `(1 5)(2 6)` | minus on coordinates 3 and 7 |
+
+The trivial character of `H` has dimension 864. The joint `(+1,+1)` dimension
+
+    (tr_V(1) + tr_V(g) + tr_V(t) + tr_V(gt)) / 4
+
+equals 216. The same 216 is the dimension of the lattice of vectors fixed by
+`H`, by `g`, and by `t`. The verifier rebuilds that lattice and checks that
+it equals the published basis in
+`research/a1-joint-216-charpoly/evidence/basis.json`. Call this space `E`.
+
+PR #7008 produces a dihedral image of order 12 on `E`, generated by
+
+| name | `inv` | output signs |
+|---|---|---|
+| `r` | `(0, 1, 6, 7, 3, 2, 5, 4)` | minus on coordinates 0 and 7 |
+| `u` | `(0, 1, 2, 3, 7, 6, 5, 4)` | all positive |
+
+Here `(S v)_k = eps[k] v[inv[k]]`. The element `r` has order 6 and `u`
+inverts `r`. Both preserve sector 1 and preserve `E`. Let `ψ` be the linear
+character `ψ(r^k) = (-1)^k` and `ψ(r^k u) = (-1)^{k+1}`. The corresponding
+central projector is
+
+    P = (1/12) ∑_{g ∈ ⟨r,u⟩} ψ(g) g.
+
+The verifier builds `12P` on the published basis of `E`, checks
+`(12P)^2 = 12 · (12P)`, and finds trace 96, so `P` is a projector of rank 8.
+An explicit basis of the image `V` is
+
+    w_i = e_{a_i} - e_{b_i} + e_{c_i},
+
+with joint-basis indices
+
+| i | a | b | c |
+|---|---:|---:|---:|
+| 0 | 104 | 120 | 142 |
+| 1 | 105 | 121 | 143 |
+| 2 | 106 | 122 | 140 |
+| 3 | 107 | 123 | 141 |
+| 4 | 116 | 124 | 134 |
+| 5 | 117 | 125 | 135 |
+| 6 | 118 | 126 | 132 |
+| 7 | 119 | 127 | 133 |
+
+Each `w_i` is fixed by `12P`. The eight vectors are linearly independent, so
+they are a basis of `V`. Both `r` and `u` act on this basis by `-I`. The
+Gram matrix in the standard Euclidean product is `48 I_8`, so the form is
+positive definite on `V` and the basis is orthogonal.
+
+This note does not recompute the characteristic polynomial of `A_1` on `V`.
+Reducibility of `V` under `A_1` remains the statement proved by PR #7023.
+
+## Census
+
+An element `s ∈ A(c=1)` preserves `E` when `s` sends every vector of the
+published basis into `E`. The verifier tests all 3072 elements.
+
+| set | order |
+|---|---:|
+| `A(c=1)` | 3072 |
+| elements with `sE = E` | 768 |
+| elements that move `E` | 2304 |
+
+On each of the 768 preservers, the matrix of `s` in the basis `(w_i)` is
+`+I` for 384 elements and `-I` for 384 elements. In particular every
+preserver preserves `V` and acts by a scalar. PR #7022 already places every
+preserver outside the normalizer of `{1,g,t,gt}` among these 768 elements, so
+those elements are scalar on `V` as well. This census does not recompute that
+normalizer. The scalar count is a control: the membership test accepts the
+action that PR #7008 predicts from the linear character, and it is not the
+statement about movers.
+
+For each of the 2304 movers the same test gives two facts.
+
+1. Every image `s(w_i)` is orthogonal to every basis vector `w_j`. Therefore
+   `s(V) ⊥ V`. Since the Gram matrix is `48 I_8`, `V` is not orthogonal to
+   itself, so `s(V) ≠ V`.
+
+2. Write `ρ` for the quotient map `Q^{4096} → Q^{4096}/E` along the
+   orthogonal complement of `E`. The eight vectors `ρ(s(w_i))` are linearly
+   independent over `Q`. Therefore `ρ ∘ s` is injective on `V`, and
+
+   `s(V) ∩ E = {0}`.
+
+Either fact implies that `s` does not preserve `V`. The second is stronger:
+the whole image misses `E`, not only the individual basis vectors. A linear
+combination of the eight images cannot land back in `E`.
+
+Thus no element of `A(c=1)` that moves `E` preserves `V`. A fortiori, none
+preserves `V` and acts non-scalarly on it.
+
+## One explicit mover
+
+Let `m` be the signed permutation with `inv = (3, 1, 2, 0, 4, 6, 5, 7)` and
+every output sign positive. The coordinate map `k ↦ inv[k]` is the
+permutation `(0 3)(5 6)`. It lies in `A(c=1)`, it does not preserve `E`, all
+eight images `m(w_i)` miss `E`, and those images remain linearly independent
+modulo `E`. Repeating one residual drops that rank from 8 to 7, so the rank
+test can see a dependence.
+
+Two preservers are recorded as controls, with the same basis of `V`. The
+normalizer element `u` acts by `-I`. The coordinate-1 sign `h` is orthogonal
+and has compressed trace 216 on `E`. For an orthonormal basis `(v_j)` of `E`,
+that trace is `∑ ⟨h v_j, v_j⟩`, and Cauchy-Schwarz gives `h v_j = v_j`, so
+`h|_E = I`. The product `u h` is the witness of PR #7022. It has compressed
+trace 72 on `E`, so it is non-scalar on `E`, and it acts by `-I` on `V`. A
+non-scalar action on `E` is not a non-scalar action on `V`.
+
+## What this does not say
+
+The census is restricted to `A(c=1)` and to this one subspace `V`. It does
+not claim that an element of `A` outside the `c=1` stabilizer fails to
+preserve `V`. It does not identify which character space contains `m(V)`. It
+does not treat the 80-dimensional or 128-dimensional dihedral components, and
+it does not use the different 8-dimensional joint space of the nontrivial
+sign character studied in PR #7019.
+
+No characteristic polynomial is computed. The degree-881 one-slot annihilator
+is untouched. The selected conditional kappa stays `781451/250000000`.

research/c1-mover-8-summand/README.md

@@ -0,0 +1,97 @@
+# c=1 movers miss the 8-dimensional dihedral summand
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+No element of the `c=1` stabilizer that moves the trivial-character `(+1,+1)`
+216-space preserves the 8-dimensional dihedral isotypic summand inside that
+space. For every one of the 2304 movers, the image of the summand misses the
+216-space entirely. No new kappa. The selected conditional kappa stays
+`781451/250000000`.
+
+## Scope and evidence
+
+Catalogue card `formal-interface-lemma`, scope changed. The card asks for a
+formal caller binding. The assigned question is open question 1 of
+[PR #7022](https://github.com/CrocSwap/integer-mult-bounds/pull/7022): does
+any `c=1` stabilizer element that moves the 216-space preserve the
+8-dimensional dihedral isotypic summand and act non-scalarly on it?
+
+The answer is no. The stabilizer has order 3072. Exactly 768 elements
+preserve the 216-space, and 2304 move it. None of the movers preserves the
+summand. The proof, the named mover `(0 3)(5 6)`, and the hypotheses are in
+[PROOF.md](PROOF.md). Source pins are in [SOURCES.json](SOURCES.json). The
+selected record and the task catalogue are historical provenance.
+
+Evidence class: exhaustive finite census of a finite set of order 3072, plus
+an exact rank computation over `Q` for each mover. The completeness argument
+is the decomposition of the hyperoctahedral group into 30 left cosets of the
+line-preserving subgroup of order 344064. This is not a heuristic or
+incomplete search. It is not an unrestricted nonexistence claim about
+operators outside this stabilizer.
+
+The 768 preservers of the 216-space all preserve the summand and act by `±I`,
+with 384 elements of each sign. That agrees with the linear-character
+prediction in PR #7008 and with the placement, in PR #7022, of the
+outside-normalizer preservers among those 768 elements. It is a control on
+the membership test. It is not a new normalizer census, and it is not the
+answer to the mover question.
+
+PR #7023 already proved that this summand is reducible under `A_1`. This
+package rebuilds the projector only to name the subspace. It does not
+recompute that characteristic polynomial. The different 8-dimensional joint
+space of PR #7019 meets the 216-space only at zero and is not this summand.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+python3 -B -W error research/c1-mover-8-summand/verify.py
+python3 -B -O research/c1-mover-8-summand/verify.py
+python3 -B scripts/research_package.py --package research/c1-mover-8-summand --check-only
+```
+
+The marker is `PASS_C1_MOVER_8_SUMMAND`. Acceptance uses explicit checks, so
+`-O` does not skip an element or a rejection control.
+
+Not run: Lean, Docker, the degree-881 replay, any characteristic polynomial,
+and the selected cold replay. Selected-baseline orientation is source-binding
+only.
+
+## Overlap
+
+`scripts/find_overlap.py --refresh` was run on 2026-11-10 against upstream
+`17469fff78c22941280f04d39dc5a1faee09c840`. Coverage: local notes 10180,
+HEAD paths 10178, complete; 339 open PRs, pagination complete, fetched
+2026-11-10T10:22:32Z; 7013 discussion records, pagination complete, fetched
+2026-11-10T10:23:39Z. The phrases `8-dimensional dihedral`, `moves the 216`,
+and `isotypic summand` match PR #7008, PR #7022, and PR #7023, which ask or
+narrow this question, and PR #7019, which states that its 8-dimensional joint
+space is a different subspace. No open PR reports the action of a mover on
+this summand. Closed PRs were searched through local READMEs, task metadata,
+and the ledger only. No code diffs.
+
+## Open next questions
+
+See [TASK.json](TASK.json).
+
+- For the named mover `(0 3)(5 6)`, does `g` or `t` act by a scalar on the
+  image of the summand? The image misses the `(+1,+1)` space, and this
+  package does not test the other three joint signs. This is not the
+  basis-transport question of PR #7019, which uses a different 8-dimensional
+  space.
+- Does any element of the line-preserving group outside the `c=1` stabilizer
+  preserve this summand and act non-scalarly? The census stops at sector
+  `c=1`.
+
+## Credit
+
+JoyboyBrian recorded the sign-character dimensions. PR #6944 split the
+trivial `c=1` character into 216-dimensional blocks. PR #6964 pinned the
+basis of one 216-space. PR #7008 computed the dihedral image and the
+multiplicity-8 character. PR #7022 enumerated the stabilizer action on the
+216-space and left the mover question open. PR #7023 built the basis of the
+summand used here and proved reducibility under `A_1`. Ali Romman's PR #4958
+and PR #4720 retain the query and the Bell action. Krzysztof Wojt's
+`research/exact-one-slot-gram/` supplies the 13 generators. The doubled
+representation comes from PR #1719. New work is Apache-2.0.

research/c1-mover-8-summand/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/a1-joint-216-charpoly/evidence/basis.json",
+      "usage": "input",
+      "git_blob": "5e524a41ed1c65017b7d902b5445aedd2eb606ff",
+      "sha256": "e198cd71f4100d2629ecc25fb40b135a8c18c7756be8bc80bf24d7b349af418a"
+    },
+    {
+      "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json",
+      "usage": "input",
+      "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3",
+      "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3"
+    }
+  ]
+}