Record equal degree-8 factors for odd-sign weight-4 pairs.

research/c3-weight4-odd-sign-factors/PROOF.md

@@ -0,0 +1,180 @@
+# Odd-sign cross-coset pairs do not split the weight-4 degree-16 polynomial
+
+The selected conditional kappa stays `781451/250000000`. Nothing here changes
+that frontier, replaces the degree-881 one-slot certificate, or reclassifies
+the signed-permutation stabilizer.
+
+Two claim types are used, and they are not interchangeable.
+
+- A **proof for one named pair** exhibits the joint spaces, the integer
+  matrices of `B = 4 A_3`, their characteristic polynomials, a spanning
+  determinant, and the identity `B(B^2 - 64 I) = 0`.
+- An **exhaustive finite census** checks every element of the described list
+  of 96 splitting involutions, and every one of the 32 diagonal signs with
+  equal even coordinates. The passage from those 96 operator identities to
+  all `3072` unordered cross-coset pairs is the reduction below. It is not a
+  sample. Completeness of the list of 96, as the set of all residual signed
+  permutations that split every `c=3` character, is the census in
+  `research/c3-centre-sign-split`. It is not repeated here.
+
+## Operator and the weight-4 character
+
+The input is the pinned 8-by-112 query, SHA256
+`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`.
+On `Q^8 ⊗ Q[F_2^9]`,
+
+```text
+A_3 = (1/4) sum_q r_q r_q^T ⊗ P_q(3),
+B   = 4 A_3.
+```
+
+`P_q(3)` is the same sector-3 action used for the degree-16 polynomial in
+upstream PR #7021. `H` is the order-16 group of diagonal signs that are
+positive on the even coordinates `{0,2,4,6}` and arbitrary on the odd
+coordinates `{1,3,5,7}`. The weight-4 character is
+
+```text
+chi(h) = product of the signs of h on coordinates 1, 3, 5 and 7.
+```
+
+The canonical signed-orbit basis of the equations `h v = chi(h) v` has
+dimension 32. Call this space `W`.
+
+## The named pair
+
+Let `u0`, `v0` and `w0` be the explicit no-odd-minus involutions recorded by
+#6965 and used again by #7021:
+
+| name | permutation | minus signs |
+|---|---|---|
+| `u0` | `(0 2)(4 6)` | coordinates 0 and 2 |
+| `v0` | `(0 4)(2 6)` | coordinates 0 and 4 |
+| `w0` | `(0 6)(2 4)` | coordinates 0 and 6 |
+
+The named pair keeps those even signs and puts a minus on odd coordinate 1
+only:
+
+| name | permutation | minus signs |
+|---|---|---|
+| `u` | `(0 2)(4 6)` | coordinates 0, 1 and 2 |
+| `v` | `(0 4)(2 6)` | coordinates 0, 1 and 4 |
+
+Both are in the described list of 96. Both fix sector 3, both square to the
+identity, and they commute. Their product is exactly `w0`, whose odd signs
+are all positive. The odd-sign pattern of the pair is nontrivial: coordinate
+1 is negative and coordinates 3, 5 and 7 are positive.
+
+The same odd signs with both even cycles left positive send sector 3 to 48.
+So do equal minus signs on the two even cycles. Those patterns are symmetries
+of the query, but they are not splitting involutions of sector 3 and they are
+not the pair under test.
+
+Let `d` be the diagonal sign with a minus on coordinate 1 only. The composite
+that applies `u0` first and `d` second equals `u`, including the port map, and
+the same composite with `v0` equals `v`. On `W`, `d` acts as `-I`.
+
+## Direct factorisation of the named pair
+
+Inside `W`, each of the four joint spaces of `(u, v)` has dimension 8. In the
+canonical basis of each space the matrix of `B` has characteristic polynomial
+
+```text
+x^4 (x - 8)^2 (x + 8)^2,
+```
+
+so the characteristic polynomial of `A_3` is
+
+```text
+x^4 (x - 2)^2 (x + 2)^2.
+```
+
+Ascending-coefficient SHA256, matching the degree-8 fingerprint recorded by
+#7021:
+
+```text
+4078d16db1834dcd427c4f1094b96838a2c425c116c7cd1b60d46aa1f472f632
+```
+
+Each matrix of `B` is killed by `x(x - 8)(x + 8)`. The minimal polynomial
+therefore divides a square-free polynomial, so `A_3` is diagonalizable over
+`Q` on each joint space. Algebraic and geometric multiplicities agree:
+eigenvalue `0` has multiplicity 4, and eigenvalues `2` and `-2` each have
+multiplicity 2.
+
+The `u = +1` space and the `u = -1` space each have dimension 16. Each is the
+direct sum of its two joint spaces: the sixteen joint basis vectors are
+linearly independent modulo `1000003` when written in the canonical basis of
+that 16-dimensional space. `B` preserves each joint space, so the
+characteristic polynomial of the 16-dimensional space is the product of the
+two degree-8 polynomials. Both factors are the same polynomial, and the
+product is
+
+```text
+x^8 (x - 2)^4 (x + 2)^4,
+```
+
+SHA256
+
+```text
+4207a8e80e73e3fcd16abc6cba001f8e9881023742eeb587cbd8fbadd9f24350
+```
+
+which is the degree-16 polynomial recorded by #7021. The named pair therefore
+does not split that polynomial into two different degree-8 factors.
+
+The same canonical bases, with both eigenvalues flipped, are the four joint
+bases of the explicit pair `(u0, v0)`. That identifies the spaces. It is not
+a second factorisation of the no-odd-minus pair; #7021 already recorded that
+pair.
+
+## The other odd-sign patterns
+
+A diagonal sign whose four even coordinates carry one common sign, and whose
+odd signs are arbitrary, is one of 32 signs. All 32 fix sector 3. On `W`,
+each acts by the scalar
+
+```text
+(product of its four odd signs) * (its common even sign).
+```
+
+In particular every element of `H` acts by `chi`, and the all-even-minus
+diagonal acts by `-1`. This is checked on every vector of the 32-dimensional
+basis, for every one of the 32 signs. A diagonal with unequal even signs need
+not act by a scalar; the control with a minus on coordinate 0 only does not.
+
+Every described splitting involution has the same coordinate permutation as
+exactly one of `u0`, `v0` and `w0`. It equals the composite that applies that representative first and one of
+the 32 diagonals second. The equality includes the port map. Therefore, on
+`W`, the involution acts as that diagonal's scalar times the representative. Both scalars occur, 16 times in each of the three permutation
+cosets.
+
+The three representatives form one Klein group: `w0 = u0 v0`, and `u0` and
+`v0` commute. Any cross-coset pair is an unordered pair of described
+involutions from two different nontrivial cosets. There are
+`3 · 32 · 32 = 3072` such pairs. On `W`, the pair acts as a pair of scalars
+times two of `u0`, `v0` and `w0`. The four joint eigenspaces are the four
+joint spaces of `(u0, v0)`, up to swapping eigenvalue labels. All four have
+the degree-8 polynomial computed above. No described cross-coset pair splits
+the degree-16 polynomial into two different degree-8 factors.
+
+Same-coset pairs are not cross-coset pairs. The named `u` and the explicit
+`u0` have the same permutation; on `W` they differ by the scalar `-1`, so
+they do not give a four-way split.
+
+## What is not claimed
+
+The argument uses the weight-4 character in an essential way. On a weight-3
+character the same explicit pair has joint dimensions `44 + 12 + 12 + 12`,
+and the predecessor records that the slot of the large piece moves with the
+trace signs. The scalar reduction above does not determine the characteristic
+polynomial of one of those 12-dimensional spaces.
+
+The list of 96 is an input description, not a new classification. Payload
+involutions are outside that list. An involution that is not one of the 96
+is not covered, so this is not an unrestricted nonexistence statement. No
+κ change is claimed.
+
+The characteristic polynomials were recomputed from the query by the Newton
+identities and compared with the block products `x(x ± 8)`. A failed test of
+one pair was not used as a universal negative. The 96-element statement is
+the complete check of the described list.

