From 57c650a571e23e9f06d7f3aff250d57266054992 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:21:16 -0500 Subject: [PATCH 1/2] Prove local inverse-pair error cancellation and a sharper precision guard --- .../physical-pair-error-transfer/PROOF.md | 65 +++++++++ .../physical-pair-error-transfer/README.md | 35 +++++ .../physical-pair-error-transfer/RESULT.json | 48 +++++++ .../physical-pair-error-transfer/SOURCES.json | 42 ++++++ .../physical-pair-error-transfer/TASK.json | 74 ++++++++++ .../physical-pair-error-transfer/VERIFY.json | 39 ++++++ .../physical-pair-error-transfer/verify.py | 127 ++++++++++++++++++ 7 files changed, 430 insertions(+) create mode 100644 research/physical-pair-error-transfer/PROOF.md create mode 100644 research/physical-pair-error-transfer/README.md create mode 100644 research/physical-pair-error-transfer/RESULT.json create mode 100644 research/physical-pair-error-transfer/SOURCES.json create mode 100644 research/physical-pair-error-transfer/TASK.json create mode 100644 research/physical-pair-error-transfer/VERIFY.json create mode 100644 research/physical-pair-error-transfer/verify.py diff --git a/research/physical-pair-error-transfer/PROOF.md b/research/physical-pair-error-transfer/PROOF.md new file mode 100644 index 0000000000..24f918065f --- /dev/null +++ b/research/physical-pair-error-transfer/PROOF.md @@ -0,0 +1,65 @@ +# 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 new file mode 100644 index 0000000000..3edb3e5d07 --- /dev/null +++ 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 new file mode 100644 index 0000000000..30e6f3d5d2 --- /dev/null +++ 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 new file mode 100644 index 0000000000..b2d8227fe8 --- /dev/null +++ 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 new file mode 100644 index 0000000000..ca37f2ba97 --- /dev/null +++ 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 new file mode 100644 index 0000000000..f931f5e30b --- /dev/null +++ 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." + } + ] +} diff --git a/research/physical-pair-error-transfer/verify.py b/research/physical-pair-error-transfer/verify.py new file mode 100644 index 0000000000..d0b287e9ff --- /dev/null +++ b/research/physical-pair-error-transfer/verify.py @@ -0,0 +1,127 @@ +"""Check the local pair error formula. Ali Romman with OpenAI Codex assistance. +Apache-2.0. The written proof gives the all-width statement. +""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import json +from types import SimpleNamespace +import argparse + +def need(ok, why): + if not ok: + raise ValueError(why) + +HERE = Path(__file__).resolve().parent +root = HERE.parents[1] +for pin in json.loads((HERE/'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + need(sha256((root/pin['path']).read_bytes()).hexdigest() == pin['sha256'], 'Declared source pin') + +paths = ['research/native-center-free-code/CODE.json', + 'research/coded-native-caller/NORMALIZERS.json', + 'research/coded-inverse-fixed-grid/kernel.py'] +raw = [(root / p).read_bytes() for p in paths] +need([sha256(b).hexdigest() for b in raw] == [ + '8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0', + 'ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da', + 'bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303'], 'Source pins') +a = [[F(v) for v in row] for row in json.loads(raw[0])['A']] +records = json.loads(raw[1])['ports'] +n = len(a) +need(n == 112 and len(records) == n, 'Owner count') +need(all(sum(map(abs, row)) == 26 for row in a), 'Absolute code row sums') +modes = json.loads(raw[1])['mode_columns'] +need(all(sum(a[i][j]*m[j] for j in range(n)) == -13*m[i] + for m in modes for i in range(n)), 'Error modes have eigenvalue -13') +# A^2 + 12A = 13I gives the inverse used below. +need(all(sum(a[i][k]*a[k][j] for k in range(n)) + 12*a[i][j] + == 13*(i == j) for i in range(n) for j in range(n)), 'Inverse identity') + +def add(x, y, s=1): + return [(p[0]+s*q[0], p[1]+s*q[1]) for p,q in zip(x,y)] + +def phase(x, exponents): + out = [] + for (r,i), e in zip(x, exponents): + out.append(((r,i),(-i,r),(-r,-i),(i,-r))[e % 4]) + return out + +def code(x, inverse=False): + y = [(sum(aij*v[0] for aij,v in zip(row,x)), + sum(aij*v[1] for aij,v in zip(row,x))) for row in a] + if inverse: + return [((u[0]+12*v[0])/13,(u[1]+12*v[1])/13) for u,v in zip(y,x)] + return y + +def mv(rows, u): + return sum(((r & u).bit_count() % 2) << i for i,r in enumerate(rows)) + +def trans(rows): + return [sum(((r >> i)&1)<>1).bit_count() for z in vs) for vs in v] + need(all((qi+di-sum(u.bit_count() for u in us))%4 == 0 for qi,di in zip(q,d)), + 'Physical DQ phase') + qi = [-e for e in q] + fixtures = [[(F((i*i+3*s)%29,7+s), F((7*i+s)%19,11+s)) for i in range(n)] + for s in range(1,6)] + x,y,e0,e1,e2 = fixtures + y1 = add(code(y, True), e0) + x2 = phase(add(x, phase(code(y1),q),-1),d) + y2 = phase(y1,d) + query = phase(add(code(x2,True),e1),qi) + y3 = add(y2,query) + out = phase(add(code(phase(y3,q)),e2),qi) + idealx = phase(add(x,phase(y,q),-1),d) + idealy = phase(phase(x,qi),d) + dx = phase(phase(code(e0),q),d) + dy = phase(add(code(e1),e2),qi) + need(x2 == add(idealx,dx,-1), 'Entry error in X') + need(out == add(idealy,dy), 'Exact local Y residual') + rejected['entry_error_in_X'] |= x2 != idealx + wrong = phase(add(code(phase(add(y2,add(code(phase(x2,qi),True),phase(e1,qi))),q)),e2),qi) + rejected['thin_order'] |= wrong != out + rejected['exit_error_before_C'] |= out != add(idealy,phase(code(add(e1,e2)),qi)) +need(all(rejected.values()), 'Controls must fail') +# Build a literal row of G^tensor k and sum real and imaginary magnitudes. +row = [(F(1),F(0))] +for k in range(1,13): + row = [((r-s*i)/2,(i+s*r)/2) for r,i in row for s in (1,-1)] + need(sum(abs(r)+abs(i) for r,i in row) == 2**((k+1)//2), 'Real component norm') +for f in range(1,101): + guard = (9*f+1)//2 + 5 + need(F(26*2**((9*f+1)//2),2**guard) < 1, 'Precision guard') +result = {'status':'PASS_PHYSICAL_PAIR_ERROR_TRANSFER', + 'source_sha256':dict(zip(paths,map(lambda b:sha256(b).hexdigest(),raw))), + 'fibers':[list(u) for u in fibers], 'code_rows':n, 'code_abs_row_sum':26, + 'actual_kernel_fixtures':12, 'gaussian_tensor_rows':12, 'guard_widths_checked':100, + 'controls':rejected} +parser = argparse.ArgumentParser() +parser.add_argument('--write-result', action='store_true') +args = parser.parse_args() +if args.write_result: + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2)+'\n') +else: + need(json.loads((HERE/'RESULT.json').read_text()) == result, 'Receipt mismatch') +print(json.dumps(result, sort_keys=True)) From 38065821a76108dc512391b124ffb7b64feed93b Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:49:41 -0500 Subject: [PATCH 2/2] Remove the trailing empty proof line --- research/physical-pair-error-transfer/PROOF.md | 1 - 1 file changed, 1 deletion(-) diff --git a/research/physical-pair-error-transfer/PROOF.md b/research/physical-pair-error-transfer/PROOF.md index 24f918065f..43d860fb44 100644 --- a/research/physical-pair-error-transfer/PROOF.md +++ b/research/physical-pair-error-transfer/PROOF.md @@ -62,4 +62,3 @@ Expected verifier marker: PASS_PHYSICAL_PAIR_ERROR_TRANSFER. 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. -