Record the ordinary bill of the witness F1=Q, F2=C1 Q

research/two-edge-witness-bill/PROOF.md

@@ -0,0 +1,214 @@
+# Ordinary bill of the witness `F1 = Q`, `F2 = C1 Q`
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+No new κ is claimed. The selected frontier is unchanged. No call is added.
+
+## The pair and the owned bank
+
+The published feed in
+[research/coded-active-feedback](../coded-active-feedback/PROOF.md) saves the
+first FULL output `h`, adds `I · h` into query 2, and adds `C1 Q^2` times
+that response into query 4. One extra owned 112-field bank holds `h` and is
+later reset and reused for the response. The witness uses that same bank
+and the same two insertion points. It replaces the two operators by
+`F1 = Q` and `F2 = C1 Q`. Both lie outside the 8,281-policy family. First-edge choices are scalars
+times alternating `C1`/`C3` words, and `Q` is not one of those words.
+Every nonzero second-edge choice ends in `Q^2`, and `C1 Q` does not. This
+note does not re-prove the one-edge obstruction. It prices this pair.
+
+Rightmost operators act first. `Q^4 = I`, `C1^2 = C3^2 = I`, and each `D`
+commutes with `Q` and with the other `D`, while `D_s` conjugates only `C_s`
+by `Q^{-1}`. The verifier checks the four conjugations below.
+
+## While the bank holds `h`
+
+The pinned replay, and the conjugations just named, give the saved bank
+
+```text
+h = [Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0]
+```
+
+and the pair-0 X bank at query 2
+
+```text
+X = [0, -C1 Q D1, D1, 0].
+```
+
+`I` leaves `h` unchanged. Left multiplication by `Q` cancels the leading
+`Q^{-1}` on the two `C1` columns:
+
+```text
+Q h = [C1 D1, Q D1, -C1 D1, 0].
+```
+
+The two images differ on `x0`, `y0`, and `x1`. The query-2 arguments are
+`C1 X + F1 h`.
+
+```text
+C1 X + h     = [Q^{-1} C1 D1, D1 - Q D1, C1 D1 - Q^{-1} C1 D1, 0]
+C1 X + Q h   = [C1 D1, 0, 0, 0].
+```
+
+The two cancelled columns are the identities `C1(-C1 Q D1) + Q D1 = 0` and
+`C1 D1 + Q(-Q^{-1} C1 D1) = 0`. The witness argument is one monomial. The
+published argument is not. The paid response is `Q^{-1}` times the
+argument, so the witness writes
+
+```text
+r2 = [Q^{-1} C1 D1, 0, 0, 0]
+```
+
+into the reused bank. The published response, on this same bank after
+`F1 = I`, is
+
+```text
+[Q^2 C1 D1, -D1 + Q^{-1} D1, Q^{-1} C1 D1 - Q^2 C1 D1, 0].
+```
+
+## While the bank holds the response
+
+On the witness response,
+
+```text
+C1 Q · r2   = [D1, 0, 0, 0]
+C1 Q^2 · r2 = [C1 Q C1 D1, 0, 0, 0].
+```
+
+Only the witness operator returns `D1`. On the published response the same
+two operators differ on `x0`, `y0`, and `x1`. The predecessor identity
+`query4:3 = [0, 0, X1, 0] + Q^{-1} F2 r2`, with
+`X1 = Q^{-1} C3 D1 D3`, therefore gives the autonomous row
+
+```text
+[D1 Q^{-1}, 0, X1, 0]
+```
+
+for this pair and not for `C1 Q^2` on the same `r2`. The query adds that
+response into bank 1. Bank 1 still holds `h`, whose `x0` column equals
+`r2`, so the sum is
+
+```text
+[2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0].
+```
+
+The coefficient `2` is that sum. It is not a second addition and not a
+second owned bank.
+
+## Ordinary bill
+
+The ledger uses the predecessor's published units: one F-transpose is
+896 scalar ADDs, 224 monomial passes and 16 mode CLEARs; one 112-field
+addition is 112 ADDs; one capture is 112 COPYs; one reset of the saved
+bank is 112 field resets; one uniform power of `Q` or `Q^2` is 112
+monomial passes. `Q` overwrites the saved copy of `h` before that copy is
+added. The schedule does not read the unmultiplied copy again, so no third
+capture is charged. Zero columns are not discounted. Maps are not fused.
+
+| Added operation | Published `I`, `C1 Q^2` | Witness `Q`, `C1 Q` |
+| --- | ---: | ---: |
+| Two feedback additions | 224 ADDs | 224 ADDs |
+| One F-transpose, the `C1` in `F2` | 896 ADDs, 224 monomials, 16 CLEARs | same |
+| Monomial on saved `h` | none (`I`) | `Q`: 112 monomials |
+| Monomial on the saved response | `Q^2`: 112 monomials | `Q`: 112 monomials |
+| Captures of `h` and `r2` | 224 COPYs | 224 COPYs |
+| Initial, intermediate and final reset | 336 resets | 336 resets |
+| Extra owned capacity | 112 fields and 8 modes | same |
+| Gaussian children | 0 | 0 under this unit |
+
+The witness therefore pays 1120 scalar ADDs, 448 monomial passes, 16 mode
+CLEARs, 224 COPYs and 336 resets. The published feed pays the same totals
+except 336 monomial passes. The difference is one `Q` on `h`. The response
+line changes from `Q^2` to `Q` and keeps the count 112.
+
+This is an upper bound for that circuit under those units. It is not a
+minimum, not a tape cost, and not a new κ. The same unit was used for `Q`
+and `Q^{-1}` in
+[research/owner-indexed-y0-clearance](../owner-indexed-y0-clearance/PROOF.md),
+which left the primitive open. If one power of `Q` is a Gaussian child, or
+must be expanded before it is a monomial pass, the witness line
+"Gaussian children: 0" is false and 448 undercounts. That alternative is
+not settled here.
+
+## The scalar suffix
+
+After query 4 the schedule executes only the existing scalar suffix:
+add bank 0 into bank 2, subtract bank 3 from bank 1, swap banks 0 with 1
+and 2 with 3 while negating the outgoing banks, then add bank 2 into bank 0
+and subtract bank 1 from bank 3. For arbitrary banks `A, B, C, D` the
+composition is
+
+```text
+final = (B, -A, D, -C).
+```
+
+The bridge terms cancel for every content. The suffix is a signed
+permutation of the four query-4 banks. It clears a final bank to a target
+only when the corresponding preimage is already that signed target. It
+does not multiply by `Q`, `C1`, or `C3`, and it does not cancel a nonzero
+column against a different column.
+
+The witness preimages are bank 1 after the response sum, the pure y0 row
+`[0, -C1 Q D1, 0, 0]`, the autonomous row, and the FULL3 X bank. None is
+the signed uncoded target. The final banks are therefore
+
+```text
+bank 0 = [2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0]
+bank 1 = [0, C1 Q D1, 0, 0]
+bank 2 = [D1 Q^{-1}, 0, Q^{-1} C3 D1 D3, 0]
+bank 3 = [C3 C1 D1 D3, C3 Q D1 D3, -D1 D3, C3 Q D1 D3].
+```
+
+Bank 1 is the same pure y0 monomial as in the published feed. Bank 2 is
+the autonomous row, so its y0 and y1 are zero and its x0 and x1 are not.
+Bank 0 has three nonzero columns, and its x0 coefficient is 2. Bank 3 has
+four nonzero columns, with `y0 = y1 = C3 Q D1 D3`. The uncoded targets are
+`D1 Q^{-1}`, `D1 Q`, `D1 D3 Q^{-1}`, and `D1 D3 Q` on the diagonal. No
+final bank equals its target.
+
+The FULL3 shape of bank 3 is the same conjugation family. Before the left
+`D3`, bank 2 is `-Q C3` times the post-bridge bank 3, plus the carried
+`D1` on x1. Then
+
+```text
+D3 Q C3 D1           = C3 Q D1 D3
+D3 Q C3 Q^{-1} C1 D1 = C3 C1 D1 D3,
+```
+
+and `D3` commutes with `D1`. Negating that bank is final bank 3.
+
+Halving bank 0 does not produce target 0. Left multiplication of bank 3 by
+`C3` turns y1 into `Q D1 D3` and also turns y0 into that same monomial, so
+it is not target 3. Neither operation is part of the suffix.
+
+## No word-free combination hits a target
+
+A rational linear combination of the four final banks, with no extra
+monomial, is the largest word-free scalar operation on these banks. It
+still uses no new call. The target monomials are disjoint from this
+support, except for one inseparable pair:
+
+- Target 0 is the single key `Q^{-1}` on x0 at D-exponent `(1, 0)`. That
+  key occurs only as bank 2's x0 column. Bank 2's x1 column is
+  `Q^{-1} C3 D1 D3`, and that key occurs nowhere else. The coefficient
+  that copies target 0 also copies the x1 monomial.
+- Target 1 is `Q` on y0 at D-exponent `(1, 0)`. No final column contains
+  that key.
+- Target 2 is `Q^{-1}` on x1 at D-exponent `(1, 1)`. No final column
+  contains that key.
+- Target 3 is `Q` on y1 at D-exponent `(1, 1)`. No final column contains
+  that key. Bank 3's y1 key is `C3 Q`, not `Q`.
+
+The domain of this statement is these four banks and these four targets.
+Every one of the sixteen columns was inspected for each key. This is not
+a census of feedback pairs, and it does not forbid a monomial multiplier
+or a read of an earlier bank.
+
+## What is not proved
+
+The witness is one pair. The formal algebra is the predecessor's sufficient
+identity model. A quotient that collapses one of these words could make the
+same banks look cheaper; no such quotient is proved here. Native tape,
+precision, compiler, and outer costs are not repriced. The x1 block of the
+published feed and a saved-bank source other than this response are not
+taken. The selected conditional κ, `781451/250000000`, is not changed.

