Prove and cost one physical inverse-coded FULL/thin pair

research/physical-inverse-pair/README.md

@@ -0,0 +1,94 @@
+# One physical inverse-coded FULL/thin pair
+
+**Scoped exact all-block identity with a charged local recipe; no new kappa or complete caller admission.** Replacing the scalar inverse in PR5036 by the physical inverse does repair one backward FULL / next thin pair, provided its Y entrance and Y exit are also changed. The exit is a real operation: the explicit implementation adds 224 rank-one Gaussian jobs beyond the thin stage's 112. It is not a free gauge.
+
+The exact sources are pinned in [SOURCES.json](SOURCES.json), at canonical base `4c0a359d88f22f05189d51f48387750b801a45d4`, priority revision 7. The assigned claim is [Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19140791). The pair is stages 37/38 of the proposed p19 chronology; no bridge or initial IDLE separates those calls. This package changes the operator and boundary left open by PR5036, rather than repeating its scalar counterexample. It excludes the separately claimed two-stage terminal-code product and all full-controller work.
+
+## Literal four-block theorem
+
+Operators act rightmost first. On the direct sum of 112 arbitrary owner fields let `Q` be the central Gaussian, `D` the product of the eight fresh Gaussian axes, `R=DQ=QD`, and `K=diag(K_i)` the actual PR4933 signed normalizers. Set
+
+```text
+C = K^-1 (A tensor I) K,
+B = diag(D,D) [[I,-QC],[0,I]],
+T = [[I,0],[Q^-1 C^-1,I]],
+E = diag(I,C^-1),       O = diag(I,Q^-1 C Q).
+```
+
+The raw-dual convention is PR4933's actual X-only Q-squared correction. Each real signed K_i commutes with R, hence C and its inverse commute with R. Consequently literal multiplication gives every block, without commuting C through Q or D separately:
+
+```text
+T B = [[D,              -DQ C],
+       [Q^-1 C^-1 D,       0]],
+
+O T B E = [[D,        -DQ],
+           [DQ^-1,      0]].
+```
+
+For the bottom-right block use `Q^-1 C^-1 DQ C = Q^-1 DQ = D`. For the top-right block right-multiplication by C^-1 cancels the final C. For the bottom-left block left-multiplication by `Q^-1 C Q` cancels adjacent `Q Q^-1` and `C C^-1`, giving `Q^-1 D=DQ^-1`. The top-left block stays D. These equations hold on independent arbitrary X and Y, not only on x=0 or a selected source column. The uncorrected pair already cancels its YY block; its YX block is still wrong. A scalar exit C, with the Q conjugation omitted, fails the executable control.
+
+The inherited producer's complete direct-sum endpoint includes 408 autonomous helper operators. E, T's new work and O address only main/query/mode banks. Extend each by identity on the helpers and every unrelated spectator. Block multiplication therefore retains exactly those 408 original independent outputs, with their original requested transforms; it does not identify them with scratch or with unchanged input values. Their physical producer autonomy is the pinned PR4929 premise, not a new native replay here.
+
+## Source signs and every positive width
+
+For one nine-bit column write `K_i=Z_(z_i) P_(G_i)`. On the Walsh character `chi_u(x)=(-1)^(u dot x)`, its inverse maps the frequency to `G_i^T(u xor z_i)`. The Gaussian Q has eigenvalue `i^(u_0)` and R has eigenvalue `i^wt(u)`. The checker independently reads the actual G and z, verifies orthogonality and the actual central port, then checks
+
+```text
+wt(G_i^T(u xor z_i)) = wt(u) (mod 4)
+```
+
+for all 112 owners and all 512 frequencies. This is a complete finite certificate for the actual one-column absolute-phase commutator, not a supplied commutator hypothesis. Omitting the signed Z masks fails. PR4933's written orthogonal weight-congruence derivation supplies the same identity in address coordinates.
+
+For every positive column count f, take `K_i,f=K_i^tensor f`, `Q_f=Q^tensor f` and `D_f=D^tensor f`, with all other coordinates as spectators. The one-column equality tensors, so `[K_i,f,D_f Q_f]=0`. Define `C_f` by its owner entries `A_ij K_i,f^-1 K_j,f`; apply A once across owners, not once per digit column. The scalar program's inverse follows from the exact source relations `A=I-MM^T/4`, `M^T M=56I`, and `A^-1=I-MM^T/52`. Thus the displayed four-block calculation evaluates in the lifted operator algebra for every f. No tensor-of-a-sum substitution occurs.
+
+For independent finite corroboration, a common Walsh frequency tuple defines an invariant 112-owner subspace with physical frequency `v_i=(G_i^T(u_t xor z_i))_t` at owner i. In this chart C is A, while Q and D are genuinely owner-dependent diagonal phases, `q_i=i^(sum_t(v_i,t)_0)` and `d_i=i^(sum_t wt(v_i,t>>1))`. The interpreter executes entrance, backward FULL, changed thin and exit in chronological order and compares with the independent standard-pair endpoint. It tests all 224 X/Y basis columns in eight explicitly recorded width1/2 subspaces, plus mixed inputs. This finite oracle does not enumerate every width-two physical address; the quantified coverage is the preceding tensor/operator proof. All 512 Walsh coefficients of the required physical input x=0, y=owner1/address1 are separately checked. The source witness `C_01|1>=+|22>/2`, versus scalar `A_01|1>=-|1>/2`, still rejects the old scalar recipe.
+
+## Constructive local instruction schedule and complete ledger
+
+The exact rational field program is: (1) on Y apply K, inverse scalar mode code, K^-1; (2) invoke the source backward FULL with its actual normalization; (3) initialize 112 owned query fields, copy X, recode those fields by physical C^-1, apply Q^-1 to each, ADD each result to its distinct Y owner, and erase only those owned query fields; (4) on Y apply Q, physical C, then Q^-1. The query buffers can be released before the exit. Each scalar code first collects all eight modes before overwriting any owner. Its mode workspace is reused across the three recodings. Native helpers are never available as borrowed work.
+
+A Q^-1 job is lowered as one positive rank-one Gaussian Q and its Pauli translation Q^-2; it is not treated as an order-two Gaussian. The source all-column query/job ABI and its internal scratch remain inherited. Exit Q and Q^-1 act on the current Y bank, preserving X; they receive no main-output rank credit. A source job's in-place realization and movement must satisfy that ABI and are not supplied by the linear identity alone.
+
+| Operation | Explicit local charge | Evidence/status |
+| --- | ---: | --- |
+| Backward center-free FULL | `2201 H1 + 412 H2 + 510 H3 + 127 H4 + 40 H5` | Inherited source profile |
+| Original autonomous helper returns | `28 H4 + 7 H7 + 47 H8 + 326 H9` | 408 distinct owners, no scratch or erasure credit |
+| Actual four port wrappers | 448 monomial field maps | Inherited constructive bound |
+| X-only backward conversion | At most 448 monomial maps | Inherited bound, no fusion assumed |
+| Entrance physical C^-1 | 224 K maps, 896 ADDs, 16 owned CLEARs | Exact eight-mode program, coefficient -1/52 |
+| Thin physical C^-1 | 224 K maps, 896 ADDs, 16 owned CLEARs | Same program on owned query copies |
+| Exit physical C | 224 K maps, 896 ADDs, 16 owned CLEARs | Eight-mode program, coefficient -1/4 |
+| Thin owned query bank | 112 initial CLEARs, 112 COPYs, 112 terminal ERASEs | Only owned query fields |
+| Thin Q^-1 plus destination update | 112 H1, 112 Pauli maps, 112 ADDs | Positive Gaussian lowering |
+| Exit Q then Q^-1 | 224 H1, 112 Pauli maps | Q conjugation is explicitly paid |
+
+The complete paid Gaussian profile of this emitted recipe is `{1:2537,2:412,3:510,4:127,5:40}`. It includes 336 added H1 jobs, not merely 112. Its additional explicit scalar ADD count is 2,800 (2,688 recoding ADDs plus 112 destination updates), and the wrapper/query monomial upper bound is 1,792 (448+448+672+224), beyond the native internal word. There are 48 mode CLEARs, 112 query CLEARs, 112 COPYs and 112 terminal ERASEs. Additional field workspace peaks at 120 owned fields: 112 query copies plus eight modes, beyond source native/query internal scratch. These are constructive field-operation upper bounds, not a compiled physical tape tariff or a claim of optimality. Fusion or amortization would need a separately priced replacement word.
+
+Both inverse recodings introduce denominator 13; exit C is dyadic. For N real/imaginary scalar components per owner, the retained PR5037 classical grid kernel implements one scalar inverse within `2*2^-P` component error and charges `N(2898W+5922)+18W+100` transitions, with `W=bit_length(56H+2)+1` for a validated input bound H. Conditional on that kernel's common-coordinate, classical-overwrite ABI, the two calls cost the sum of that expression at their respective H/N values, with all 224 K maps per invocation additional. Its nine word buffers represent the eight modes plus one reusable division buffer at the current scalar coordinate; that additional division word and its scans are already included in the kernel tariff, not counted as nine extra field owners. It cannot be substituted into the exact identity as an exact inverse, and its output error requires propagation through the actual Gaussian/interstage suffix. The kernel is noninjective and does not provide reversible cleanup.
+
+The exact field program has finite local norm bounds: source inverse mode prefixes at most 56 and forward prefixes at most 57; signed K preserves component magnitude. A fixed finite composition of these and actual Gaussian operators yields a finite error-propagation constant. Selecting a global precision and funding that constant is still a caller obligation. Native ordinary arithmetic (including the retained 6,596 dyadic compensation ADDs), matching, routing, field movement, query-internal work, denominator rounding, and compiler/outer error funding remain inherited or explicitly unknown nonzero costs. There is no claimed complete bit/tape invoice for the physical composition.
+
+## Family decision and remaining obligations
+
+**Finish this local implication; do not expand the p19 construction from it.** The algebraic missing implication is resolved for this changed recipe. The honest recipe has 224 extra boundary H1 jobs compared with the already-charged thin-only alternative, and no evidence here makes those free. Its complete field inventory is known; physical tariff and full-controller affordability are not. A downstream expansion must present a named complete caller allowance and legal interstage boundary composition, or a different explicit costed decoder. A favorable local cancellation is insufficient. The selected conditional kappa `0.00302015` is unchanged.
+
+## Reproduce and validation scope
+
+```sh
+python3.12 -I -B research/physical-inverse-pair/verify.py
+python3.12 -I -O -B research/physical-inverse-pair/verify.py
+python3.12 -B scripts/research_package.py --package research/physical-inverse-pair
+```
+
+The standard-library verifier authenticates every live source input, checks every code entry and the mode Gram matrix, actual signed phases, independent basis/mixed inputs, and the literal physical address fixture. Semantic controls reject an omitted entry recoding, an unconjugated exit, reversed thin operator order, omitted K signs, the old scalar substitution and an attempt to erase helper 17. Assertions are not used for correctness. The all-width proof, source-bound finite certificate, and conditional implementation ledger are different claims. No full native/controller replay, Lean, Docker, production build, physical TM execution, or complete multiplication theorem is claimed.
+
+Test-authoring rationale: the observable contract is the chronological all-block physical pair; plausible regressions are the six listed semantic mutations; predecessors do not test the changed C^-1 recipe with its new Y boundaries; the checker adds no production-only API or test seam.
+
+## Open next questions
+
+1. Can a complete caller afford these boundaries, or can a concrete shared boundary word remove their paid queries? First compare this full field inventory with a named allowance; stop if the optimistic complete bill fails. No two-stage terminal-code product analysis is supplied here.
+2. Can the caller realize the stated common-coordinate field accesses, classical cleanup and finite-precision inverses with a complete physical tariff? Start with one actual boundary and its numerical range; the scalar PR5037 kernel alone does not resolve Gaussian propagation or reversible ownership requirements.
+
+## Credit
+
+Cayden Burkart / SethBurkart123 supplies PR4940's coded reverse chronology; Dillon supplies PR4933's actual signed normalizers, physical ABI, mode factorization and local bounds; Dugongue / mdumitrean supplies PR4929's coded producer. Credit Cinna Davis for PR4440/4470/4694/4698, Cao Yifan / intqwq, zxv, Jacob Alan Sussman, and all retained native, Clifford, query, ownership, precision and compiler contributors. JoyboyBrian's PR5036 scalar gap and PR5037 finite-grid kernel are retained predecessors. The new result is the one-pair all-block correction and honest boundary-inclusive ledger. Prepared for JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. Independent human or formal-kernel acceptance is not claimed.

