Audit #6114's controller income bound: theorem holds, two proof gaps closed, 'only escape' scope corrected (no new κ)

research/p104-controller-income-audit/PROOF.md

@@ -0,0 +1,83 @@
+# Audit of PR6114: controller income bound
+
+Audited: PR #6114 (Matarener), head `3183c6553e5559df8807fde4fec27e2403f3040a`,
+`research/p104-controller-income-bound/PROOF.md`, against the literal alphabet of
+`research/p104-productive-controller/caller.py` on main `721c03822`.
+
+**Verdict.** The theorem is correct as stated for the literal alphabet: with a constant invertible right
+boundary, `s` paid odd shears and `n_odd` outputs with zero even part, `n_odd ≤ s − 1`. The three retained
+controllers attain it (33 shears, 32 twisted outputs, income 17 = 18 − 1); an independent engine reproduces every
+number. There are two gaps in the written argument, both closable (A1, A2), and a cosmetic error (A3). The scope sentence
+"a paid primitive that touches several banks or ports at once ... is the only way to escape the bound" is
+overstated: one-bank paid primitives and non-constant boundaries also escape, while multi-source jobs that write
+a single row do not (A4).
+
+Notation as in PR6114: every bank row is `a + Q·b` with `a, b ∈ R_even^n`, `R_even = ℚ[Q^{±2}] ⊗ ℚ[D_0, …, D_32]`;
+`E` is the matrix of even parts and `B` the matrix of odd coefficients, so the state is `M = E + Q·B`.
+
+## A1. The left boundary (gap in step 4 / the theorem's last inequality)
+
+PR6114's PROOF.md says that the left boundary is applied at the end. It then uses "the `n_odd` zero rows give
+`rank E_final ≤ n − n_odd`". But the zero rows belong to `L·M`, not to `M`. The repair below does not need `L`
+to be invertible. Let `T` be the set of twisted outputs and `L_T` the corresponding rows of the constant matrix
+`L`. The even part of `L_T·M` is `L_T·E = 0`, so the rows of `L_T` lie in the left kernel of `E`. The outputs
+`Q^{±1}D^{S_i}e_i` (`i ∈ T`) are linearly independent, so `rank L_T ≥ rank(L_T M) = |T|`. Hence
+`n − rank E ≥ |T|`. On the literal words `L` is invertible anyway (checked).
+
+## A2. Lift cancellation (unproved step of the invoice consequence)
+
+The consequence `income = Σ_i (1 + d|S_i|) − d·lifts − n_thin = n_out − n_thin` needs `Σ_i |S_i| = lifts`.
+PR6114 asserts this ("every stage that appears in an output was paid once as a lift"). That assertion is
+true, and it follows from the determinant for every word whose outputs form the full monomial diagonal.
+Scalar `ADD`, swaps and shears have determinant `±1`, `Q_POWER` multiplies the determinant by `Q^{±2}`, and a
+lift of row `r` by `D_s` multiplies it by `D_s`. So `det(L·M_final) = c·Q^{2k}·∏_s D_s^{ℓ_s}`, with `c ∈ ℚ^×` and
+`ℓ_s` the number of row-lifts at stage `s`. For each output `i`, `S_i` is its stage set. The diagonal
+`diag(Q^{q_i}D^{S_i})` has determinant `∏ Q^{q_i} ∏_s D_s^{#{i : s ∈ S_i}}`, and `ℚ[Q^{±1}, D]` is a UFD. Hence
+`#{i : s ∈ S_i} = ℓ_s` for every stage `s`, and `Σ_i q_i = 2k`. The verifier checks both identities stage by
+stage on all three controllers (`Σ|S_i| = 194` lifts, net `Q_POWER` = `Σ q_i`). If a word twists only some of its
+outputs, this argument does not apply, and the consequence needs the untwisted outputs' targets to be stated.
+The physical cost model in `caller.py` accepts only odd diagonal outputs.
+
+## A3. Cosmetic
+
+The stage markers are `D_0, …, D_32` (33 of them; `caller.py` exponent tuples have 1 + 33 entries). They are not
+`D_0, …, D_33`.
+
+## A4. Which paid primitives escape
+
+Write a paid job as `M ← A·M` with `A = A_e + Q·A_o` (`A_e, A_o` over `R_even`). Then the new even part is
+`E' = A_e·E + Q²·A_o·B`. Sylvester's rank inequality gives
+
+    rank E' ≥ rank E − (n − rank A_e) − rank A_o ,     and, if B = 0,   rank E' ≥ rank E − (n − rank A_e).
+
+Free events have `A_o = 0` and invertible `A_e`, so they preserve `rank E` and keep `B = 0` before the first paid
+job. With a constant invertible entry this gives
+
+    n_odd ≤ (n − rank A_e^(1)) + Σ_{k ≥ 2} [(n − rank A_e^(k)) + rank A_o^(k)] .
+
+PR6114's open question 1 asks for this bound ("twisted ≤ sum over paid jobs of their even-rank change"), and the
+formula above computes it from the job matrices alone. Consequences:
+
+* **Positive (generalization).** A paid job that writes one row, `y ← u·y + Σ_{j≠y} f_j·x_j`, has `A_e`
+  invertible and `rank A_o ≤ 1` when `u ∈ R_even` is nonzero. This holds for any number of source banks and any
+  Laurent coefficients `f_j`. Such jobs obey PR6114's bound exactly, including the `− 1`. Touching several banks is
+  therefore not by itself an escape.
+* **Escape 1: an odd one-bank job.** A paid odd translation `y ← Q·y` has `rank A_e = n − 1` and twists one output
+  even as the first job. So `s` such jobs can twist `s` outputs, which is one more than the bound. Control:
+  one job, one odd row.
+* **Escape 2: a non-constant boundary.** If the entry rows already carry odd content, step 3 fails. Control
+  (2 banks): entry `x = e1 − Q·e2`, `y = e2`, then `y += Q^{-1}x` and `x += −Q·y` give the odd rows `−Q·e2`
+  and `Q^{-1}·e1`. That is 2 twisted outputs from 2 shears. The entry is one backward shear of the identity, so
+  a Laurent boundary can hide a paid shear. With a general entry the bound is `n_odd ≤ (n − rank E_entry) + s`.
+* **Escape 3: a job that writes several rows.** This is the case PR6114 names. Control: the 2×2 composite of the
+  three Whitehead shears, taken as one paid job, drops the even rank by 2 from a constant entry.
+
+Within the literal alphabet (rational boundary programs, `Q_POWER ∈ {±2}`, one-pair shears with coefficient
+`Q^{-1}` or `−Q`) none of these escapes is available, so PR6114's theorem and its 17 = 18 − 1 conclusion stand.
+
+## Not audited
+
+The surplus formula `M = v·income − n_thick·c` and the value `c = 56` on the PR5907 word (`760`) were not
+rechecked against an invoice. The choice of rank mass rather than the moment as the objective was not audited
+either; PR6114 itself defers the moment to PR5554 and `research/fragmentation-ceiling`. The random one-destination
+test supports the A4 positive case, and the A4 proof is the evidence for it.