research/two-edge-witness-bill/README.md

@@ -0,0 +1,132 @@
+# The two-edge witness pays 112 extra monomial passes, and the scalar suffix clears no final bank
+
+**Scoped bill and suffix identity; no new κ.** On the one reused owned
+bank of
+[research/coded-active-feedback](../coded-active-feedback/README.md), the
+witness `F1 = Q`, `F2 = C1 Q` replaces the published `I` and `C1 Q^2`.
+Under the predecessor's uniform field units the witness pays one extra
+`Q` on the saved FULL output, 112 monomial passes, and changes the
+response monomial from `Q^2` to `Q` at the same 112-pass count. The
+existing scalar suffix is a signed permutation of the four query-4 banks.
+It clears none of them to an uncoded target. Final banks 0 and 3 stay the
+explicit nonzero rows below.
+
+The selected frontier is unchanged. This does not re-prove the one-edge
+coupling of
+[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md).
+
+## Result
+
+`Q` and `I` disagree on three columns of the common saved bank
+
+```text
+h = [Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0].
+```
+
+`Q h` cancels the query-2 argument down to the single monomial `C1 D1`.
+`C1 Q` then returns `D1` on that response. `C1 Q^2` on the same response
+returns `C1 Q C1 D1`.
+
+The additional ledger, with each uniform power charged as 112 monomial
+passes, is 1120 scalar ADDs, 448 monomial passes, 16 mode CLEARs, 224
+COPYs, 336 resets, 112 owned fields and 8 reused mode fields. The
+published feed pays 336 monomial passes and the same other totals. No
+Gaussian child is charged while `Q` uses that monomial unit. The unit is
+not a tape proof.
+
+After query 4 the suffix sends banks `(A, B, C, D)` to `(B, -A, D, -C)`.
+The witness finals are
+
+```text
+bank 0 = [2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0]
+bank 1 = [0, C1 Q D1, 0, 0]
+bank 2 = [D1 Q^{-1}, 0, Q^{-1} C3 D1 D3, 0]
+bank 3 = [C3 C1 D1 D3, C3 Q D1 D3, -D1 D3, C3 Q D1 D3].
+```
+
+Bank 1 matches the published pure y0 monomial. Banks 0 and 3 do not match
+the published feed or their uncoded targets. No rational word-free
+combination of these four banks hits any of the four targets: the only
+target monomial present is bank 2's restored `D1 Q^{-1}`, and it is tied
+to the x1 monomial `Q^{-1} C3 D1 D3`. [PROOF.md](PROOF.md) gives the
+cancellations, the ledger, and the support check.
+
+Evidence class: the operator comparison, the suffix identity, and the four
+final rows are proofs in the predecessor's formal algebra. The word-free
+miss is a complete support check of these sixteen columns, not a search
+and not a census of other pairs. The ledger is an upper bound under
+inherited units.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3 -B scripts/research_package.py --package research/two-edge-witness-bill --check-only
+python3 -B scripts/research_package.py --package research/two-edge-witness-bill
+```
+
+Direct replay:
+
+```sh
+python3 -I -W error -B research/two-edge-witness-bill/verify.py
+python3 -I -O -W error -B research/two-edge-witness-bill/verify.py
+```
+
+The optimized command still executes the checks. They are `need` failures,
+not assertions. Allow a few seconds. No network, native build, or full
+multiplier replay is used.
+
+## Scope
+
+Original card: `joint-query-controller`. Scope status: **refined**. The
+card asks whether one changed caller removes real work. This package does
+not change the query demand and does not add a call. It takes the first
+open question of
+[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md):
+compare `Q` and `C1 Q` with the published `I` and `C1 Q^2` on the same
+owned bank, then read final banks 0 and 3.
+
+Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in
+[SOURCES.json](SOURCES.json). The catalogue and selected record are
+provenance. The selected conditional result remains
+`781451/250000000`. `search.py` and `gauge.py` are live inputs.
+
+Local overlap at this base found the witness named only as that open
+question. The one-edge theorem, the owner-indexed y0 charge, and the
+owner-indexed x1 obstruction are different objects and are not redone.
+
+## Open next questions
+
+Does one source monomial primitive implement a single power of `Q` at the
+same 112-pass unit as `Q^2`? The witness bill charges two such powers, one
+on `h` and one on the response, and its zero Gaussian-child line is false
+if either power is a Gaussian child. The first step is to bind that
+primitive for one `Q` on one 112-field bank and reprice those two lines.
+No native word is replayed here. This is the primitive left open by the
+owner-indexed y0 charge, now used twice.
+
+Can one charged monomial, still with no new call, turn final bank 0 or
+final bank 3 into its uncoded target while bank 2 stays the autonomous
+row? Word-free rational combinations cannot. The first step is one left
+monomial on bank 0 or bank 3, charged at 112 passes, checked against that
+target and against bank 2. This is not the published-feed x1 owner index
+and not a new saved-bank source.
+
+## Credit
+
+The schedule, algebra, owned-bank lifetime, and field units are Cinna
+Davis's `research/coded-active-feedback`, using Dugongue's PR4948
+chronology, Dillon's PR4933 code, and the passive ceiling packaged by
+Chris R / Clear1nsight. The gauge engine remains the inherited
+`research/coded-native-caller/gauge.py`. The witness pair and the one-edge
+identities are
+[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md).
+The monomial unit for one power of `Q` is the convention in
+[research/owner-indexed-y0-clearance](../owner-indexed-y0-clearance/README.md),
+whose primitive question stays open. New work is the owned-bank comparison,
+the witness ledger, the suffix identity, and the support check for banks
+0 and 3.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance.
+Apache-2.0.

research/two-edge-witness-bill/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/coded-active-feedback/search.py",
+      "usage": "input",
+      "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e",
+      "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6"
+    },
+    {
+      "path": "research/coded-native-caller/gauge.py",
+      "usage": "input",
+      "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167",
+      "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad"
+    }
+  ]
+}