[petalas]

Change and mathematical scope

Formal interface lemma; no new κ. Selected κ stays 0.001672660197076918. New package research/gate-operand-parity-lean/: an all-size, machine-checked Lean 4 proof of the exact gate-operand agreement contract at the pinned PR589 checker/exporter boundary, replacing the informal coefficient argument behind the bounded census of PR #3738 (which answered PR #3696 open question 1 in the #2977/#3004 cascade) with a kernel-checked theorem at the same hypotheses.

theorem GateParity.sym_eq_exp_iff_contract (d : Nat) (srcs : List Nat) :
    Contract d srcs ↔ ∀ v : Nat → Bool, sym d srcs v = exp d srcs v

with sym the checker's accumulate-then-write gate operator (xcheck_p.py lines 252-255: acc = 0; for s in srcs: acc ^= val[s]; val[d] ^= acc) and exp the exporter's one-sequential-ADD-per-source operator (export_records.py, run: for s in srcs: rec.append((1,d,s,1,f,ph))), both formalized line for line over v : Nat → Bool. The contract is:

d ∉ srcs ∨ ∃ p t, srcs = p ++ (d :: t) ∧ d ∉ t ∧ ∀ r, EvenCount (p.count r)

i.e. destination-free, or split at the destination's last occurrence with an all-even prefix (EvenCount (p.count d) is the odd-multiplicity clause) and no destination in the suffix.

Machine-checked, all sizes (Lean 4.21.0 core, no Mathlib): the main theorem, plus exp_dest_free (destination-free agreement — the case used by all 5,472 selected D/A/B/C gates), exp_split_d, allEvenCount_xfold (the pairing lemma) and xfold_indicator (supplies the divergent valuation when the contract fails). Kernel reports: main theorem [propext, Classical.choice, Quot.sound]; supporting lemmas [propext, Quot.sound]; no sorryAx.

Bounded corroboration (stdlib Python, registered command): an independent implementation of both operators and of the predicate requires agreement on all valuations to coincide with the contract for every (d, srcs) with 4 registers and lists of length ≤ 4 — 1,364 pairs, 708 agreeing, 656 diverging, 100 % match — on a domain disjoint from the published census domain (6 registers, length ≤ 4). Six rejection controls (a sorry, a dropped axiom report, a changed Contract body, a changed pinned operator line, a wrong predicate, a bad axiom report) must each be refused.

What this does not establish

No supplier, tariff, hosting, precision or selected-chain change; no new κ; no selected-frontier change. The Lean statement formalizes the two operators as functions; it does not replay the exporter/checker, and the record-stream/blast-radius counts remain PR #3738's and PR #3696's measurements. This is a boundary lemma, not a multiplication theorem.

Task and overlap

• Card formal-interface-lemma (independent-verification track), scope changed with the reason in TASK.json: the card's method is used directly, but the missing boundary lemma is taken from the live supplier-boundary cascade rather than the historical selected review.
• Base 20ecf2891d80b5acf18d980b2164fb44ea7faa90 (canonical main, fetched this round); priority revision 6.
• Overlap checked with scripts/find_overlap.py --task formal-interface-lemma and by reading the open PRs and the cascade packages; no open PR formalizes the gate-operand contract. PR Record the gate-operand agreement counts #3741 records the same census counts with a different (non-Lean) implementation; this package proves the all-size statement instead and does not re-run that census.

Validation

All commands from a repository root, CPython 3.12.15 (~/git/integer-mult-bounds/.venv/bin/python3.12) and Lean 4.21.0 (local, read-only):

python3.12 -B research/gate-operand-parity-lean/verify.py
python3.12 -B research/gate-operand-parity-lean/test_package.py
python3.12 -B research/gate-operand-parity-lean/verify.py --lean /opt/homebrew/bin/lean
python3.12 -B scripts/research_package.py --package research/gate-operand-parity-lean
python3.12 -B scripts/check_research_commit.py --package research/gate-operand-parity-lean --check-source-history

Expected:

PASS_GATE_OPERAND_PARITY_LEAN pins=2 targets=5 census_pairs=1364 census_agreements=708 census_divergences=656 contract_matches=1 lean_kernel=not_run
PASS_GATE_OPERAND_PARITY_LEAN_CONTROLS controls=6 positive_total=120
PASS_GATE_OPERAND_PARITY_LEAN_KERNEL ... lean=4.21.0 axioms=Classical.choice,Quot.sound,propext sorry_free=true
PASS_REGISTERED_RESEARCH_PACKAGE research/gate-operand-parity-lean outcome=completed
PASS_RESEARCH_COMMIT_BYTES {"commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", ...}

The registered command is standard-library only and does not claim Lean ran; the all-size kernel claim is certified by this PR's own gate-operand-parity-lean workflow, which downloads the checksum-pinned official Lean 4.21.0 release and runs kernel mode plus the controls. Its hosted result will be reported here once green.

Credit

Prepared by Nick Petalas with AI assistance. Predecessor credit: Wentao Li's PR #3696 (gate-operand export parity and its open question 1), the PR #2977/#3004 scatter cascade with the #2992/#3273/#3346 successors, PR #3738 (the bounded census and exact contract this package formalizes), eumemic's pinned symbolic checker and Dylan Crow's pinned record exporter. Apache-2.0.

CI result (reported after completion)

All checks on head 4c3530f42a6abcc48e7a6bcffd6c901911dc8269 are green:

• plan: pass.
• replay (research/gate-operand-parity-lean): pass — PASS_GATE_OPERAND_PARITY_LEAN pins=2 targets=5 census_pairs=1364 census_agreements=708 census_divergences=656 contract_matches=1 lean_kernel=not_run and PASS_REGISTERED_RESEARCH_PACKAGE research/gate-operand-parity-lean outcome=completed (Python 3.12).
• formal (gate-operand-parity-lean workflow, checksum-pinned official Lean 4.21.0): pass — PASS_GATE_OPERAND_PARITY_LEAN_KERNEL ... lean=4.21.0 axioms=Classical.choice,Quot.sound,propext sorry_free=true and PASS_GATE_OPERAND_PARITY_LEAN_CONTROLS controls=6 positive_total=120.

The all-size kernel claim is therefore certified by CI under the pinned toolchain on Linux; the local run under Lean 4.21.0 (macOS arm64) agrees.