Prove D1^4 = I leaves the residual x1 monomial nonzero

research/residual-d1-fourth-power/PROOF.md

@@ -0,0 +1,152 @@
+# The omitted relation D1^4 = I does not kill the residual x1 word
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+No new κ is claimed. The selected frontier stays
+`781451/250000000`.
+
+Evidence class: **proof** that one named central relation does not send
+one explicit monomial to zero. The quotient is the predecessor group
+algebra modulo the principal ideal `(D1^4 - 1)`. The check reduces that
+one word. It is not an enumeration of words, not a search, and not a
+theorem about every physical quotient at once.
+
+## The named relation
+
+The predecessor algebra is the one installed by
+`research/coded-active-feedback/search.py`: the rational group algebra
+of the free product `C4(Q) * C2(C1) * C2(C3)`, with formal integer D
+exponents, and with `D_i` conjugating only `C_i` by `Q^{-1}`. That is
+`Q^4 = C1^2 = C3^2 = I` together with the inherited D conjugation rule
+from `research/coded-native-caller/gauge.py`. In that algebra `D1^4` is
+the normal form with empty word and degree `(4, 0)`, which is not `I`.
+
+The relation imposed here is the single extra equation
+
+```text
+D1^4 = I.
+```
+
+`research/coded-active-feedback/PROOF.md` names this law as omitted:
+the formal search adds `C1^2 = C3^2 = I` and `Q^4 = I`, keeps fresh D
+exponents as integers, and records that `D^4 = I` is a physical source
+relation not imposed there. `D1` is the stage-1 fresh eight-axis
+Gaussian in that note. The same note's opening conventions identify
+those stage operators with the fresh Gaussians.
+
+The displayed one-axis factor of that Gaussian law is the normalized
+matrix in `research/moving-stage-restoration-tariff/PROOF.md`,
+
+```text
+A = [[a, b], [b, a]],  a = (1+i)/2,  b = (1-i)/2.
+```
+
+Clearing the denominator, `2A = [[1+i, 1-i], [1-i, 1+i]]`. Exact
+arithmetic in `Z[i]` gives `(2A)^2 = 4 X` and `(2A)^4 = 16 I`, where
+`X = [[0, 1], [1, 0]]`. Therefore `A^2 = X` and `A^4 = I`, which is the
+sentence `D^2 = X` and `D^4 = I` in that note. The tariff applies the
+same normalized block Gaussian at width 8 to the eight-axis blocks.
+`research/coded-native-caller/PHYSICAL.md` writes each stage factor as
+a coordinate C gate and the fresh stage Gaussian as the product of the
+eight noncentral gates. This package does not replay that native
+product. The equation imposed on the residual is the one formal
+equation `D1^4 = I`. `D3^4 = I` is not imposed.
+
+## Reduction of the residual word
+
+Rightmost factors apply first in the engine, and the product is written
+left to right. The residual word of open question 2 in PR #7033 is
+
+```text
+Q^{-1} C1 Q^2 C1 C3 D1 D3.
+```
+
+The Q letters in the middle are adjacent and already form the normal
+syllable `Q^2`. The leading `Q^{-1}` is separated from them by `C1`, so
+the free-product reducer does not combine those runs. The two `C1`
+letters are separated by `Q^2`, so they do not cancel. `C3` remains at
+the right of the coefficient. The two D factors contribute degree
+`(1, 1)` and an empty word. The engine product is the single basis
+element
+
+```text
+word (-1, 2, 1, 1, 2, 3), degree (1, 1), coefficient 1.
+```
+
+`D1^4` commutes with each generator `Q, C1, C3, D1, D3`. It therefore
+commutes with their inverses and with every word. On this monomial the
+commutation is a pure shift: left or right multiplication by `D1^4`
+replaces the basis element by the same word at degree `(5, 1)`. The
+action of degree `(4, 0)` inserts `Q^{-4}` and `Q^4` around each `C1`,
+and those runs are empty because `Q^4 = I`. No coefficient is cancelled.
+
+The quotient by the central element `D1^4` identifies a normal form
+`(w, (e1, e3))` with `(w, (e1 + 4k, e3))` and with nothing else. Coset
+sums of coefficients are the quotient coordinates. The residual has one
+term, already at D1 exponent `1`, so its coset sum is `1` at
+
+```text
+((-1, 2, 1, 1, 2, 3), (1, 1)).
+```
+
+That coordinate is not zero. The same quotient sends `D1^4 - I` to zero,
+and it sends `D1^5` and `D1^{-3}` to the class of `D1`, which is not
+the class of `I`.
+
+## Q^{-1} C1 stays nonzero and distinct
+
+The comparison element is the single basis element
+
+```text
+Q^{-1} C1 = word (-1, 2), degree (0, 0), coefficient 1.
+```
+
+Its D1 exponent is `0`, so the coset of `D1^4` does not mix it with any
+other degree-`(0, 0)` word. The quotient coordinate is `1` at
+`((-1, 2), (0, 0))`. That is not the residual class. The Q-letter parity
+character, the sign of the number of letters of absolute value `1`,
+still sends this representative to `-1`.
+
+Thus `D1^4 = I` does not send the residual word to zero and does not
+collapse `Q^{-1} C1`.
+
+## Separating representation
+
+Let the basis of `C^8` be indexed by `q + 2 d1 + 4 d3` with each bit in
+`{0, 1}`. Define
+
+```text
+Q  = diag(i^q),   D1 = diag(i^{d1}),   D3 = diag(i^{d3}),
+C1 = swap of bits q and d1,            C3 = swap of bits q and d3.
+```
+
+These matrices are monomial, hence invertible. They satisfy `Q^4 = I`,
+`C1^2 = C3^2 = I`, commutation of each `D` with `Q` and with each other,
+commutation of `D1` with `C3` and of `D3` with `C1`, the two conjugation
+identities `D_s C_s = Q^{-1} C_s Q D_s`, and `D1^4 = I`. They also
+satisfy the further equations `D3^4 = I` and `(C1 C3)^3 = I`. Those
+further equations are relations of this representation only. They are
+not imposed on the formal quotient above.
+
+The representation is therefore a ring homomorphism out of the quotient
+by `D1^4 - I` into 8 by 8 matrices over the Gaussian integers. The image
+of the residual is an invertible monomial matrix, and the image of
+`Q^{-1} C1` is a different invertible monomial matrix. A homomorphism
+that sends an element to a nonzero matrix witnesses that the element
+was nonzero, and unequal images witness that the two elements were not
+equal.
+
+`C1` does not commute with `Q` in this representation, so the witness
+does not force the predecessor noncommutation `[C1, Q] = 0`.
+
+## What this does not claim
+
+The quotient does not produce an autonomous row. No owner-indexed
+multiplier is exhibited, and the four published banks are not reread.
+A later quotient that did kill the residual would still need its own
+multiplier before anyone could call the result an autonomous caller.
+
+`D3^4 = I` is a different equation and is not part of the quotient.
+Nonzero D exponents, owner mixing, and any feedback edge other than the
+published pair stay outside. The result is not a change of the selected
+conditional κ.

