diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 6207ec57b..4cd48e87e 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -395,6 +395,21 @@ jobs: echo "=== kt4_prem1_indep_check.py ===" python3 kt4_prem1_indep_check.py + probes_oichannel1: + name: Numerical probes / OI channel protocol + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - uses: actions/setup-python@v5 + with: + python-version: '3.11' + - name: Exact channel and cone controls + run: python3 -I -B verification/lean/oi_channel1_check.py + - name: Audit control mutation tests + run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/controls.py --self-test + # Act 42. Two shards run on every event; the exclusion shards, about six CPU-hours between them, # run only on workflow_dispatch, which is how the exact-head attestations are taken (section A.39). # On any other event the matrix job is skipped and the aggregate below requires exactly that. @@ -490,7 +505,7 @@ jobs: probes: name: Numerical probes - needs: [probes_core_a, probes_core_b, probes_a36, probes_a38, probes_a40, probes_a41_production, probes_a41_independent, probes_a41_hulls, probes_a45, probes_nb1, probes_kinf2, probes_kt4prem1, probes_a42_witness, probes_a42_census01, probes_a42_exclusion, probes_foundations] + needs: [probes_core_a, probes_core_b, probes_a36, probes_a38, probes_a40, probes_a41_production, probes_a41_independent, probes_a41_hulls, probes_a45, probes_nb1, probes_kinf2, probes_kt4prem1, probes_oichannel1, probes_a42_witness, probes_a42_census01, probes_a42_exclusion, probes_foundations] if: ${{ always() }} runs-on: ubuntu-latest steps: @@ -508,6 +523,7 @@ jobs: NB1_RESULT: ${{ needs.probes_nb1.result }} KINF2_RESULT: ${{ needs.probes_kinf2.result }} KT4PREM1_RESULT: ${{ needs.probes_kt4prem1.result }} + OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }} A42W_RESULT: ${{ needs.probes_a42_witness.result }} A42C_RESULT: ${{ needs.probes_a42_census01.result }} A42X_RESULT: ${{ needs.probes_a42_exclusion.result }} @@ -525,6 +541,7 @@ jobs: echo "nb1=${NB1_RESULT}" echo "kinf2=${KINF2_RESULT}" echo "kt4prem1=${KT4PREM1_RESULT}" + echo "oichannel1=${OICHANNEL1_RESULT}" echo "a42_witness=${A42W_RESULT}" echo "a42_census01=${A42C_RESULT}" echo "a42_exclusion=${A42X_RESULT} (event ${GITHUB_EVENT_NAME})" @@ -541,6 +558,7 @@ jobs: test "${NB1_RESULT}" = success test "${KINF2_RESULT}" = success test "${KT4PREM1_RESULT}" = success + test "${OICHANNEL1_RESULT}" = success test "${A42W_RESULT}" = success test "${A42C_RESULT}" = success if [ "${GITHUB_EVENT_NAME}" = workflow_dispatch ]; then diff --git a/verification/lean/oi_channel1_check.py b/verification/lean/oi_channel1_check.py new file mode 100644 index 000000000..3b4cc4a6f --- /dev/null +++ b/verification/lean/oi_channel1_check.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""Exact channel controls. Decision rule: PREREGISTRATION.md, commit 78aa5b25. + +No imported thread code, external input, floating point, or third-party package. +Finite checks are [X]; universal steps in ARGUMENT.md are separately [W]. +""" +from dataclasses import dataclass +from fractions import Fraction as F +from itertools import permutations, product +import sys + + +@dataclass(frozen=True) +class G: + r: F = F(0) + i: F = F(0) + + @staticmethod + def of(x): + return x if isinstance(x, G) else G(F(x)) + + def __add__(self, x): + x = G.of(x) + return G(self.r + x.r, self.i + x.i) + + __radd__ = __add__ + + def __neg__(self): + return G(-self.r, -self.i) + + def __sub__(self, x): + return self + -G.of(x) + + def __rsub__(self, x): + return G.of(x) + -self + + def __mul__(self, x): + x = G.of(x) + return G(self.r*x.r - self.i*x.i, self.r*x.i + self.i*x.r) + + __rmul__ = __mul__ + + def conj(self): + return G(self.r, -self.i) + + +I = G(F(0), F(1)) + + +def mat(rows): + return tuple(tuple(G.of(x) for x in row) for row in rows) + + +def eye(n): + return mat([[int(i == j) for j in range(n)] for i in range(n)]) + + +def unit(n, i, j): + return mat([[int(a == i and b == j) for b in range(n)] for a in range(n)]) + + +def add(a, b): + return tuple(tuple(x+y for x, y in zip(r, s)) for r, s in zip(a, b)) + + +def scale(x, a): + return tuple(tuple(x*v for v in r) for r in a) + + +def mul(a, b): + return tuple(tuple(sum((a[i][k]*b[k][j] for k in range(len(b))), G()) + for j in range(len(b[0]))) for i in range(len(a))) + + +def adj(a): + return tuple(tuple(a[j][i].conj() for j in range(len(a))) for i in range(len(a[0]))) + + +def kron(a, b): + return tuple(tuple(a[i][j]*b[k][l] for j in range(len(a[0])) for l in range(len(b[0]))) + for i in range(len(a)) for k in range(len(b))) + + +def ad(u, x): + return mul(mul(u, x), adj(u)) + + +def tr(a): + return sum((a[i][i] for i in range(len(a))), G()) + + +def msum(xs, n): + z = scale(0, eye(n)) + for x in xs: + z = add(z, x) + return z + + +def pair(a, b): + z = tr(mul(a, b)) + assert z.i == 0 + return z.r + + +X = mat([[0, 1], [1, 0]]) +Y = mat([[0, -I], [I, 0]]) +Z = mat([[1, 0], [0, -1]]) +P = (eye(2), X, Y, Z) +Hraw = mat([[1, 1], [1, -1]]) +S = mat([[1, 0], [0, I]]) +D = mat([[1, 0], [0, G(F(3, 5), F(4, 5))]]) +J = scale(F(1, 2), add(eye(2), scale(-I, msum([X, Y, Z], 2)))) +hh = kron(eye(2), kron(Hraw, Hraw)) +tof = mat([[int(i == (j ^ 4 if j % 4 == 3 else j)) for j in range(8)] for i in range(8)]) +U = scale(F(1, 4), mul(mul(mul(mul(hh, tof), kron(S, eye(4))), tof), hh)) +raw = tuple(mat([[U[4*a+j][4*b] for b in range(2)] for a in range(2)]) for j in range(4)) +branches = (raw[0],) + tuple(mul(Z, raw[j]) for j in range(1, 4)) + + +def stopped(k, rho, spectator=False, correct=True): + bs = branches if correct else raw + if spectator: + bs = tuple(kron(eye(2), b) for b in bs) + if k == 0: + return rho + success = ad(bs[0], rho) + failed = msum([ad(b, rho) for b in bs[1:]], len(rho)) + return add(success, stopped(k-1, failed, spectator, correct)) + + +def formula(k, rho, spectator=False): + p = F(3, 8)**k + u = kron(eye(2), D) if spectator else D + return add(scale(1-p, ad(u, rho)), scale(p, rho)) + + +checks = [] + + +def check(name, ok, detail=""): + checks.append((name, bool(ok))) + print(f"{name}: {'PASS' if ok else 'FAIL'}" + (f" ({detail})" if detail else "")) + + +check("U", mul(adj(U), U) == eye(8)) +reset = tuple(unit(4, 0, j) for j in range(4)) +check("RESET", msum([ad(r, scale(F(1, 4), eye(4))) for r in reset], 4) == unit(4, 0, 0)) +check("BRANCH", raw[0] == scale(G(F(3, 4), F(1, 4)), D) + and mul(adj(raw[0]), raw[0]) == scale(F(5, 8), eye(2)) + and all(mul(adj(b), b) == scale(F(1, 8), eye(2)) + and b == scale(b[0][0], eye(2)) for b in branches[1:])) +check("TP", msum([mul(adj(b), b) for b in branches], 2) == eye(2)) +check("TOKEN", all(stopped(k, unit(2, a, b)) == formula(k, unit(2, a, b)) + for k in range(7) for a, b in product(range(2), repeat=2)), "28 matrix-unit cases") +check("PAIR", all(stopped(k, unit(4, a, b), True) == formula(k, unit(4, a, b), True) + for k in range(7) for a, b in product(range(4), repeat=2)), "112 matrix-unit cases") +dict_ok = True +j_ok = mul(adj(J), J) == eye(2) +for k, m, n in product(range(7), range(4), range(4)): + p = F(3, 8)**k + a, b = p + (1-p)*F(3, 5), (1-p)*F(4, 5) + target = (P[0], add(scale(a, X), scale(b, Y)), add(scale(-b, X), scale(a, Y)), Z)[n] + dict_ok &= stopped(k, scale(F(1, 4), kron(P[m], P[n])), True) == scale(F(1, 4), kron(P[m], target)) +for m, n in product(range(4), repeat=2): + target = P[(0, 2, 3, 1)[n]] + j_ok &= ad(kron(eye(2), J), scale(F(1, 4), kron(P[m], P[n]))) == scale(F(1, 4), kron(P[m], target)) +check("DICT", dict_ok, "112 Pauli table cases") +check("J", j_ok, "16 Pauli table cases") + +# Independent defect-cone witnesses. Each dual test is an explicit rank-one PSD matrix. +es = [] +psis = [] +for s, t in product((-1, 1), repeat=2): + e = scale(F(1, 16), msum([eye(4), scale(s, kron(X, Z)), + scale(t, kron(Y, Y)), scale(-s*t, kron(Z, X))], 4)) + es.append(e) + proj = scale(F(1, 2), add(eye(4), scale(-8, e))) + psi = tuple(2*proj[j][0] for j in range(4)) + assert sum((z.conj()*z for z in psi), G()) == G.of(1) + psis.append(psi) + + +def proj(v, weight=1): + return mat([[weight*x*y.conj() for y in v] for x in v]) + + +def mv(u, v): + return tuple(sum((u[i][j]*v[j] for j in range(len(v))), G()) for i in range(len(u))) + + +def defect_min(u): + u = kron(eye(2), u) + tests = [proj(mv(u, v)) for v in psis] + for a, b in permutations(range(4), 2): + for phase in (G.of(1), G.of(-1), I, -I): + tests.append(proj(tuple(x+phase*y for x, y in zip(psis[a], psis[b])), F(1, 2))) + dual = [y for y in tests if all(pair(y, e) >= 0 for e in es)] + return min(pair(y, ad(u, e)) for y in dual for e in es) + + +d_min, j_min = defect_min(D), defect_min(J) +check("ZF", d_min == F(-1, 10) and j_min == F(-1, 8), f"drive={d_min}, mixer={j_min}") + +# The six-test cone: each signed permutation permutes the octahedral tests. +oct_tests = {(0, 0, 0)} +oct_tests = {tuple(sign if j == i else 0 for j in range(3)) for i in range(3) for sign in (-1, 1)} +rots = [] +for perm in permutations(range(3)): + parity = (-1)**sum(perm[i] > perm[j] for i in range(3) for j in range(i+1, 3)) + for signs in product((-1, 1), repeat=3): + if parity*signs[0]*signs[1]*signs[2] == 1: + rots.append((perm, signs)) +oct_ok = len(rots) == 24 and all({tuple(s[j]*v[p[j]] for j in range(3)) for v in oct_tests} == oct_tests + for p, s in rots) +image = (F(1, 4), F(5, 4), F(1)) +check("OCT", oct_ok and all(1+sum(v) >= 0 for v in oct_tests) + and min(1+sum(x*y for x, y in zip(image, v)) for v in oct_tests) == F(-1, 4), "24 actions; failing value=-1/4") + +open_ok = True +for k in range(1, 7): + p = F(3, 8)**k + a, b = p+(1-p)*F(3, 5), (1-p)*F(4, 5) + open_ok &= a*a+b*b == 1-F(4, 5)*p*(1-p) and a*a+b*b < 1 +check("OPEN", open_ok and F(3, 5)**2+F(4, 5)**2 == 1 + and (F(3, 5), F(4, 5)) != (1, 0), "finite images interior; limiting boundary point excluded") + +kappa = F(3, 2) +kp = scale(F(1, 2), add(eye(4), scale(kappa, kron(X, eye(2))))) +km = scale(F(1, 2), add(eye(4), scale(-kappa, kron(X, eye(2))))) +v = (G.of(1), G(), G.of(-1), G()) +negative_psd = sum((x.conj()*y for x, y in zip(v, mv(kp, v))), G()) +check("KAPPA", pair(kp, km) == F(-5, 4) and negative_psd == G.of(F(-1, 2)), "pair=-5/4; PSD test=-1/2") +check("CC-Z", any(stopped(1, unit(2, a, b), correct=False) != formula(1, unit(2, a, b)) + for a, b in product(range(2), repeat=2))) +check("CC-OUTCOME", mul(adj(raw[1]), raw[1]) != scale(F(5, 8), eye(2))) + + +def uniform_channel(rho): + inp = scale(F(1, 4), kron(rho, eye(4))) + full = ad(U, inp) + parts = [mat([[full[4*a+j][4*b+j] for b in range(2)] for a in range(2)]) for j in range(4)] + return msum([parts[0]] + [ad(Z, x) for x in parts[1:]], 2) + + +check("CC-RESET", any(uniform_channel(unit(2, a, b)) != formula(1, unit(2, a, b)) + for a, b in product(range(2), repeat=2))) +check("CC-ID", defect_min(eye(2)) >= 0) +check("CC-CLIFFORD", defect_min(X) >= 0) +failed = [name for name, ok in checks if not ok] +print(f"CHANNEL-CHECK: {'VOID' if failed else 'PASS'}; {len(checks)} checks; 140 matrix-unit cases") +if failed: + print("Failed: " + ", ".join(failed)) +sys.exit(bool(failed)) diff --git a/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/controls.py b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/controls.py new file mode 100644 index 000000000..55c16ebc4 --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/controls.py @@ -0,0 +1,173 @@ +#!/usr/bin/env python3 +"""Frozen controls for OI-CHANNEL-1; no network and no imported probe code.""" +import argparse +import hashlib +from pathlib import Path +import re +import subprocess +import sys + +ROUND = 'verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/' +PROBE = 'verification/lean/oi_channel1_check.py' +WORKFLOW = '.github/workflows/verify.yml' +D = '9f9f8257a980a1819fbbc1dc0019917cf8678626' +PROBE_SHA = '9937b6ffca6cf570cf7e1c3267ba1525ead48ada4d5f1e92959ec0f603baebff' +OUTPUT_SHA = 'ec73839a23e1c2e051140ff9b56d47bbda4f9b55e37963ca1256500b36642da5' +READING = ('The finite stopped circuit realizes the channel formula at depths 0 through 6 by exact arithmetic. ' + 'The all-depth recurrence and the universal cone arguments are written proofs. ' + 'Transfer to an arbitrary pair cone and the general-k InstAvail witness remain additional obligations. ' + 'This audit does not establish unconditional quantum reconstruction or full-model independence.') + + +def sha(b): + return hashlib.sha256(b).hexdigest() + + +def git(*args): + return subprocess.check_output(['git', *args]) + + +def predicted_workflow(base): + text = base.decode() + anchor = ' # Act 42. Two shards run on every event;' + job = (' probes_oichannel1:\n' + ' name: Numerical probes / OI channel protocol\n' + ' runs-on: ubuntu-latest\n' + ' steps:\n' + ' - uses: actions/checkout@v4\n' + ' with:\n' + ' fetch-depth: 0\n' + ' - uses: actions/setup-python@v5\n' + ' with:\n' + " python-version: '3.11'\n" + ' - name: Exact channel and cone controls\n' + ' run: python3 -I -B verification/lean/oi_channel1_check.py\n' + ' - name: Audit control mutation tests\n' + ' run: python3 -I -B '+ROUND+'controls.py --self-test\n\n') + replacements = [ + (anchor, job + anchor), + ('probes_kt4prem1, probes_a42_witness', 'probes_kt4prem1, probes_oichannel1, probes_a42_witness'), + (' KT4PREM1_RESULT: ${{ needs.probes_kt4prem1.result }}\n', + ' KT4PREM1_RESULT: ${{ needs.probes_kt4prem1.result }}\n' + ' OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }}\n'), + (' echo "kt4prem1=${KT4PREM1_RESULT}"\n', + ' echo "kt4prem1=${KT4PREM1_RESULT}"\n' + ' echo "oichannel1=${OICHANNEL1_RESULT}"\n'), + (' test "${KT4PREM1_RESULT}" = success\n', + ' test "${KT4PREM1_RESULT}" = success\n' + ' test "${OICHANNEL1_RESULT}" = success\n'), + ] + for old, new in replacements: + if text.count(old) != 1: + raise ValueError('workflow splice anchor is not unique') + text = text.replace(old, new) + return text.encode() + + +def failures(files, original, freeze, output, stderr, rc, result_required): + errors = [] + if sha(files.get(PROBE, b'')) != PROBE_SHA: + errors.append('P') + if files.get(WORKFLOW) != predicted_workflow(original[WORKFLOW]): + errors.append('W') + for path in original: + if path != WORKFLOW and files.get(path) != original[path]: + errors.append('L') + if files.get(ROUND+'preregistration.md') != freeze: + errors.append('F') + control_hash = re.search(r'^Controls SHA256: ([0-9a-f]{64})$', freeze.decode(), re.M) + if not control_hash or sha(files.get(ROUND+'controls.py', b'')) != control_hash.group(1): + errors.append('C') + expected = {'preregistration.md', 'controls.py'} | ({'result.md'} if result_required else set()) + actual = {p[len(ROUND):] for p in files if p.startswith(ROUND)} + if actual != expected: + errors.append('R') + if rc or stderr or sha(output) != OUTPUT_SHA: + errors.append('V') + if result_required: + result = files.get(ROUND+'result.md', b'').decode() + if result.count('Outcome: OI-CHANNEL-1-READ') != 1 or result.count(READING) != 1: + errors.append('S') + if 'CHANNEL-CHECK: PASS; 17 checks; 140 matrix-unit cases' not in result: + errors.append('S') + rest = result.replace(READING, '').lower() + if any(x in rest for x in ('establishes unconditional', 'kernel-certified', 'sources h3', + 'full-model independence established', 'oi implies qm')): + errors.append('S') + return sorted(set(errors)) + + +def self_test(probe_path, workflow_path): + probe = Path(probe_path).read_bytes() + base = Path(workflow_path).read_bytes() if workflow_path else git('show', D+':'+WORKFLOW) + proc = subprocess.run([sys.executable, '-I', '-B', probe_path], capture_output=True) + original = {WORKFLOW: base, 'kernel-source': b'unchanged kernel'} + freeze = ('frozen prospective scope\nControls SHA256: '+sha(b'controls')+'\n').encode() + files = {PROBE: probe, WORKFLOW: predicted_workflow(base), 'kernel-source': original['kernel-source'], + ROUND+'preregistration.md': freeze, ROUND+'controls.py': b'controls', + ROUND+'result.md': ('Outcome: OI-CHANNEL-1-READ\n'+READING+ + '\nCHANNEL-CHECK: PASS; 17 checks; 140 matrix-unit cases\n').encode()} + def run(f, out=proc.stdout, err=proc.stderr, rc=proc.returncode): + return failures(f, original, freeze, out, err, rc, True) + if run(files): + raise ValueError('positive fixture fails '+str(run(files))) + mutations = [(PROBE, b'changed', 'P'), (WORKFLOW, base, 'W'), ('kernel-source', b'changed', 'L'), + (ROUND+'preregistration.md', b'changed', 'F'), (ROUND+'extra', b'extra', 'R'), + (ROUND+'result.md', b'overstated result', 'S'), (ROUND+'controls.py', b'changed', 'C'), + (ROUND+'result.md', files[ROUND+'result.md']+b'It establishes unconditional reconstruction.', 'S')] + for path, value, code in mutations: + changed = dict(files); changed[path] = value + if code not in run(changed): + raise ValueError('mutation missed '+code) + for out, err, rc in [(b'PASS', b'', 0), (proc.stdout, b'error', 0), (proc.stdout, b'', 1)]: + if 'V' not in run(files, out, err, rc): + raise ValueError('output mutation missed V') + print('controls self-test: PASS; positive fixture and 11 mutations') + + +def check(head, freeze): + paths = [WORKFLOW, 'verification/lean-mathlib/OIBridge/OperationalValidity.lean', + 'verification/lean-mathlib/OIBridge/ImplementationLocality.lean'] + original = {p: git('show', D+':'+p) for p in paths} + names = git('ls-tree', '-r', '--name-only', head, '--', ROUND).decode().splitlines() + files = {p: git('show', head+':'+p) for p in set(paths+[PROBE]+names)} + fixed = git('show', freeze+':'+ROUND+'preregistration.md') + execution = git('diff', '--name-only', D, head).decode().splitlines() + allowed = {PROBE, WORKFLOW, ROUND+'preregistration.md', ROUND+'controls.py', ROUND+'result.md'} + if not set(execution) <= allowed: + raise ValueError('G: changed path outside scope') + frozen = git('diff', '--name-only', D, freeze).decode().splitlines() + if frozen != [ROUND+'preregistration.md']: + raise ValueError('G: freeze delta is not the preregistration alone') + on_disk = Path(PROBE).read_bytes() + if on_disk != files[PROBE]: + raise ValueError('P: local probe differs from checked object') + if Path(__file__).read_bytes() != files[ROUND+'controls.py']: + raise ValueError('C: running controls differ from checked object') + proc = subprocess.run([sys.executable, '-I', '-B', PROBE], capture_output=True) + required = ROUND+'result.md' in files + failed = failures(files, original, fixed, proc.stdout, proc.stderr, proc.returncode, required) + if failed: + raise ValueError('controls failed: '+','.join(failed)) + print('controls: PASS') + sys.stdout.write(proc.stdout.decode()) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('head', nargs='?') + parser.add_argument('--freeze') + parser.add_argument('--self-test', action='store_true') + parser.add_argument('--probe', default=PROBE) + parser.add_argument('--workflow') + args = parser.parse_args() + try: + if args.self_test: + self_test(args.probe, args.workflow) + elif args.head and args.freeze: + check(args.head, args.freeze) + else: + parser.error('head and --freeze, or --self-test, required') + except (ValueError, subprocess.CalledProcessError) as exc: + print(str(exc), file=sys.stderr) + sys.exit(1) diff --git a/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/preregistration.md b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/preregistration.md new file mode 100644 index 000000000..05118f61d --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/preregistration.md @@ -0,0 +1,147 @@ +# OI-CHANNEL-1 — channel protocol and transfer-boundary audit + +Status: candidate freeze, native V3 draft. Owner authorization to prepare the research and +PR sequence: 2026-10-11. This file is drafted from D on one PR under AGENTS.md section A.39. +It becomes a freeze only after an exact-head all-green workflow run and the owner's +designation of F. Execution follows F; E and the final receipt require their own checks. +No owner designation is inferred from the instruction to proceed. + +```v3-round +round OI-CHANNEL-1 +kind non-sealing +record-directory verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/ +``` + +```v3-governed-paths +record AM verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/ +record AM verification/receipts/OI-CHANNEL-1.json +execution A verification/lean/oi_channel1_check.py +execution M .github/workflows/verify.yml +``` + +D: 9f9f8257a980a1819fbbc1dc0019917cf8678626. +The delta from D to F is this preregistration alone. F and E are exact objects the owner +designates after their exact-head workflow attestations, not synthetic pull-request merges. + +## The bounded package + +The audit promotes saved exact evidence for the stopped repeat-until-success circuit and +its cone controls, plus a separately labelled written dependency assessment. It adds no +Lean module and proves no new theorem in the kernel. It neither adopts nor sources H2, +H3, A_miss, arbitrary-cone channel transfer, or a closure of exact availability. No +manuscript, ROADMAP, census registry, kernel source, legacy record or other round's +record changes. The historical research archives are cited, not imported into main. + +Research provenance: research/round7-channel-audit at +e7d380fcb9881e3063243aaa149e85be3cd0a914, research/round7-channel/ and +research/AUDITS/2026-10-11-round6/. Round-7 registration preceded the first saved run at +78aa5b25415cf1cd26994cb2280343ab86cd72d9. The prior review's circuit computations and +this batch's successful runs are exploratory evidence, disclosed before this freeze; +their outputs are not presented as blind predictions. + +## Frozen files + +The files are read from e7d380fcb9881e3063243aaa149e85be3cd0a914 and added byte for byte +during execution under the names below. + +| source in research/round7-channel/ | execution destination | SHA256 | +|---|---|---| +| channel_check.py | verification/lean/oi_channel1_check.py | 9937b6ffca6cf570cf7e1c3267ba1525ead48ada4d5f1e92959ec0f603baebff | +| native-controls.py | record directory controls.py | 76b7b76acd6115a7a1bd342859d4d38b4b246a9cab76b0e2e38c3b6bde0b25d7 | +| predicted-verify.yml | .github/workflows/verify.yml | bd71bdc270753be8296c4a5c9723e23673c2f8acdaa9417fb70a6ddd6cbe2443 | + +Controls SHA256: 76b7b76acd6115a7a1bd342859d4d38b4b246a9cab76b0e2e38c3b6bde0b25d7 + +The original workflow at D has SHA256 +c31d34ac7f15f2a0f37e7d64592b5ff102381d0fa30fc5bdf5d864ca03e6f185. +The predicted workflow changes only five splices: one OI-channel shard before Act 42, +its addition to the aggregate needs list, and its result environment variable, echo and +required success test. The new shard uses Python 3.11 and no third-party dependency, +runs the exact checker and the controls' mutation tests, and fetches complete Git history. +The frozen controls reconstruct all five splices from D and compare the bytes. + +## Questions and decision rules + +| question | evidence checkpoint | earned reading when checkpoint passes | +|---|---|---| +| Does the actual circuit realize the stopped channel formula? | U, RESET, BRANCH, TP, TOKEN, PAIR, DICT, J; all exact; depths k=0,...,6 | finite exact identities; general-k recurrence written separately | +| Does the defect-cone countercontrol remain valid? | ZF, CC-ID, CC-CLIFFORD | normalized matrix-trace witnesses -1/10 and -1/8; construction-level obstruction | +| Do the control cones distinguish the assumptions used? | OCT, OPEN, KAPPA; exact examples and separate written arguments | 24 Clifford target actions versus Phi_1; closedness used by the limit; expanded block cone fails self-duality and maxCone | +| Do the protocol countercontrols discriminate wrong constructions? | CC-Z, CC-OUTCOME, CC-RESET | omitted correction, wrong success outcome and missing reset rejected | +| Are the availability, transfer and self-duality boundaries preserved? | unchanged kernel definitions, frozen earned reading and scoped result note | sources remain OPEN; no upgrade from finite evidence to a kernel proof or full-model independence | + +The checker reads no file, imports no thread code, uses Gaussian rational arithmetic +from the standard library, and prints the 17 named check groups. The exact stdout +SHA256 is ec73839a23e1c2e051140ff9b56d47bbda4f9b55e37963ca1256500b36642da5, +stderr empty, exit 0. Its final line is: +CHANNEL-CHECK: PASS; 17 checks; 140 matrix-unit cases +Any changed stdout, nonempty stderr, failing check or nonzero status voids the reading. + +## Written reading and non-inferences + +The result note contains this exact earned reading, once: + +The finite stopped circuit realizes the channel formula at depths 0 through 6 by exact arithmetic. The all-depth recurrence and the universal cone arguments are written proofs. Transfer to an arbitrary pair cone and the general-k InstAvail witness remain additional obligations. This audit does not establish unconditional quantum reconstruction or full-model independence. + +The note states Phi_0=id and Phi_(k+1)=S0+Phi_k composed with F0, with S0=(5/8)Ad(D0) +and F0=(3/8)id, where D0=diag(1,(3+4i)/5). The all-depth formula follows by written +induction. Limits use closedness of the invariant cone, not exact availability of D0. +On closed convex K, the sequence-preservation and D0-preservation directions are written +separately; neither is labelled kernel-certified. + +The broader channel-transfer clause remains an additional hypothesis. I4.66 preserves +PSD matrix states and I4.38 derives that validity from implementation locality. Extending +it to an arbitrary pair cone requires validity on an identified pair state space C and +C=dict '' K, plus the context and label premises for the spectator step. At C=PSD, +this identification is K=Q3, so it is excluded as an independent source. + +KAPPA has a negative test on a product vector and fails the maxCone upper bound. It is a +control for the stated H1, H2 and target-channel hypotheses, not a full OI countermodel. +The 118 reached inventory rows and the 68 NOT REACHED rows are kept distinct. The latter +remain unresolved. H3's possible replacement by cone structure and maxCone, given H2 and +A_miss, is a separate proof question, not a result certified by this audit. + +## Invariants and checkpoints + +| invariant | measurement | +|---|---| +| probe and controls unchanged from the frozen sources | P and C SHA256 checks | +| exactly the five frozen workflow splices | W byte comparison with reconstructed D workflow | +| I4.66, I4.38 and their source modules unchanged | L object-byte checks of OperationalValidity and ImplementationLocality at D and the checked execution | +| preregistration unchanged after F | F object-byte check; V3 control-plane immutability | +| exact record population and bounded changed paths | R and G controls; V3 governed-path verification | +| expected exact output and no hidden errors | V checksum, stderr and return code | +| scoped earned reading, outcome and summary line | S control; review of the separate written statements | +| controls reject mutations | positive fixture plus 11 mutations in controls --self-test | + +The mutations change the probe, workflow, landed source, preregistration, record population, +earned reading, controls, appended overclaim, stdout, stderr and exit status. All must be +rejected by their named control. No success verdict is printed over a failed control. + +## Design evidence and stages + +Saved checker run 1 and its replay are byte-identical: 17/17 PASS, 140 matrix-unit cases, +five negative controls discriminating the stated faults. The frozen controls pass their +positive fixture and 11 mutations. Python parsing passes for both scripts. + +Separately, disposable design 13ad14a1ba2973245354aea7790c021d946b1ff0 repairs the +missing ComplexOrder scope in BridgeChannelTransfer. Run 38162504147, Mathlib job +114538184326: Build successful, seven standard axiom reports, lean-axioms 6136 with no +sorryAx; release gate failed at lean-manuscript with 12 undispositioned design modules. +This is design evidence only. This round adds none of those Lean modules. + +1. Before F: hold the control-plane branch at the proposed F, dispatch verify.yml on + that exact head, and record an all-green run before requesting the owner's designation. +2. S1 after the owner's F designation: add the three frozen files in one linear + commit. Run controls HEAD --freeze F and the mutation tests; CI must pass. +3. S2: add result.md with Outcome: OI-CHANNEL-1-READ, the frozen earned reading, the + checker's final line, written arguments at their labels and exact evidence pointers. + Run controls HEAD --freeze F; obtain an all-green exact-head run and the owner's E + designation. No unrelated main history enters before E. +4. Reconcile if needed, build the native receipt, and require v3_verifier --verify-round Q + to print VERDICT HOLDS before ordinary review and merge. + +A failed frozen checker or control halts this round under V3 S12 rather than changing the +decision rule after F. A valid read is a consistency-axis audit; it sources no premise and +does not complete the OI-to-QM research programme. Later proof packages follow their own +scopes, freezes, exact-head attestations and owner approval. diff --git a/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/result.md b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/result.md new file mode 100644 index 000000000..743ac740c --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/result.md @@ -0,0 +1,211 @@ +# OI-CHANNEL-1 audit result + +Outcome: OI-CHANNEL-1-READ + +Evidence classes: [X] denotes an exact saved computation, [W] a written argument, +and [D] disposable design validation. This package adds no Lean theorem or new +reconstruction premise. Its preregistration remains byte-identical to F. + +## Earned reading + +The finite stopped circuit realizes the channel formula at depths 0 through 6 by exact arithmetic. The all-depth recurrence and the universal cone arguments are written proofs. Transfer to an arbitrary pair cone and the general-k InstAvail witness remain additional obligations. This audit does not establish unconditional quantum reconstruction or full-model independence. + +## Exact execution checkpoint [X] + +The native controls passed at S1 2d870fc508cbf2d0f74d7681a8546a694eaef92b: +exit 0, empty stderr, all 17 groups PASS. TOKEN covers 28 matrix-unit cases and +PAIR 112 at depths 0 through 6. DICT separately covers 112 Pauli table cases; +J covers 16. The five countercontrols reject omitted correction, the wrong +success outcome, missing reset, identity and a target Clifford action in the +stated constructions. The controls' positive fixture and all 11 mutations pass. + +CHANNEL-CHECK: PASS; 17 checks; 140 matrix-unit cases + +The checker stdout SHA256, excluding the native controls' own prefix, is +`ec73839a23e1c2e051140ff9b56d47bbda4f9b55e37963ca1256500b36642da5`. +The original design run and replay were byte-identical. The probe, controls and +workflow have the exact SHA256 values in the preregistration; the unchanged +kernel-source check and all five workflow splices pass the native controls. + +ZF's normalized matrix-trace witnesses are -1/10 for the drive and -1/8 for +the mixer. These values are matrix traces. Under the Pauli dictionary the +unscaled table inner product is four times the matrix trace; the trace +normalization is kept explicit. + +The cone for ZF is the historical +`K(Z_F) = (Q3 intersect Z_F*) + cone(Z_F)`, recorded in +[R6 NOTES, N2](https://github.com/amaybaum/incompleteness/blob/e7d380fcb9881e3063243aaa149e85be3cd0a914/research/archive/pt/R6/NOTES.md) +and used by [B4's realization, sections 1 and 2](https://github.com/amaybaum/incompleteness/blob/5f4089a4500a59943c33ba13656b2530824068c5/research/bridge/NOTES-B4.md). +Under the Pauli dictionary this cone is contained in the sum of the PSD cone +and the conic hull of the four defect matrices used by ZF. A PSD test has +nonnegative trace pairing with every PSD matrix; if it also has nonnegative +pairing with each defect, linearity gives nonnegative pairing with every +element of that sum and hence with all of K(Z_F). This sufficiency argument +is [W]; ZF's exact rank-one tests and four generator inequalities are [X]. +B4's realization retains its conditional branch-(a) scope; this citation +does not extend it to the unreached inventory rows. + +## Provenance and certification boundary + +- D: `9f9f8257a980a1819fbbc1dc0019917cf8678626`. +- F: `a5aad0c1c52df963f8d1365479e4c6f1a0305de0`. +- Owner-designation F: recorded in S1's commit message and PR #808's description, + from the owner's in-session approval on 2026-10-11T19:15:22Z. +- F check-run: [verify #1891](https://github.com/amaybaum/incompleteness/actions/runs/38164920166), + workflow_dispatch at F, attempt 1, all 33 jobs successful. +- Frozen sources and original exact evidence: `e7d380fcb9881e3063243aaa149e85be3cd0a914`, + `research/round7-channel/`; prospective registration: + `78aa5b25415cf1cd26994cb2280343ab86cd72d9`. +- Written-argument source: `research/round7-channel/ARGUMENT.md` at that frozen + research source. Its mathematical arguments are restated below with their + evidence classes retained. +- S1: `2d870fc508cbf2d0f74d7681a8546a694eaef92b`, one linear child of F, + adding the three frozen files. Its PR-triggered CI is a stage checkpoint, + and is not used as an F or E exact-head attestation. +- S1 stage CI: [verify #1892](https://github.com/amaybaum/incompleteness/actions/runs/38167557092), + pull_request event at S1, 19 jobs successful and the A42 exclusion matrix + intentionally skipped. The OI channel job passes its exact 17-group, + 140-case checker and the controls' positive fixture plus 11 mutations. +- E's exact-head check-run and owner designation must be recorded on the host + and in the later native receipt. This result note precedes those events; + it does not infer them from a pull-request run. + +Separate [D] evidence: the ComplexOrder scope repair at +`13ad14a1ba2973245354aea7790c021d946b1ff0`, PR #807, built successfully in +[run 38162504147](https://github.com/amaybaum/incompleteness/actions/runs/38162504147), +Mathlib job 114538184326. Its seven BridgeChannelTransfer axiom reports use +only propext, Classical.choice and Quot.sound. The 6136-result axiom census +passed with no sorryAx; the release gate failed on 12 missing design-module +manuscript dispositions. No design Lean module is imported by this audit. + +The historical inventory's 118 reached rows, 13 FAILS rows and 68 NOT REACHED +rows remain distinct. The 68 unreached rows are unresolved. The expanded +block cone below fails the maxCone product-effect bound and is not a full OI +countermodel. The transfer premise, pair self-duality and general-k formal +availability remain additional obligations; no source of these premises is +adopted by this package. + +I4.38 derives the PSD-validity reading from implementation locality. Extending +I4.66 to a pair state space also requires the operational context and label +premises for the spectator step, in addition to validity on the identified +space. Those premises are retained as obligations. + +## Written arguments [W] and finite witnesses [X] + +Evidence: `channel_check.py`, run 1 and byte-identical replay, 17 checks PASS. +The computations below are [X]; arguments over all depths or all inputs are [W]. +None constructs a Lean `InstAvail` witness. The class membership of each primitive +must still be supplied by the operational model when using this circuit as an +availability witness. + +### Finite stopped protocols + +Use data register a and ancillas b,c, prepared in 00. Hadamard acts on the +ancillas, Toffoli flips a when bc=11, and S=diag(1,i) acts on a. The circuit is +`(I tensor H tensor H) Toffoli (S tensor I tensor I) Toffoli (I tensor H tensor H)`. +The checker uses unnormalized Hadamard matrices and divides the final matrix by +4, so every entry is Gaussian rational; U checks its unitarity independently. + +Readout followed by conditional bit flips prepares 00 from the uniformly +attached four-state ancilla: the reset Kraus maps are |00><00|. RESET checks this step; attachment alone +does not prepare the circuit's input, as CC-RESET verifies. + +The successful branch is ((3+i)/4) D, with D=diag(1,(3+4i)/5), and has weight +5/8. Each other branch has weight 1/8 and is proportional to Z; applying Z +after failure restores the data, up to a scalar. BRANCH and TP check all four +matrices and their normalization. CC-Z and CC-OUTCOME reject omitted correction +and mistaking a failure outcome for success. + +Let S0=(5/8) Ad(D) and F0=(3/8) id be the success and corrected-failure maps. +The protocol stops at its first success, or returns the corrected data after k +failures. Its recurrence is Phi_0=id and Phi_(k+1)=S0+Phi_k composed with F0. +Induction therefore gives, for every integer k>=0, + +`Phi_k=(1-(3/8)^k) Ad(D)+(3/8)^k id`. + +The saved computation rebuilds this recurrence from the branch matrices, +independently of the formula, on all matrix units for k=0,...,6: TOKEN has 28 +cases and PAIR has 112. DICT checks the Pauli dictionary separately; J checks +the mixer and its cyclic action. This protocol differs from unconditionally +composing Phi_1 with itself: that would apply D again after success. + +All finite protocols use only attachment, reset/readout and feed-forward, +available primitive unitaries, composition, coarse-graining and discard. This +is a written construction in the `InstAvail` vocabulary; the general-k Lean +witness remains OPEN. Finite exact checks do not discharge that obligation. + +### The limit and its transfer premise + +The failure weight tends to zero, so Phi_k tends pointwise to Ad(D). If K is +closed and every transferred Phi_k preserves K, its limit preserves K: for +each omega in K, the convergent images stay in K. Availability of the limit is +not used. Conversely, if K is convex and Ad(D) preserves K, each Phi_k +preserves K by its displayed convex combination with the identity. These two +written implications show that requiring this specific sequence to preserve +a closed convex K has exactly the same invariance content as requiring D to +preserve it. Each direction is a written proof [W]; this audit adds no Lean theorem for the equivalence. + +The broader transfer clause for every available channel is a separate premise. +I4.66 at main 9f9f8257 quantifies over PSD matrix states. To apply it to K one +needs the identification of a pair state space C with dict '' K and validity +on C. If C is the PSD state space, the identification is K=Q3, the conclusion. +The limit route therefore does not supply an independent source of transfer. + +### Cone controls + +OCT uses K_oct={omega: omega b lies in the Lorentz cone for every b=(1,+/-e_i)}. +It is closed and convex, contains every product of Lorentz-cone vectors, and +is invariant under target proper signed permutations, which permute the six +tests. The finite test permutation check exhausts all 24 such rotations. +The table e0 tensor (1,1,1,1) belongs. Phi_1 maps its target spatial vector to +(1/4,5/4,1); pairing with (1,0,-1,0) gives -1/4, outside K_oct. Thus these 24 +unitary actions and the transferred Phi_1 have different preservation content. +This control alone does not classify every available unitary with arbitrary +dilations in MixR. + +OPEN uses the cone over the open unit disc plus its boundary point (1,0), +embedded in span{e00,e01,e02}, with its apex included. This is a convex cone +and is not closed. For p=(3/8)^k, k>=1, the target-plane map has squared norm +factor 1-(4/5)p(1-p)<1, so it sends the distinguished boundary point and every +interior point into the disc. Phi_0 is the identity. The limiting image of +(1,0) is (3/5,4/5), a different boundary point, excluded from the cone. +The scope is the sequence Phi_k; preservation by every available channel is +not asserted. Closedness cannot be removed from this limit argument. + +KAPPA uses block matrices [[A,B],[B*,D0]] with A,D0 PSD and +||B||_1 <= kappa sqrt(tr(A) tr(D0)), kappa>1. The constraint is closed and +convex: the geometric mean is concave on nonnegative arguments, while the +trace norm is convex. Every product PSD matrix obeys it because positivity of +the first token gives |r01|<=sqrt(r00 r11). CNOT controlled on the first token +sends D0 to X D0 X and B to B X, preserving the traces and trace norm. +Every target CPTP channel preserves it. To see the trace-norm contraction, +write B=sum_s b_s |u_s>-|10>, so it strictly +contains Q3. KAPPA checks both exact witnesses. Thus closedness, products, +CNOT invariance and all target-channel invariance do not by themselves give +self-duality. The universal statements here are [W], not Lean proofs. + +This quadratic test is a product vector, so the expanded cone also violates +the maxCone product-effect upper bound. It is a control for the listed H1, +H2 and target-channel hypotheses, not a full OI countermodel. A possible +replacement of H3 by cone structure and maxCone, given H2 and A_miss, requires +a separate argument: the dual cone inherits the inverse unitary actions, +contains the product tests, and the pure-orbit result can then constrain both +cones. That question is proposed for the next conditional-pair proof; no +kernel claim for that replacement is made in this batch. + +### Remaining reconstruction work + +Source the transfer premise, source pair self-duality, and formalize the +general finite-protocol availability witness. Full-model independence remains +OPEN because the 68 NOT REACHED inventory rows are unresolved. Subsequent +milestones are elementary-token geometry, the conditional pair theorem, +arbitrary finite composites and operation/measurement equivalence. No result +here proves unconditional OI implies quantum mechanics. diff --git a/verification/receipts/OI-CHANNEL-1.json b/verification/receipts/OI-CHANNEL-1.json new file mode 100644 index 000000000..a68b041b0 --- /dev/null +++ b/verification/receipts/OI-CHANNEL-1.json @@ -0,0 +1,67 @@ +{ + "schema": "v3-receipt", + "version": 1, + "round": "OI-CHANNEL-1", + "status": "complete", + "kind": "non-sealing", + "object_format": "sha1", + "d": "9f9f8257a980a1819fbbc1dc0019917cf8678626", + "f": "a5aad0c1c52df963f8d1365479e4c6f1a0305de0", + "control_plane_blobs": [ + { + "path": "verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/preregistration.md", + "blob": "05118f61d7be7d09a39d619439570cb41254e00b" + } + ], + "governed_paths_digest": "73dbd9ba84a5a55db1f04c449f687d6c11d8dc03c019de8c9ad301bdeb681f63", + "e": "d84536837b591de4601e09dada57a4e565db34c7", + "tree_e": "979892a133da17ac92d3d1b9360001d60692f7a0", + "execution_delta_digest": "91fc8d010dc146c1b19200330dbec65fd207f6b37fd972be6b44c1df6a26bd4d", + "candidates": [ + { + "commit": "2d870fc508cbf2d0f74d7681a8546a694eaef92b", + "tree": "150b151d47ebaa4756f12c825bf6e011c78704c2", + "measured": "S1 native controls PASS; frozen stdout checksum, 17 groups and 140 matrix-unit cases; positive fixture and 11 mutations PASS; PR verify 38167557092 success (19 successful jobs, intentional A42 matrix skip)." + }, + { + "commit": "d84536837b591de4601e09dada57a4e565db34c7", + "tree": "979892a133da17ac92d3d1b9360001d60692f7a0", + "measured": "S2 native controls PASS, frozen stdout checksum, empty stderr, exit 0; 17 groups and 140 matrix-unit cases. Exact-head workflow_dispatch 38168537087, attempt 1, all 34 jobs successful and no skips; OI mutation self-test PASS." + } + ], + "landing": { + "base": "9f9f8257a980a1819fbbc1dc0019917cf8678626", + "object": "2f05823c038d2142f3178ce3aa9f3adbad643cfc", + "reconciliations": [ + "2f05823c038d2142f3178ce3aa9f3adbad643cfc" + ], + "resolved_paths": [], + "delta_digest": "72f426ee43d84efb41e4cb2c517865e6d9dd7f88ddac21d45bed4072b90ac625" + }, + "attestations": [ + { + "kind": "owner-designation", + "subject": "F", + "commit": "a5aad0c1c52df963f8d1365479e4c6f1a0305de0", + "record": "https://github.com/amaybaum/incompleteness/commit/2d870fc508cbf2d0f74d7681a8546a694eaef92b" + }, + { + "kind": "check-run", + "subject": "F", + "commit": "a5aad0c1c52df963f8d1365479e4c6f1a0305de0", + "record": "https://github.com/amaybaum/incompleteness/actions/runs/38164920166" + }, + { + "kind": "owner-designation", + "subject": "E", + "commit": "d84536837b591de4601e09dada57a4e565db34c7", + "record": "https://github.com/amaybaum/incompleteness/commit/2f05823c038d2142f3178ce3aa9f3adbad643cfc" + }, + { + "kind": "check-run", + "subject": "E", + "commit": "d84536837b591de4601e09dada57a4e565db34c7", + "record": "https://github.com/amaybaum/incompleteness/actions/runs/38168537087" + } + ] +}