research/p104-controller-income-audit/README.md

@@ -0,0 +1,72 @@
+# Audit of PR6114's controller income bound
+
+**Independent adversarial audit; no new κ; the selected record is unchanged.**
+
+[PR #6114](https://github.com/CrocSwap/integer-mult-bounds/pull/6114) (Matarener, head `3183c655`) proves a
+theorem about the literal p16 Laurent caller alphabet of
+[`research/p104-productive-controller/caller.py`](../p104-productive-controller/caller.py). Starting from a
+constant invertible boundary, a caller word with `s` paid odd shears (`LOCAL`, `QUERY_SHEAR`) twists at most
+`s − 1` outputs. So the controller income per port is at most `thick calls − 1`, and the three retained controllers
+attain this (17 = 18 − 1). This package checks that theorem independently.
+
+## Result
+
+* **The theorem holds** for the literal alphabet. I re-derived the proof, and a separate engine reproduces every
+  number. That engine is written here without importing `caller.py` or PR6114's code. It runs an exact symbolic
+  Laurent replay of all three controllers to the declared odd diagonal. It also tracks the even-part rank after
+  every event under a different specialization: `Q² → 13/7, 19/11`, with random nonzero stage values where
+  PR6114 sets `D_s → 1`.
+
+  | Controller | thick + thin | twisted | even-rank trace | lifts = Σ\|S_i\| | income |
+  |---|---:|---:|---|---:|---:|
+  | `kappa-backward-controller-20261023` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 |
+  | `joint-helper-lattice` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 |
+  | `p104-productive-controller` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 |
+
+* **Two gaps in the written proof, both closed** ([PROOF.md](PROOF.md) A1–A2). First, the last inequality uses
+  zero rows of `L·M`, not of `M`. A left-kernel argument repairs it, and `L` need not be invertible. Second, the
+  invoice step "every output stage was paid once as a lift" was asserted, not proved. It follows from the
+  determinant, stage by stage, for every word whose outputs form the full monomial diagonal. The verifier checks
+  all 33 stages and the central exponent on each controller.
+* **The scope claim needs correcting** (A4). PR6114 says a paid primitive touching several banks or ports is
+  "the only way" to beat the bound. For a paid job `A = A_e + Q·A_o`, Sylvester's inequality bounds the even-rank
+  drop by `(n − rank A_e) + rank A_o`. When no odd content exists yet, the bound is `n − rank A_e`. From that:
+  * Every paid job that writes **one** row `y ← u·y + Σ f_j·x_j` obeys PR6114's bound exactly, including the
+    `− 1`. This needs the self-coefficient `u` to be nonzero and even. The sources can be any number of banks,
+    and the `f_j` can be any Laurent coefficients.
+  * Three escapes exist, each with an exact control: a paid **one-bank** odd translation `y ← Q·y` (1 twist from
+    1 job); a **Laurent entry boundary** (2 twists from 2 shears); and a **two-row** job (2 twists from 1 job).
+    None of them is in the literal alphabet, so PR6114's conclusion stands.
+
+Not audited: the surplus formula `M = v·income − n_thick·c` and `c = 56`/`760` on the PR5907 word, and the
+moment side.
+
+## Reproduce
+
+```sh
+python3.12 -B research/p104-controller-income-audit/verify.py
+python3.12 -B scripts/research_package.py --package research/p104-controller-income-audit
+```
+
+The run takes under a second and uses only the standard library. Engine: [audit.py](audit.py). Evidence:
+[RESULT.json](RESULT.json), compared in full. The random one-destination words (n = 2, 4, 6; 3,909 paid jobs)
+never exceed the bound. In 41 of them the even-rank deficit `n − rank E` equals `s − 1`. This counts the rank
+deficit only; the test builds no twisted outputs. They support the A4 proof and do not replace it.
+
+## Open next questions
+
+1. **Can Escape 1 or 2 be realized physically at the P104 caller?** A legal paid odd translation `Q^{±1}`, or a
+   supplier boundary that already carries odd content, would lift the cap from `thick − 1` to `thick` per port.
+   That is up to 104 rank units on the PR5907 word, before the primitive's own charge is paid. First step: price
+   `Q^{±1}` as a native job in the terms of `caller.py`'s `physical()`. Blocker: the literal alphabet rejects it
+   as a free event, and no native realization is known here.
+2. **What twist capacity do the available multi-row paid jobs have?** For any candidate job, compute
+   `(n − rank A_e, rank A_o)` before searching, and compare the result with its paid rank. Blocker: there is no
+   priced inventory of multi-bank primitives.
+
+## Credit
+
+PR6114 and its theorem: Matarener (prepared with Claude). The retained controllers come from Cinna Davis (p16/a7
+lattice) and Ali Romman (PR5398 replay, all-forward wrapper). The binary predecessor theorem is Cinna Davis's
+`research/productive-controller-basis-search`. Audit by Josie Elliston, prepared with Claude Code (Opus 5.5).
+Apache-2.0.