research/physical-inverse-pair/RESULT.json

@@ -0,0 +1,74 @@
+{
+  "status": "PASS_PHYSICAL_INVERSE_PAIR",
+  "scope": "One-stage exact operator identity; conditional physical ledger, no new kappa",
+  "normalizer_absolute_phase_checks": 57344,
+  "widths": [
+    1,
+    2
+  ],
+  "walsh_fibers": [
+    [
+      0
+    ],
+    [
+      1
+    ],
+    [
+      19
+    ],
+    [
+      511
+    ],
+    [
+      0,
+      1
+    ],
+    [
+      1,
+      19
+    ],
+    [
+      17,
+      256
+    ],
+    [
+      511,
+      511
+    ]
+  ],
+  "independent_main_basis_columns": 1792,
+  "physical_address1_walsh_coefficients": 512,
+  "mixed_input_checks": 8,
+  "helpers": "408 inherited autonomous output operators; never scratch",
+  "semantic_rejections": [
+    "omit_exit_q",
+    "omit_entry",
+    "wrong_order",
+    "unsigned_K",
+    "old_scalar_A",
+    "helper_erasure"
+  ],
+  "added_paid_rank1_jobs": 336,
+  "total_paid_profile": {
+    "1": 2537,
+    "2": 412,
+    "3": 510,
+    "4": 127,
+    "5": 40
+  },
+  "wrapper_monomial_maps_upper": 1792,
+  "scalar_adds": 2800,
+  "recoding_owned_clears": 48,
+  "query_initial_clears": 112,
+  "query_copies": 112,
+  "query_owned_erases": 112,
+  "recoding_field_workspace": 120,
+  "inverse_recode_calls": 2,
+  "forward_recode_calls": 1,
+  "unknown_nonzero_costs": [
+    "Native/query internal scratch and movement",
+    "Physical field-map and rational ADD tape tariffs",
+    "Finite precision and global error budget",
+    "Full-controller bridge and boundary accounting"
+  ]
+}

research/physical-inverse-pair/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/coded-inverse-fixed-grid/PROOF.md",
+      "usage": "input",
+      "git_blob": "a465ed5ce6b0bd7ac03bc79e72003380a839d7f4",
+      "sha256": "2bf523cf4f4b3e6bd90805e86f2cbf5d1d85142c16e751e72f09480bcdbee5cd"
+    },
+    {
+      "path": "research/coded-native-caller/CODE.json",
+      "usage": "input",
+      "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae",
+      "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0"
+    },
+    {
+      "path": "research/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    },
+    {
+      "path": "research/coded-native-caller/PHYSICAL.md",
+      "usage": "input",
+      "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f",
+      "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078"
+    },
+    {
+      "path": "research/coded-reverse-controller/verify.py",
+      "usage": "input",
+      "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c",
+      "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67"
+    },
+    {
+      "path": "research/coded-reverse-physical-pair-gap/README.md",
+      "usage": "input",
+      "git_blob": "fe31036c0ee2f35583767ee32dc0160e0aeb4f72",
+      "sha256": "cc258ef038af79dfcda1be97156cf2164f936a38ebf8e06ddf186ea8be56fae9"
+    }
+  ]
+}