Price the register-333 K/adjoint round trip as Z_256.

research/k-adjoint-boundary-price/PROOF.md

@@ -0,0 +1,92 @@
+# One K/adjoint round trip on register 333
+
+## Pinned boundary
+
+PR #4002 freezes forty recipe descriptors and sixteen warps on four binary
+maps. One of those maps is the credited source witness
+
+```text
+G = (1, 2, 8, 32, 44, 128, 59, 66, 489).
+```
+
+The new-version sign-+1 warp with those columns has entrance
+`(266, 138, 74, 30, 1)`, terminal `(426, 96, 24, 6, 1)`, and coverage rows
+for providers `base` and `extra` at register `333`, index `4`. The matching
+sign-−1 descriptor swaps that entrance and terminal. This package prices that
+pair and no other warp.
+
+## Operators
+
+Columns are images of the standard basis. Write `P_G|x> = |Gx>`,
+`Z_t|x> = (-1)^{t·x}|x>`, and `D|x> = i^{wt(x)}|x>`. The source canonical
+lift and the normalized section are
+
+```text
+K_G|x> = i^{q(Q_G)(Gx)}|Gx>,
+J_G|x> = i^{wt(Gx)-wt(x)}|Gx>,
+Q_G = I + G^{-T} G^{-1}.
+```
+
+The quadratic value is the source polar form modulo 4. PR #4002 proves
+`K_G = J_G Z_{t_G}` with
+
+```text
+(t_G)_j = [q(Q_G)(G e_j) - wt(G e_j) + 1]_4 / 2,
+```
+
+and the cocycle
+
+```text
+K_H K_G = K_{HG} Z_{t_G + G^t t_H + t_{HG}}.
+```
+
+Masks add by XOR. Those identities are used here only for this `G`.
+
+## The round trip
+
+Direct inversion gives
+
+```text
+G^{-1} = (1, 2, 28, 4, 79, 8, 130, 32, 431),
+t_G = 144, t_{G^{-1}} = 68.
+```
+
+The identity has tag 0, so
+
+```text
+K_{G^{-1}} K_G = Z_{144 + G^t 68} = Z_{256}.
+```
+
+`256 = 2^8`, so the character is the single coordinate sign on bit 8. It is
+not the identity: the states with that bit set, 256 of the 512 addresses,
+pick up phase `2` modulo 4, which is a factor `-1`.
+
+The same permutation round trip under `J` is `J_{G^{-1}} J_G = J_I`. The
+section phase of `J_I` is `wt(x) - wt(x) = 0`. Substituting `J` for `K` on
+this pair therefore deletes `Z_256` and disagrees on those 256 states. The
+binary permutation of either product is the identity, so the deleted object
+is only that central character.
+
+## What the recipe already records, and what it does not
+
+The sign-+1 descriptor stores `phase = 3` and
+
+```text
+linear_Z4 = (1, 2, 2, 0, 2, 2, 3, 2, 2).
+```
+
+That Z4 vector is not the coboundary mask `144`. Paying the published
+`linear_Z4` field does not display `Z_256`, and deleting the coboundary is a
+separate change.
+
+The descriptor's `rank` field is `0`. This note does not read that field as a
+free child. Helper return, routing and tape are absent, so those charges are
+unknown. Unknown charges are not zero. The sign itself is an exact factor
+`±1`, so this boundary adds no further denominator.
+
+The uncompensated `J` pair is consequently not a zero-cost rewrite of the
+`K` pair. This is not a complete supplier invoice, a scalar-addition saving,
+or a change of selected κ.
+
+The old-version descriptors on the same register use the same columns with a
+shorter entrance. They are not part of this pair.

research/k-adjoint-boundary-price/README.md

@@ -0,0 +1,76 @@
+# Price of one K/adjoint round trip
+
+**Partial ledger. No new κ.** Selected conditional κ stays
+`0.001672660197076918`.
+
+## Scope and evidence
+
+Original card: `independent-moment`, scope **changed**. The card asks for an
+independent check of one changed supplier claim and its physical ledger. The
+session handoff is the unpaid physical boundary in discussion #1166 comment
+19036235, left by PR #4002. The catalogue method used is that card's frame
+reconstruction: one coordinated substitution and its single-change control.
+
+The pinned boundary is the new-version witness warp on register `333`, index
+`4`, together with the adjoint descriptor that swaps its entrance and
+terminal. Both use
+
+```text
+G = (1, 2, 8, 32, 44, 128, 59, 66, 489).
+```
+
+`K_{G^{-1}} K_G = Z_{256}` and `J_{G^{-1}} J_G = J_I`. The single-change
+control deletes only `Z_{256}`. The binary product stays the identity, and
+256 of 512 states change sign. [PROOF.md](PROOF.md) records the tags
+`t_G = 144` and `t_{G^{-1}} = 68`.
+
+The published `linear_Z4` on the sign-+1 gate is not the mask `144`. Helper,
+routing and tape charges are absent from the descriptor and stay unknown.
+The exact sign adds no denominator. A favorable complete bill is not
+established. No native expansion and no κ change.
+
+`RECIPES.json` is the byte-identical `source/RECIPES.json` from PR #4002 at
+`d593941ea0a4926021cba9d01fe60500579e464f`, SHA256
+`64b85f6aef485026eebaec7acddb41999f57e074b0dfde8077b6543700cd684b`. That
+commit is not required as a Git object in this clone. The checker rejects any
+other bytes. It does not import PR #4002's verifier.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/k-adjoint-boundary-price
+```
+
+Direct check:
+
+```sh
+python3.12 -B research/k-adjoint-boundary-price/verify.py
+```
+
+Expected marker: `PASS_K_ADJOINT_BOUNDARY_PRICE` with
+`central_child=Z_256`, `states_wrong_under_J=256`,
+`favorable_complete_bill=false`, and `new_kappa=false`.
+
+## Open next questions
+
+1. Can `Z_{256}` be absorbed by an adjacent paid gate on register `333`?
+   First step: name the predecessor and successor of index `4` in the
+   PR #3945 schedule and multiply those three operators. Blocked here
+   because this descriptor has no neighboring gates.
+2. What helper, routing and tape tariff does this warp pay in the emitter?
+   First step: read the owner row for register `333` in the PR #3945
+   native inventory. Blocked because those fields are not in `RECIPES.json`.
+
+## Credit
+
+Chris R / Clear1nsight, PR #3987, for the canonical lift and the inverse
+witness. ToikY, PR #4002, for the explicit tag formula, the frozen four-map
+inventory, and the open pricing question. Dugongue, PR #3945 / #3929, and the
+native lineage named in that package, for the recipe convention. The tag
+arithmetic on this one pair was recomputed here and does not import that
+checker.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review is claimed.