Prove a complete local residual budget for the physical inverse pair

research/physical-pair-full-residuals/PROOF.md

@@ -0,0 +1,156 @@
+# Full local residual transfer for the inverse-coded pair
+
+This enabling proof extends the inverse-only result in
+[PR #5322](https://github.com/CrocSwap/integer-mult-bounds/pull/5322).
+It allows errors at every stated operation in the local pair. It does not
+prove provider accuracy or admit a complete caller. The complete paid
+Gaussian profile and kappa are unchanged.
+
+Use the physical operators and order from JoyboyBrian's
+[PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069),
+as retained at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf.
+D and Q commute, and C commutes with DQ. In general C does not commute
+with D or Q separately. All operators act on 112 independent owners.
+Errors use the maximum absolute real or imaginary component.
+
+## The chronological residual identity
+
+Each residual is the returned output minus the exact operator on its actual
+computed input. Thus a residual can be nonlinear and depend on all earlier
+errors. Define e0 after the entrance inverse, bX and bY after FULL, e1 after
+the thin inverse, et after its Q^-1 and destination update, eQ after the exit
+Q, eC after the exit C, and eL after the final Q^-1. Exact copies and monomial
+wrappers are assumed. A defect in an update can be included in et, at the
+same output site. The executed values satisfy these definitions:
+
+```text
+y1 = C^-1 y + e0
+x2 = D(x-Q C y1) + bX
+y2 = D y1 + bY
+y3 = y2 + Q^-1(C^-1 x2+e1) + et
+outY = Q^-1[C(Q y3+eQ)+eC] + eL.
+```
+
+Set S=Q^-1 C Q. Relative to the exact standard-pair outputs
+`D(x-Qy)` and `DQ^-1 x`, the errors are exactly
+
+```text
+Delta X = -DQ C e0 + bX
+Delta Y = Q^-1 bX + S bY + Q^-1 C e1 + S et
+          + Q^-1 C eQ + Q^-1 eC + eL.
+```
+
+To prove this, substitute x2 in y3. The two terms involving the original y
+cancel by `C^-1 DQ C=DQ`; the two terms involving e0 cancel by the same
+identity. The exact part left in y3 is `Q^-1 C^-1 D x`. Its perturbation is
+`Q^-1 C^-1 bX+bY+Q^-1 e1+et`. Apply the last line of the schedule and collect
+terms. This proves the formula on every input and every residual vector.
+There is no residual product and no assumption that a rounded map is linear.
+
+## Exact terminal norm
+
+Dillon's [PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933)
+gives the actual normalizers `K_i=Z_(z_i) P_(G_i)` and the four-point expansion
+in its retained TERMINAL.md. For a nonzero code entry, put M=K_i^-1 K_j.
+The source ports are distinct, so `G_i^-1 G_j e` is neither zero nor e.
+In one digit column, each row of `Q^-1 M Q` therefore has four entries,
+each equal to one of `+1/2,-1/2,+i/2,-i/2`.
+
+At positive fiber width f, the block is its f-fold tensor power. Each row has
+4^f entries of magnitude 2^-f, and each entry is real or purely imaginary.
+Thus each realified row has absolute sum 2^f. The owner coefficient A_ij is
+applied once. Distinct input owners occupy disjoint columns, so there is no
+cancellation between their row sums. Every row of A has absolute sum 26.
+Consequently
+
+```text
+||Q_f^-1 C_f Q_f||_(infinity,real) = 26 * 2^f.
+```
+
+This is an exact induced norm for arbitrary residuals. It improves the
+product bound `26*2^(2 ceil(f/2))` by a factor two when f is odd.
+It does not reduce the paid cost of the terminal operation.
+
+For comparison, let B1=2^ceil(f/2) and B9=2^ceil(9f/2).
+The canonical Gaussian row formula gives `||Q^-1||=B1` and `||DQ||=B9`.
+A real signed monomial preserves row absolute sums. Each block of Q^-1 C
+is a Gaussian followed by a signed monomial, with total owner weight 26.
+Hence `||Q^-1 C||=26 B1`; likewise `||DQ C||=26 B9`.
+
+## Budget with the actual inverse kernel
+
+The source finite kernel in [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035)
+computes `x-M round(M^T x/52)` in integer grid units. Since
+`A=I-MM^T/4` and `M^T M=56I`, its residual from A^-1 is `-M delta`,
+where each mode rounding error delta has magnitude at most half a grid unit.
+Each owner has four mode entries, so its error is at most two grid units.
+Also `A M=-13 M`. Exact signed monomial wrappers therefore give `C e=-13 e`
+for each of the two inverse residuals, even on perturbed valid inputs.
+This is the error-shape premise already isolated by PR #5322.
+
+Let the eight residual bounds be epsilon0, epsilonX, epsilonY, epsilon1,
+epsilont, epsilonQ, epsilonC and epsilonL in the order defined above. Then
+
+```text
+||Delta X|| <= 13 B9 epsilon0 + epsilonX
+||Delta Y|| <= B1 epsilonX + 26*2^f (epsilonY+epsilont)
+               + 13 B1 epsilon1 + 26 B1 epsilonQ
+               + B1 epsilonC + epsilonL.
+```
+
+These unequal allowances let a caller assign accuracy at each actual output
+site. A useful common sufficient contract is, for u=2^-P,
+
+```text
+epsilon0, epsilon1 <= 2u
+all six other residual bounds <= u.
+```
+
+Under that contract, X error is at most `(26B9+1)u`, and Y error is at most
+`(54B1+52*2^f+1)u`. For f>=1, B1<=2^f and B9>=16*2^f. Thus X is below
+27B9 u and Y is at most 107*2^f u, below 7B9 u. It follows that
+
+```text
+P = p + ceil(9f/2) + 5  =>  both output errors are strictly below 2^-p.
+```
+
+The inverse-only guard now funds the additional returned residuals under
+explicit call contracts. It is not a proof that each physical provider meets
+those contracts. If the inverse implementation does not preserve the error
+subspace, replace the coefficients 13 by 26 in the two displayed bounds.
+
+## Evidence and limits
+
+The checker authenticates all six declared inputs. It checks all code entries,
+the mode Gram identity, all 112 normalizers and all 5,824 terminal-block
+independence premises. Three actual blocks have all 512 rows and columns
+expanded with exact signed coefficients. A diagonal control loses four-point
+support. Sixty-three exact rational chronological cases cover seven actual
+Walsh fibers at widths 1, 2, 3 and 5, with each residual injected alone and
+all injected together. Controls detect a missing FULL-Y residual, a missing
+exit-Q residual, and reversed thin order. Twelve actual kernel calls verify
+the inverse error subspace and paid scratch return. Five hundred widths check
+the integer guard. The written operator, row and inequality proofs cover all
+positive widths; the finite checks corroborate them.
+
+The second inverse range must include the perturbed x2. Provider input-domain
+gates and their internal precision costs remain necessary. All Gaussian calls,
+ordinary arithmetic, movement, workspace, copying and cleanup must retain
+paid physical contracts. The error bound does not remove the unshared
+boundary-call obstruction or supply a cheaper complete caller. It is a local
+analytic result, not a full native, compiler, Lean or selected replay.
+
+## Credit and next question
+
+PR #5069 supplies the exact pair and its charged schedule. PR #4933 supplies
+the real signed normalizers, mode code and four-point terminal formula.
+PR #5035 supplies the finite rounded kernel. PR #5322 supplies the inverse-only
+residual cancellation and error-shape guard. Those predecessors are not new
+claims here. New result: all returned residual sites, the exact component
+terminal norm and the resulting complete local accuracy contract.
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+
+The next question is whether a changed or shared-boundary caller can meet
+these local provider bounds within its complete price and range budget.
+Start by binding each epsilon above to a named provider contract. No
+independent human or proof-kernel acceptance is claimed.

research/physical-pair-full-residuals/README.md

@@ -0,0 +1,47 @@
+# A complete local residual contract for the inverse-coded pair
+
+The guard `P=p+ceil(9f/2)+5` suffices for both pair outputs at every f>=1,
+provided the two actual inverse kernels return at most two grid units of
+error and each of the other six residual vectors has at most one. The new
+proof includes FULL and Gaussian errors, which PR #5322 treated as zero.
+It also proves `||Q^-1 C Q||_(infinity,real)=26*2^f` for the actual code.
+The complete paid Gaussian profile and kappa do not change.
+
+[PROOF.md](PROOF.md) gives the chronological identity, unequal site budgets,
+quantified proof, source credit and limits. [RESULT.json](RESULT.json) records
+the exact checks. [SOURCES.json](SOURCES.json) pins canonical main
+ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority 7. The scoped
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19151016)
+excludes the active native-history construction.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/physical-pair-full-residuals
+python3.12 -I -O -W error -B research/physical-pair-full-residuals/verify.py
+```
+
+Expected marker: PASS_FULL_PAIR_RESIDUAL_TRANSFER. Both modes check 63
+chronological cases, all 5,824 block premises, 3,072 literal rows/columns,
+12 actual source-kernel vectors and 500 guard widths. Source modules load
+from authenticated source bytes. The written proof covers the all-width
+result. No full physical caller, provider-accuracy, Lean, compiler or
+selected-frontier replay ran.
+
+## Open next questions
+
+Bind each returned residual allowance to one physical provider and include
+its input range, internal precision, movement and cost. A changed or shared
+boundary caller still needs an affordable complete invoice. TASK.json states
+the next check and blocker.
+
+## Credit
+
+JoyboyBrian's PR #5069 supplies the pair; PR #5035 supplies the finite kernel.
+Dillon's PR #4933 supplies the normalizers and terminal formula. PR #5322
+supplies the inverse-only error transfer. PROOF.md links these predecessors.
+The retained native, controller, precision and compiler authors keep their
+credit. New all-site theorem and checks: Ali Romman with substantial OpenAI
+Codex assistance. Apache-2.0. Author-checked, not independent acceptance.

research/physical-pair-full-residuals/RESULT.json

@@ -0,0 +1,17 @@
+{
+  "status": "PASS_FULL_PAIR_RESIDUAL_TRANSFER",
+  "chronological_cases": 63,
+  "actual_terminal_blocks": 5824,
+  "literal_row_and_column_checks": 3072,
+  "source_kernel_vectors": 12,
+  "guard_widths": 500,
+  "controls": {
+    "omit_full_Y": true,
+    "omit_exit_Q": true,
+    "wrong_thin_order": true
+  },
+  "terminal_component_norm": "26*2^f",
+  "guard": "P=p+ceil(9f/2)+5",
+  "provider_accuracy_verified": false,
+  "complete_caller_run": false
+}

research/physical-pair-full-residuals/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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/kernel.py",
+      "usage": "input",
+      "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b",
+      "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303"
+    },
+    {
+      "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-native-caller/TERMINAL.md",
+      "usage": "input",
+      "git_blob": "213a1726761224d6f705b90affc52b6600c95676",
+      "sha256": "49e8f958e0a43f5d0b307dbef81c81076a55e83137563d7e620c608201d6dbcc"
+    },
+    {
+      "path": "research/native-center-free-code/CODE.json",
+      "usage": "input",
+      "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae",
+      "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0"
+    },
+    {
+      "path": "research/physical-inverse-pair/README.md",
+      "usage": "input",
+      "git_blob": "a4ed4756eaa2e2e1fe3d91f2d8c7f1d682d8185b",
+      "sha256": "32505039ae7289b6358de5ec9d83a8bb63b76140209b521c7e8c82e8e0000783"
+    }
+  ]
+}

research/physical-pair-full-residuals/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "All-site local residual transfer and an exact terminal component norm for the physical inverse-coded pair.",
+  "scope_change_reason": "PR5322 assumes exact native and Gaussian calls. This follow-up assigns residuals to the actual remaining sites and derives their full local budget.",
+  "bottleneck_link": "A physical coded caller needs explicit numerical accuracy at every call site before admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the local conditional theorem and source-bound checks; do not expand or admit a complete caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json: quantified residual/norm proof, exact chronological cases, terminal rows and source-kernel checks.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human acceptance.",
+  "open_questions": [
+    {
+      "question": "Can an affordable changed caller meet every stated provider residual and input-range contract?",
+      "why_it_matters": "The analytic bound does not establish provider accuracy or physical cost.",
+      "first_step": "Bind each epsilon to one named provider and include its internal precision and movement cost.",
+      "blocked_by": "Complete caller allowance and provider domain/accuracy proofs."
+    }
+  ]
+}

research/physical-pair-full-residuals/VERIFY.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-inverse-fixed-grid/kernel.py",
+    "research/coded-native-caller/NORMALIZERS.json",
+    "research/coded-native-caller/PHYSICAL.md",
+    "research/coded-native-caller/TERMINAL.md",
+    "research/native-center-free-code/CODE.json",
+    "research/physical-inverse-pair/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source pins, all-site chronological errors, exact terminal rows, actual inverse residual shape and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source pins, all-site chronological errors, exact terminal rows, actual inverse residual shape and semantic controls."
+    }
+  ]
+}