research/residual-d1-fourth-power/README.md

@@ -0,0 +1,127 @@
+# D1^4 = I leaves the residual x1 monomial nonzero
+
+**Scoped proof; no new κ.** The formal algebra of the published two-edge
+feed imposes `Q^4 = C1^2 = C3^2 = I` and the inherited rule that `D_i`
+conjugates only `C_i` by `Q^{-1}`. One physical relation omitted by that
+algebra is the fresh-Gaussian equation `D1^4 = I`. In the quotient by
+that single central equation, the residual word
+
+```text
+Q^{-1} C1 Q^2 C1 C3 D1 D3
+```
+
+keeps the representative with word `(-1, 2, 1, 1, 2, 3)` and degree
+`(1, 1)`, coefficient 1. The comparison element `Q^{-1} C1` keeps the
+distinct representative with word `(-1, 2)` and degree `(0, 0)`, and the
+Q-letter parity character still sends that representative to `-1`.
+
+[PROOF.md](PROOF.md) gives the coset reduction and an 8-dimensional
+separating representation. The representation also satisfies `D3^4 = I`
+and `(C1 C3)^3 = I`. Those two equations are extra relations of the
+matrices. They are not part of the formal quotient.
+
+The selected frontier is unchanged. This quotient is not an autonomous
+caller. No multiplier is exhibited.
+
+## Result
+
+`research/coded-active-feedback` records that `D^4 = I` is a physical
+source relation not imposed on its formal algebra. The stage-1 instance
+of that law is `D1^4 = I`. In the predecessor algebra this element is
+the empty word at degree `(4, 0)`, so the equation is not already true.
+
+Multiplying the residual by `D1^4` only adds 4 to the D1 exponent. The
+quotient therefore leaves the exponent-1 representative in place, with
+coefficient 1. `D1^4 - I` itself reduces to zero, and `D1` does not.
+
+The one-axis factor `A = [[a, b], [b, a]]` with `a = (1+i)/2` and
+`b = (1-i)/2` satisfies `A^2 = X` and `A^4 = I` by exact arithmetic in
+`Z[i]`. That is the matrix law named in the moving-stage tariff. The
+native eight-axis word is not replayed.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3 -B scripts/research_package.py --package research/residual-d1-fourth-power --check-only
+python3 -B scripts/research_package.py --package research/residual-d1-fourth-power
+```
+
+Direct replay:
+
+```sh
+python3 -I -W error -B research/residual-d1-fourth-power/verify.py
+python3 -I -O -W error -B research/residual-d1-fourth-power/verify.py
+```
+
+The optimized command still executes the checks. They are `need`
+failures, not assertions. No network, native build, or full multiplier
+replay is used. The run prints `PASS_RESIDUAL_D1_FOURTH_POWER` and
+`new_kappa null`.
+
+## Scope
+
+Original card: `joint-query-controller`. Scope status: **refined**. The
+card asks for one source-bound caller identity, or an obstruction to
+that change, together with its charges. This package does not change
+the query demand. It takes open question 2 of the D-exponent-0 x1
+obstruction, the question posed by
+[PR #7033](https://github.com/CrocSwap/integer-mult-bounds/pull/7033)
+and recorded in
+[discussion comment 19513870](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19513870).
+The first step named there is one source relation outside
+`Q^4 = C1^2 = C3^2 = I` and the inherited D conjugation rule. The
+relation used here is `D1^4 = I`.
+
+Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in
+[SOURCES.json](SOURCES.json). The catalogue is provenance. The selected
+record, `search.py`, `gauge.py`, and the three cited proofs are live
+inputs. The selected conditional value is the selected record,
+`781451/250000000`.
+
+Overlap at this base used `scripts/find_overlap.py`. Local notes at
+`17469fff78c22941280f04d39dc5a1faee09c840` (10178 paths, complete
+inventory), 339 open-PR records fetched at 2026-11-10T10:19:05Z, and
+7013 discussion records fetched at 2026-11-10T10:20:14Z. The phrase
+`Q^{-1} C1 Q^2 C1 C3` matches PR #7033 and
+[discussion comment 19513867](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19513867),
+which ask this question. Requiring both `physical relation` and `D^4`,
+and both `omitted` and `D^4=I`, matched nothing in that snapshot. The
+search is not a novelty certificate. Closed PR bodies were outside the
+open-PR snapshot.
+
+## Open next questions
+
+Does one linear source relation, compatible with
+`Q^4 = C1^2 = C3^2 = I` and the inherited D conjugation rule, send the
+coefficient word `Q^{-1} C1 Q^2 C1 C3` to zero while leaving
+`Q^{-1} C1` nonzero? `D1^4 = I` meets this word only by adding multiples
+of 4 to a D exponent that is already zero on the coefficient, so the
+coset sum stays 1. A linear dependence among distinct degree-zero words
+could behave differently. The first step is to evaluate
+`C = diag(K_i)^{-1} F diag(K_i)` from
+`research/native-involutive-dual/PROOF.md` on one shared central axis
+and reduce this coefficient there. This package does not evaluate `F`.
+
+If a later quotient does send the residual to zero and keeps
+`Q^{-1} C1` nonzero, which owner-indexed multiplier on the four
+published banks becomes the autonomous row `[A, 0, 0, 0]`? Killing the
+monomial in a quotient is not yet a caller. The first step is to name
+that quotient and recompute the four columns. No such quotient is
+constructed here.
+
+## Credit
+
+The trace, algebra, and omitted-relation sentence are Cinna Davis's
+`research/coded-active-feedback`, using Dugongue's PR4948 chronology,
+Dillon's PR4933 code, and the gauge engine in
+`research/coded-native-caller/gauge.py`. The normalized one-axis law
+`D^2 = X`, `D^4 = I` is Nick Petalas's
+`research/moving-stage-restoration-tariff`. The residual monomial and
+the question are the open remainder of the D-exponent-0 x1 obstruction.
+The nonzero D-exponent multiplier question from that obstruction is a
+separate question and is not answered here.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance.
+Apache-2.0.

research/residual-d1-fourth-power/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "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/coded-active-feedback/PROOF.md",
+      "usage": "input",
+      "git_blob": "9716baebb4895b07acf9db0cbce010590b03945a",
+      "sha256": "c6233d2759811190c7ea1be455c9351b61c29f6a8afc8584e7bc0dfbc00f3a3d"
+    },
+    {
+      "path": "research/coded-active-feedback/search.py",
+      "usage": "input",
+      "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e",
+      "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6"
+    },
+    {
+      "path": "research/coded-native-caller/PHYSICAL.md",
+      "usage": "input",
+      "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f",
+      "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078"
+    },
+    {
+      "path": "research/coded-native-caller/gauge.py",
+      "usage": "input",
+      "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167",
+      "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad"
+    },
+    {
+      "path": "research/moving-stage-restoration-tariff/PROOF.md",
+      "usage": "input",
+      "git_blob": "a571bb602aefe6d1eddcd15b189751bef5b31ebe",
+      "sha256": "36d3b13ab3919559fde46b1c33f856379cd5b2bab06d835ddf7e177c96868712"
+    }
+  ]
+}