Mister-Meeseeks · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026
diff --git a/research/physical-pair-error-transfer/PROOF.md b/research/physical-pair-error-transfer/PROOF.md
@@ -0,0 +1,64 @@
+# Exact local error cancellation and a sharper inverse-pair precision guard
+
+FINDING — exact local rounding transfer for the physical inverse-coded pair. This closes one part of the precision question in [PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069). It supplies a precision guard for the two inverse recodings. It does not admit a complete caller or increase kappa.
+
+Use the exact operators and order in the [source pair proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/physical-inverse-pair/README.md). Let e0 be the residual just after the entrance C^-1, e1 the residual just after the thin C^-1 on its actual, possibly perturbed input, and e2 the residual just after the exit C, before the final Q^-1. Other operations are exact in this local statement. Then the output errors are exactly
+
+```text
+Delta X = -D Q C e0
+Delta Y = Q^-1 (C e1 + e2).
+```
+
+In particular, the entrance inverse error cancels from Y. The second inverse need not be linear or have an error independent of its input: define e1 as its actual output minus C^-1 of that input. Thus this formula also applies to the noninjective rounded kernel in [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035). It has no product of e0 and e1.
+
+Proof: after entrance and FULL,
+
+```text
+y1 = C^-1 y + e0
+x2 = D x - D Q y - D Q C e0
+y2 = D C^-1 y + D e0.
+```
+
+The thin adds Q^-1(C^-1 x2+e1) to y2. Use [C,DQ]=0, which the source proves for the actual signed normalizers. Both the original-y term and the e0 term cancel. The remaining value is Q^-1 C^-1 D x+Q^-1 e1. Applying the exit Q^-1 C Q, with e2 injected at the stated site, gives D Q^-1 x+Q^-1(C e1+e2). This proof never commutes C through Q alone.
+
+**Component precision, for every positive tensor width f.** Measure the maximum absolute real or imaginary component. The exact [112-owner code](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/native-center-free-code/CODE.json) has absolute row sum 26. A row of a k-axis canonical complex Gaussian has real-component absolute row sum 2^ceil(k/2): its 2^k coefficients have modulus 2^(-k/2); for even k each is real or imaginary, while for odd k both components have equal magnitude. Right multiplication by a real signed monomial preserves this sum. Each owner block of C_f is A_ij K_i,f^-1 K_j,f, with A applied once across owners. Therefore
+
+```text
+||D_f Q_f C_f||_(infinity,real) = 26 * 2^ceil(9f/2)
+||Q_f^-1 C_f||_(infinity,real) = 26 * 2^ceil(f/2)
+||Delta X|| <= 26 * 2^ceil(9f/2) ||e0||
+||Delta Y|| <= 2^ceil(f/2) (26 ||e1|| + ||e2||).
+```
+
+These are induced norms for arbitrary residual vectors. They do not assert that a rounded kernel attains each worst case. With exact exit recoding and each inverse error at most 2*2^-P, the two inverse errors contribute at most 52*2^(ceil(9f/2)-P) to any output component. Hence
+
+```text
+P = p + ceil(9f/2) + 6
+```
+
+makes their combined contribution strictly less than 2^-p. The width-dependent guard cannot be replaced by the width-independent Euclidean norm 13 when the contract is componentwise absolute precision.
+
+**Sharper guard for the actual mode kernel.** The [source kernel](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/coded-inverse-fixed-grid/kernel.py) rounds each of the eight modes before owner updates. In common coordinates its residual is -M delta, where delta contains the eight mode rounding errors. Since A M=-13 M, each physical residual obeys C_f e=-13 e. For these two kernel calls, with exact wrappers and exact other operations, the formula improves to
+
+```text
+Delta X = 13 D Q e0
+Delta Y = -13 Q^-1 e1          (e2=0).
+```
+
+The component bound is then 26*2^(ceil(9f/2)-P), and **P=p+ceil(9f/2)+5 suffices**. This reduces the generic residual guard by one bit. It uses the source kernel's error shape, not a better rounding rule or a new machine tariff. A different inverse implementation must establish that error-shape premise before it uses the sharper guard.
+
+**Evidence.** The checker in verify.py authenticates the declared input files, verifies A^2+12A=13I and all 112 row sums and A M=-13 M, and checks the chronological residual formula with exact rational complex arithmetic in seven actual signed-normalizer Walsh fibers at widths 1,2,3,5. It rejects omitted X error, reversed thin order and the wrong exit injection site. Literal Gaussian tensor rows through 12 axes check the real-component norm; integer guards are checked for f=1,...,100. The written operator and row arguments establish the all-width statement; these finite fixtures do not enumerate every address. Twelve actual finite-kernel invocations also satisfy C e=-13 e and return owned scratch clean. Normal and optimized CPython 3.12.13 give the same receipt.
+
+Run the registered checks with CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/physical-pair-error-transfer
+```
+
+Expected verifier marker: PASS_PHYSICAL_PAIR_ERROR_TRANSFER.
+
+**Remaining limits and next step.** This is a local residual theorem. It does not fund native or Gaussian rounding, movement, field storage, common-coordinate access, or the whole caller's error budget. The second inverse input bound H must include the perturbed x2. The source kernel uses paid classical destructive writes; no reversible cleanup follows. No full native, compiler, outer-ledger or selected replay ran. First use this guard in a changed or shared-boundary caller with an affordable complete invoice; [the unshared p19 boundary budget](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19149724) already rejects repeated use of the original recipe.
+
+Source-number note: some retained package prose calls the finite-grid kernel PR5037. The actual kernel contribution is PR5035, as its PR body and package paths confirm. Links here use that verified identity.
+
+Credit: JoyboyBrian supplied the physical pair and finite-grid kernel; Dillon supplied the actual normalizers and code factorization; Dugongue supplied the center-free producer; Cayden Burkart supplied the coded controller. Cinna Davis, Cao Yifan, zxv, Jacob Alan Sussman and retained native/precision/compiler contributors keep their source credit. New residual derivation and checker: Ali Romman with OpenAI Codex assistance, Apache-2.0. This is author-checked evidence, not independent human or proof-kernel review.
diff --git a/research/physical-pair-error-transfer/README.md b/research/physical-pair-error-transfer/README.md
@@ -0,0 +1,35 @@
+# Exact local error cancellation and a sharper inverse-pair precision guard
+
+FINDING — exact local rounding transfer for the physical inverse-coded pair. This closes one part of the precision question in [PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069). It supplies a precision guard for the two inverse recodings. It does not admit a complete caller or increase kappa.
+
+[PROOF.md](PROOF.md) states the quantified result, dependencies and limits.
+[RESULT.json](RESULT.json) records the bounded exact replay.
+[SOURCES.json](SOURCES.json) pins the input bytes at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf.
+This publishes the result from [its Discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/5302); it is the same
+contribution, with a committed proof and registered replay.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/physical-pair-error-transfer
+python3.12 -I -O -W error -B research/physical-pair-error-transfer/verify.py
+```
+
+Both registered modes authenticate the declared input bytes and compare the
+exact receipt. Source modules load from authenticated source bytes. The written
+proof covers the quantified domain; finite fixtures do not replace it.
+No full physical caller, native/compiler, Lean or selected-frontier replay ran.
+The complete kappa calculation is unchanged.
+
+## Open next questions
+
+Bind the local residual guard to an affordable complete caller and include Gaussian and native residuals.
+The remaining contracts block caller admission. See TASK.json and PROOF.md.
+
+## Credit
+
+The proof retains the named predecessors and links their exact sources.
+New theorem and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0. This is author-checked evidence, not independent acceptance.
diff --git a/research/physical-pair-error-transfer/RESULT.json b/research/physical-pair-error-transfer/RESULT.json
@@ -0,0 +1,48 @@
+{
+  "status": "PASS_PHYSICAL_PAIR_ERROR_TRANSFER",
+  "source_sha256": {
+    "research/native-center-free-code/CODE.json": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0",
+    "research/coded-native-caller/NORMALIZERS.json": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da",
+    "research/coded-inverse-fixed-grid/kernel.py": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303"
+  },
+  "fibers": [
+    [
+      0
+    ],
+    [
+      1
+    ],
+    [
+      19
+    ],
+    [
+      511
+    ],
+    [
+      0,
+      1
+    ],
+    [
+      1,
+      19,
+      256
+    ],
+    [
+      17,
+      256,
+      3,
+      98,
+      511
+    ]
+  ],
+  "code_rows": 112,
+  "code_abs_row_sum": 26,
+  "actual_kernel_fixtures": 12,
+  "gaussian_tensor_rows": 12,
+  "guard_widths_checked": 100,
+  "controls": {
+    "entry_error_in_X": true,
+    "thin_order": true,
+    "exit_error_before_C": true
+  }
+}
diff --git a/research/physical-pair-error-transfer/SOURCES.json b/research/physical-pair-error-transfer/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "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/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"
+    }
+  ]
+}
diff --git a/research/physical-pair-error-transfer/TASK.json b/research/physical-pair-error-transfer/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": "Exact local error cancellation and a sharper inverse-pair precision guard",
+  "scope_change_reason": "Publish the completed, scoped Discussion result as a source-bound proof and replay package. The local interface or error obligation is separate from the complete physical caller.",
+  "bottleneck_link": "The physical construction needs funded precision and owned state. This result supplies one exact local obligation; it does not change the paid Gaussian profile.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the stated theorem and its bounded checks. Do not admit a caller or change the selected frontier.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json give the theorem, source-bound exact checks and their limits.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Bind the local residual guard to an affordable complete caller and include Gaussian and native residuals.",
+      "why_it_matters": "The complete physical cost and accuracy obligations still bind admission.",
+      "first_step": "Bind the local residual guard to an affordable complete caller and include Gaussian and native residuals.",
+      "blocked_by": "The remaining caller contracts listed in PROOF.md."
+    }
+  ]
+}
diff --git a/research/physical-pair-error-transfer/VERIFY.json b/research/physical-pair-error-transfer/VERIFY.json
@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-inverse-fixed-grid/kernel.py",
+    "research/coded-native-caller/NORMALIZERS.json",
+    "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": "Authenticate source bytes, check the stated exact identities and controls, and compare the committed receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate source bytes, check the stated exact identities and controls, and compare the committed receipt."
+    }
+  ]
+}