All-width certificate for the complete #5413 caller: group-algebra lifting lemma, 896 port identities, free body, abelian controller (no new kappa)

research/allwidth-caller-certificate/PROOF.md

@@ -0,0 +1,115 @@
+# A lifting lemma and its certificate for the selected caller
+
+Mark (Matarener), with substantial Claude Code assistance. Apache-2.0. No new κ.
+
+## 1. Setting
+
+Fix a finite group `G` of exact complex matrices on `D = 2^n` coordinates. Here `G` is the dyadic Clifford group of
+nine (locally) or 145 (globally) binary axes with its absolute phase, so the central scalars `i^k I` are elements
+of `G`. A scalar register program with fixed coefficients evaluates, at column multiplicity `f`, to an operator
+whose entries are finite sums
+
+    A_f = sum_g c_g g^{(x) f},        c_g in C fixed, independent of f.
+
+The native operators enter only through `g^{(x) f}`; the coefficients `c_g` of ADD and SCALE instructions stay
+outside the tensor power. This is the free-word evaluation convention of the selected proof review (#4359
+`PROOF-REVIEW.md` section 2) and of PR5376.
+
+## 2. Lemma
+
+**Lemma.** For `a = sum_g c_g g` in `C[G]`, the operators `A_f = sum_g c_g g^{(x) f}` vanish for every positive
+integer `f` if and only if `a = 0` in `C[G]`.
+
+*Proof.* The map `rho_f: g -> g^{(x) f}` is a group homomorphism `G -> GL(D^f)`, because
+`(gh)^{(x) f} = g^{(x) f} h^{(x) f}`. Its linear extension to `C[G]` is an algebra homomorphism, so `a = 0`
+implies `A_f = rho_f(a) = 0` for every `f`. Conversely suppose `rho_f(a) = 0` for all `f >= 1`. Let `rho = rho_1`,
+which is faithful because `G` is a group of matrices. The representation `rho (x) R`, with `R` the regular
+representation, is `D` copies of `R` and contains every irreducible representation of `G`. By Burnside's theorem
+every irreducible representation of `G` occurs in some tensor power `rho^{(x) m}`, `m >= 0`, so every irreducible
+representation occurs in some `rho^{(x) (m+1)}` with `m + 1 >= 1`. Hence `a` acts as zero in every irreducible
+representation, and `a = 0` in `C[G]`. ∎
+
+Three consequences are used below.
+
+1. **Group identities lift.** If two products of native generators are the same element of `G` (same Pauli
+   tableau and same action on the basis state `|0>`, which fixes the absolute phase), they agree at every width.
+   This covers inverses, exponent two (`C_0^2 = X_0`), commutation of operators on disjoint axes, Hadamard
+   children, phases and spectators (tensoring with the identity on the untouched axes is again an element of the
+   larger Clifford group).
+2. **Free-word identities lift.** An identity that holds in the free group algebra on the native symbols, with
+   only adjacent inverse cancellation, holds in `C[G]` under every assignment of symbols to group elements, hence at
+   every width.
+3. **Linear relations between distinct elements do not lift.** `C_0 = (1+i)/2 I + (1-i)/2 X_0` is an identity of
+   matrices at width one and a nonzero element of `C[G]` (three distinct group elements); it fails at width two.
+   The same holds for the scalar `i` against the element `iI`, whose tensor square is `-I`. A certificate must
+   therefore keep the scalar layer and the group layer apart, exactly as the selected convention prescribes.
+
+The census `a = 0 in C[G]` is a complete decision procedure: no finite set of widths has to be evaluated. PR5369 and
+PR5376 prove the same criterion in the quantitative form of finite width cutoffs (four and eight widths), which is
+what one needs when the distinct group elements cannot be canonicalized; here they can, by `clifford_exact.py`.
+
+## 3. The selected caller as a composition of liftable identities
+
+The runtime of PR5413 is the controller `NEUTRAL-CALLER-v16c` with eighteen backward calls of the body
+`NEUTRAL-BACKWARD-v16c`, whose `PROVIDER_5402` is the changed #5383 word with the port wrappers of
+`NORMALIZERS.json`. [verify.py](verify.py) checks the following.
+
+**A. Port binding (896 exact group identities).** For each of the 112 ports and both orientations, the physical
+path operators of the body are, with absolute phase,
+
+    x -> X : D,      y -> Y : D,      y -> X : D C_0,      Q_p := A_y A_x^-1 = C_0,
+
+where `A_role` is the input wrapper followed by the inverse canonical chart of the entrance frame, `O_role` the
+canonical chart of the exit frame followed by the output wrapper, `D` the positive rank-eight Gaussian on axes 1..8
+and `C_0` the positive central Gaussian on axis 0. The backward orientation uses the entrywise-conjugate chart and
+operator semantics of PR5376 `PROVIDER.md`; mixing conventions produces a different element on every port. These
+are statements about elements of `G`, so by consequence 1 they hold at every width: the body is the controller's
+`X = D x - D Q y`, `Y = D y` on every column.
+
+**B. Body endpoint (free-word identity).** The free-word replay of the body with the provider expanded ends with
+every native warp cancelled, the main rows `X_p = Nout_x (Nin_x x_p - Nin_y y_p)` and `Y_p = Nout_y Nin_y y_p`
+carrying only the port wrappers, the 400 autonomous helpers returned as their own input under an alias pair of exact
+signed monomials (318 pure central phases, 82 with an address action; none is the identity) with the recorded exit
+frame reached by their paid climbs, and all seventeen owned fields zero. By consequence 2 this endpoint is the same
+at every width. Combined with A, the body's physical endpoint on main data is exactly `D x - D C_0 y`, `D y`.
+
+The eight mode owners need one more step, because two different operator paths reach them. Each mode's cache SWAP
+moves the provider's transformed cache row into the owner (it holds the source's `-D Z y`), and the body then adds
+the owned field `T = D(S z + Z y)`, computed through one positive `C8` between alias and route monomials. As free
+words the owner has 113 terms: its own input, 56 `y` terms through `C8` and 56 cached `y` terms through the
+provider, which carry no `C8` symbol. The free group cannot see that they cancel, so [verify.py](verify.py) binds
+every symbol to its exact element of `G`: monomials to their literal words, `G` to the positive `C8` on axes
+`0..7`, `Nin_f` to the input wrapper of `f` followed by the inverse canonical chart of its entrance frame, and
+`N_o` to the canonical chart of the recorded mode frame followed by the literal `output_N` word. Charts are read
+in the backward (entrywise conjugate) convention, as for the ports. Summing like elements in `C[G]`, all 448
+pairs of `y` terms cancel and each owner is exactly `C8 z` with coefficient `+1` and absolute phase, which is the
+source proof's `S(-DZy + D(Sz+Zy)) = S D S z = C8 z`. This is an identity in `C[G]`, so it lifts by the Lemma.
+The unconjugated reading leaves all 896 `y` terms, and a sign change in one `output_N` word breaks the
+cancellation; both are checked. (An earlier version of this package dropped the cache row at the SWAP and
+certified `C8(h - Zy)` instead; the review of #5442 found the error.)
+
+**C. Controller (free commutative identity, abelian realization).** The controller's thirty-two bank rows are
+replayed in the free commutative Laurent ring on `Q` and `D_1, ..., D_33` (the semantics of
+`check_wholecaller_v1.py`, no finite-order quotient); the endpoint is the recorded diagonal with exterior
+coefficient `+1`. The plan `WHOLECALLER-PLAN-v1.json` realizes `Q = C_0` on the global central axis 0 and `D_s` as
+the rank-eight Gaussian on the eight private axes of stage `s`; the eighteen private planes are pairwise disjoint
+and disjoint from axis 0, so all realized symbols commute as exact group elements. A polynomial identity in
+commuting invertible variables holds for any commuting invertible assignment, in particular for the tensor powers
+`C_0^{(x) f}` and `D_s^{(x) f}`, which still commute. The sixteen banks whose diagonal carries `Q^{-1}` are
+corrected by the central translation `X_0 = C_0^2`, and `C_0^{-1} X_0 = C_0` is an exact group identity (phase
+included), so every main target is the positive canonical Gaussian with absolute phase at every width. The scalar
+`Q_POWER` events are `X_0^{±1}` (even exponents), and the signed swaps use the fixed scalar `-1`.
+
+**Conclusion.** The complete caller identity of PR5413 is a composition of identities of types 1 and 2, with
+fixed real dyadic coefficients. Each lifts to every positive column multiplicity. This is the algebraic half of
+the retained assumption `native_all_columns` for the selected caller. It does not address the physical half: that
+the lifted operators, spectators and whole-job adapters are realized on the fixed tape at the retained tariff.
+
+## 4. Controls
+
+[verify.py](verify.py) evaluates the four traps of section 2 on dense `2x2` and `4x4` matrices over `Q(i)`: the
+Reynolds-type relation and the scalar phase trap vanish at width one and fail at width two, while the census
+reports three and two distinct elements; exponent two is one element written two ways and vanishes at widths one to
+three; reversed noncommuting factors are distinct elements and already differ at width one. [test_verify.py](test_verify.py)
+rejects: input drift, a wrapper phase mutation, a mixed-convention reading, a leftover native warp in the body
+endpoint, a cache SWAP that drops the cache row, a sign change in one mode output word, an owned field left nonzero, overlapping private planes, a missing `Q_POWER`, and a tampered result.

research/allwidth-caller-certificate/README.md

@@ -0,0 +1,62 @@
+# All-width certificate for the complete selected #5413 caller
+
+**Scoped positive result; no new κ.** The complete caller identity of
+[PR #5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413) holds at every positive column multiplicity,
+and the proof is a census of exact group elements that a small checker verifies. This is target 8 of
+[PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428): compact all-width native identity
+certificates. It discharges the algebraic half of the retained assumption `native_all_columns` for the selected
+caller; the physical half (tape realization of the lifted operators with spectators and adapters at the retained
+tariff) is left explicit and untouched.
+
+## Lemma
+
+For a finite group `G` of exact matrices and fixed coefficients `c_g`,
+
+    sum_g c_g g^{(x) f} = 0 for every f >= 1    <=>    sum_g c_g g = 0 in C[G].
+
+The map `g -> g^{(x) f}` is a group homomorphism, so group identities and free-word identities lift; by Burnside a
+nonzero element of `C[G]` fails at some width. [PROOF.md](PROOF.md) gives the proof and the three consequences
+used. The census replaces the finite width cutoffs of [PR5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369)
+and [PR5376](https://github.com/CrocSwap/integer-mult-bounds/pull/5376) whenever the elements can be canonicalized,
+which `clifford_exact.py` does (Pauli tableau plus the image of `|0>`, fixing the absolute phase).
+
+## What [verify.py](verify.py) certifies
+
+| Layer | Identity | Count | Lifts because |
+|---|---|---|---|
+| Ports | `x->X = D`, `y->Y = D`, `y->X = D C_0`, `Q_p = C_0`, both orientations, absolute phase | 896 | group identities |
+| Body | free-word endpoint of `NEUTRAL-BACKWARD-v16c` with `PROVIDER_5402` expanded: all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under exact signed alias monomials (318 pure phases, 82 with address action) in their recorded exit frames, 17 owned fields zero; the 8 mode outputs are `C8 z`: their 448 cached provider `y` terms cancel the 448 `y` terms through `C8` element by element | 649 rows | free-word identity; modes in `C[G]` |
+| Controller | Laurent replay in free commuting `Q, D_1..D_33` reproduces the diagonal; 18 private planes disjoint and disjoint from axis 0; `C_0^2 = X_0`, `C_0^-1 X_0 = C_0`, `[C_0, D] = 0` exact | 32 banks | commutative identity, abelian realization |
+
+Backward uses the entrywise-conjugate semantics of PR5376 `PROVIDER.md`. Reading the backward wrappers against
+unconjugated charts gives a different element on every port (port 0: `-C_0^-1 Z_1 Z_2`), so the convention is part
+of the certificate.
+
+Controls on dense `Q(i)` matrices: the Reynolds-type relation `C_0 = (1+i)/2 I + (1-i)/2 X_0` and the scalar trap
+`i = iI` vanish at width 1 and fail at width 2 while the census counts three and two distinct elements; exponent two
+(`C_0^2 = X_0`) is one element and lifts; reversed noncommuting factors differ already at width 1.
+[test_verify.py](test_verify.py) rejects ten mutations, including a cache SWAP that drops the cache row (the error of
+an earlier version, found in the review of this PR) and a sign change in one mode output word.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/allwidth-caller-certificate
+```
+
+`verify.py` runs in about 40 seconds with the standard library. `RESULT.json` is rebuilt and compared.
+
+## Open next questions
+
+- The physical half of `native_all_columns` for this caller: can the distinct exact group elements used (wrappers,
+  `D`, `C_0`, `X_0`, the plan's `J` routes) be reduced to a finite list of fixed-tape primitives whose cost at width
+  `f` is the retained tariff? This is target 10 of PR #5428, not a symbolic certificate.
+- The same census for the forward body (`NEUTRAL-FORWARD-v16c`, review only; it does not run in the selected
+  controller).
+
+## Not claimed
+
+No new κ, no selected-record change, no physical tape implementation, no independent human or kernel review.
+Credit: PR5413 (Clear1nsight), PR5402 (dillona), PR5383/PR5398 (aliromman), PR5369/PR5376 (aliromman) for the
+width-cutoff theorems and the orientation semantics, the Clifford compiler lineage, and PR5428 (zxv) for the target.
+Prepared with substantial Claude Code assistance.

research/allwidth-caller-certificate/RESULT.json

@@ -0,0 +1,71 @@
+{
+ "body_endpoint": {
+  "autonomous_helpers": 400,
+  "block_monomials_identity": 448,
+  "distinct_warp_symbols": 72,
+  "exit_frames_recorded": 632,
+  "helper_alias_pairs_pure_phase": 318,
+  "helper_alias_pairs_with_address_action": 82,
+  "main_rows": "X_p = Nout_x(Nin_x x_p - Nin_y y_p), Y_p = Nout_y Nin_y y_p on all 112 ports",
+  "mode_outputs": {
+   "cached_terms": 448,
+   "cancelled_y_pairs": 448,
+   "free_word_terms": 904,
+   "output": "C8 z on all 8 modes (positive C8 on axes 0..7, absolute phase)",
+   "paid_C8_terms": 456,
+   "y_terms_left": 0
+  },
+  "owned_zero": 17,
+  "warps_cancelled": true
+ },
+ "conclusion": "The complete #5413 caller identity is a composition of (i) a free-word identity of the body whose 8 mode outputs reduce to C8 z in C[G] once the cached provider path and the paid C8 path are bound to exact elements, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.",
+ "controller": {
+  "central_axis": 0,
+  "group_identities": [
+   "C_0^2 = X_0",
+   "C_0^-1 X_0 = C_0",
+   "[C_0, D] = 0"
+  ],
+  "laurent_endpoint": "diagonal, exterior coefficient +1, no finite-order quotient",
+  "negative_q_banks": 16,
+  "private_axes_disjoint": true,
+  "q_power_exponents": [
+   -2,
+   2
+  ],
+  "stages": 18
+ },
+ "lemma": "sum_g c_g g^{(x)f} = 0 for all f >= 1  <=>  sum_g c_g g = 0 in C[G]; group identities lift by g -> g^{(x)f}",
+ "lemma_controls": {
+  "exponent_two": {
+   "same_element": true,
+   "widths_zero": [
+    true,
+    true,
+    true
+   ]
+  },
+  "reversed_factors": {
+   "same_element": false,
+   "width1_zero": false
+  },
+  "reynolds_trap": {
+   "distinct_elements": 3,
+   "width1_zero": true,
+   "width2_zero": false
+  },
+  "scalar_phase_trap": {
+   "distinct_elements": 2,
+   "width1_zero": true,
+   "width2_zero": false
+  }
+ },
+ "port_bindings": {
+  "backward_semantics": "entrywise conjugate charts and operators (PR5376 PROVIDER.md); the mixed reading differs from C_0 on all 112 ports",
+  "group_identities": 896,
+  "symbols": {
+   "D": "fourier on axes 1..8 (positive rank-eight Gaussian)",
+   "Q": "C_0 (positive central Gaussian, axis 0)"
+  }
+ }
+}

research/allwidth-caller-certificate/SOURCES.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json",
+      "usage": "input",
+      "git_blob": "04c6c7f36cb1b9fcf0b464bad3d3d83aaae7c864",
+      "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json",
+      "usage": "input",
+      "git_blob": "975714d0c15714070b2303ca48d31871f2095210",
+      "sha256": "1f17fda221bc781ca0b2a120916ed500ba84c305a916a65436a5d6c72d116bcf"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json",
+      "usage": "input",
+      "git_blob": "b868fe46ce7ff96a51f7b612758685a23014d31d",
+      "sha256": "a02e79fb4615f4f987e3b3617c2b42eea2c1d7415cc66fa702a8b0cd28e6387e"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json",
+      "usage": "input",
+      "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455",
+      "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e",
+      "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc"
+    },
+    {
+      "path": "research/eight-owned-relations/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7",
+      "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b"
+    },
+    {
+      "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    }
+  ]
+}