research/c3-weight4-odd-sign-factors/README.md

@@ -0,0 +1,121 @@
+# Odd-sign factors of the weight-4 degree-16 polynomial
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+On the weight-4 character of sector `c=3`, the cross-coset pair whose odd
+signs are minus on coordinate 1 only does not split the common degree-16
+polynomial of upstream PR #7021 into two different degree-8 factors. Both
+joint factors are
+
+```text
+x^4 (x - 2)^2 (x + 2)^2.
+```
+
+The same equality holds for every cross-coset pair from the described list of
+96 splitting involutions. [PROOF.md](PROOF.md) separates the direct
+factorisation of the named pair from that finite census.
+
+No new kappa. The selected conditional kappa stays `781451/250000000`.
+
+## Result
+
+The live input is the query pinned in [SOURCES.json](SOURCES.json), SHA256
+`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`.
+The named pair is
+
+| name | permutation | minus signs |
+|---|---|---|
+| `u` | `(0 2)(4 6)` | coordinates 0, 1 and 2 |
+| `v` | `(0 4)(2 6)` | coordinates 0, 1 and 4 |
+
+Its product is the explicit no-odd-minus involution `(0 6)(2 4)` with minus
+signs on coordinates 0 and 6. Each of the four joint spaces has dimension 8
+and characteristic polynomial `x^4 (x - 2)^2 (x + 2)^2` for `A_3`. Each
+eigenspace of `u` has dimension 16, and its characteristic polynomial is the
+square
+
+```text
+x^8 (x - 2)^4 (x + 2)^4.
+```
+
+The two degree-8 factors of that square are equal. Ascending-coefficient
+SHA256 values agree with the polynomials recorded by #7021:
+
+```text
+degree 8   4078d16db1834dcd427c4f1094b96838a2c425c116c7cd1b60d46aa1f472f632
+degree 16  4207a8e80e73e3fcd16abc6cba001f8e9881023742eeb587cbd8fbadd9f24350
+```
+
+`B = 4 A_3` is killed by `x(x - 8)(x + 8)` on each of these spaces, so `A_3`
+is diagonalizable over `Q`. On each joint space the multiplicities are 4, 2
+and 2 for eigenvalues `0`, `2` and `-2`.
+
+Every one of the 96 described involutions acts on the weight-4 space as `±`
+the no-odd-minus representative of its permutation. Both signs occur 16 times
+in each of the three cosets. Every one of the `3072` unordered cross-coset
+pairs therefore has the same four joint spaces, up to eigenvalue labels, and
+the same equal degree-8 factors.
+
+## Scope
+
+Catalogue card `formal-interface-lemma` asks for a formal interface binding.
+The question answered here is open-next item 1 of upstream PR
+[#7021](https://github.com/CrocSwap/integer-mult-bounds/pull/7021):
+whether one cross-coset pair with a nontrivial odd-sign pattern splits the
+common degree-16 polynomial into two different degree-8 factors. The first
+step named there is the three even double transpositions with a minus on
+coordinate 1 only. This package factors that pair and then checks the rest of
+the described list.
+
+It does not recompute the degree-16 theorem as a new result for the
+no-odd-minus pair, and it does not repeat the signed-permutation
+classification of #6965. The 12-dimensional weight-3 polynomial and the
+payload-involution questions are not taken.
+
+Selected-baseline orientation returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`
+for kappa `781451/250000000`.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+python3 -B -W error research/c3-weight4-odd-sign-factors/verify.py
+python3 -B -O research/c3-weight4-odd-sign-factors/verify.py
+python3 -B scripts/research_package.py --package research/c3-weight4-odd-sign-factors --check-only
+```
+
+The marker is `PASS_C3_WEIGHT4_ODD_SIGN_FACTORS`. Acceptance uses explicit
+checks, so `-O` does not skip a theorem, the census, or a rejection control.
+On the measured host one run takes about one second. No Lean, Docker,
+degree-881 replay, or selected cold replay was run.
+
+## Overlap
+
+Canonical main was fetched at session start and was still
+`17469fff78c22941280f04d39dc5a1faee09c840`. Local
+`scripts/find_overlap.py --offline` searched 10178 of 10178 note paths. The
+weight-4 polynomial is not in this tree; it is the open package of #7021.
+A GitHub search of open pull requests for `odd-sign degree-8 factors` returned
+only #7021, which asks this question. A search for `cross-coset` also returned
+#7020, the payload-involution split, which is a different operator. Fork
+branches named `cursor/*` did not already contain an odd-sign factorisation
+of this polynomial. This search is not a novelty certificate.
+
+## Open next questions
+
+The structured list is in [TASK.json](TASK.json).
+
+- The odd-sign reduction uses the weight-4 character. It does not determine
+  the characteristic polynomial of one 12-dimensional joint space of a
+  weight-3 `c=3` character. That question remains the second open item of
+  #7021.
+
+## Credit
+
+The explicit pair, the list of 96 involutions, and the count of 3072
+cross-coset pairs come from upstream PR #6965. The degree-16 polynomial, the
+degree-8 polynomial of the no-odd-minus pair, and the question answered here
+come from upstream PR #7021. The query and the Bell action are Ali Romman's
+PR4958 and PR4720. The doubled representation comes from PR1719. New work is
+Apache-2.0.

research/c3-weight4-odd-sign-factors/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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"
+    },
+    {
+      "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json",
+      "usage": "input",
+      "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3",
+      "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3"
+    }
+  ]
+}