diff --git a/research/selected-linear-cnot-cancellation/PROOF.md b/research/selected-linear-cnot-cancellation/PROOF.md new file mode 100644 index 0000000000..12f18c6db0 --- /dev/null +++ b/research/selected-linear-cnot-cancellation/PROOF.md @@ -0,0 +1,88 @@ +# Twenty-five CNOTs for the selected left binary map + +Claim type: an exact finite word certificate and a scoped all-column proof. +This contribution was produced by Nick Petalas. Apache-2.0. + +## Source and new step + +Jerry Chen / CubeJerry's [PR #7430](https://github.com/CrocSwap/integer-mult-bounds/pull/7430), +head `39b40c465f7636a4bb6d70af28595fe8f70f4f3f`, binds the left binary +factor of selected MOVE24472 to the matrix with row masks + +```text +G = (3, 5, 9, 17, 32, 65, 129, 1, 256). +``` + +Bit i in a row mask is the coefficient of input coordinate i. Thus + +```text +Gx = (x0+x1, x0+x2, x0+x3, x0+x4, x5, + x0+x6, x0+x7, x0, x8), +``` + +where every addition is in F2. That source's +[MATRICES.json](https://github.com/CubeJerry/integer-mult-bounds/blob/39b40c465f7636a4bb6d70af28595fe8f70f4f3f/research/literal-selected-linear-maps/MATRICES.json) +records a 27-gate left word. Gate pairs are `(target, control)` in temporal +order, with action `x[target] ^= x[control]`. + +The new step removes its adjacent gates at zero-based positions 5 and 6. +Both are `(1,0)`. For `E=I+e1 e0^T`, the scalar product `e0^T e1` is zero, +so `E^2=I` over F2. The full product is therefore unchanged after removing +this adjacent pair. This elementary involution identity is classical; the +contribution is its application to this specified word and the shorter +explicit certificate. + +The resulting 25-gate temporal word is + +```text +(7,0) (6,0) (4,0) (3,0) (2,0) +(0,1) (1,0) (2,1) (1,2) (2,1) +(3,2) (2,3) (3,2) (4,3) (3,4) +(4,3) (5,4) (4,5) (5,4) (6,5) +(5,6) (6,5) (7,6) (6,7) (7,6). +``` + +The verifier establishes this new word's matrix identity directly by row +addition from I, rather than relying on correctness of the predecessor's +word. A separate explicit-coordinate oracle checks its entire address +action. No predecessor executable is imported or replayed. + +## Every positive column multiplicity + +For any positive integer f, let each xi be an arbitrary vector in F2^f. +Apply every gate by componentwise XOR. A gate acts independently on each +bit column, so the new word is the direct sum of f copies of G under the +coordinate/column regrouping. The same cancellation holds at every column. +Consequently the map on all nine f-bit coordinates is exactly G, coordinate +8 is fixed, and reversing the word is its inverse. Any additional untouched +coordinates or payload indices remain fixed as well. + +Executing one coordinate CNOT at each column uses 25f elementary column +CNOTs, compared with the cited 27f. This saves exactly 2f such calls. This +is a gate-count statement, not an exact local tape instruction count. + +The endpoint equality also holds as a permutation of an arbitrary payload +array indexed by these addresses: every source address has the same image. +It does not supply a new physical staging, erasure or owner-return program. + +## Verification and limits + +The checker evaluates the new word on all 512 addresses at f=1 and all +262,144 addresses at f=2, including the inverse and the spectator at every +address. It also checks the exact nine-row matrix identity. Three controls +reject an extra deletion, reversed control directions, and a purported f=2 +implementation that only updates the first bit column. + +The all-f statement follows from the direct-sum proof above; the finite +censuses are corroboration. No minimum CNOT count is claimed. The right +factor, phase recipes, offset, central native operator and the selected +frontier are not improved here. Integrating the word into the literal tape +compiler, executing its new graph, and measuring complete instructions and +historical storage remain open. No physical speedup, supplier admission, +complete multiplication theorem, or new kappa is claimed. + +The selected five framework assumptions remain. Independent human and +formal proof-kernel review are unclaimed. The source's matrix/source binding, +27-gate comparison point, and literal implementation belong to Jerry Chen / +CubeJerry. Credit also its #3834, #5188, #6992 and retained native/compiler +lineage. Their results are cited premises, not validation deliverables here. diff --git a/research/selected-linear-cnot-cancellation/README.md b/research/selected-linear-cnot-cancellation/README.md new file mode 100644 index 0000000000..cdd0fc2def --- /dev/null +++ b/research/selected-linear-cnot-cancellation/README.md @@ -0,0 +1,89 @@ +# Remove two CNOTs from the selected left binary map + +**Exact finite certificate and scoped all-column proof; no new kappa.** +This contribution was produced by Nick Petalas. Apache-2.0. + +The left binary map of MOVE24472 has an explicit **25-CNOT word**, improving +the 27-CNOT word recorded by Jerry Chen / CubeJerry in +[PR #7430](https://github.com/CrocSwap/integer-mult-bounds/pull/7430) at +`39b40c465f7636a4bb6d70af28595fe8f70f4f3f`. Its adjacent gates 5 and 6 are +both `x1 ^= x0`; their composition is the identity. The shorter word is +printed and proved in [PROOF.md](PROOF.md). + +Its exact matrix has rows `(3,5,9,17,32,65,129,1,256)`. The identity holds +for every positive number f of binary columns and arbitrary payloads, +saving exactly 2f elementary column CNOT calls. Coordinate 8 and untouched +spectators remain fixed. This is the first strict word improvement found; +no shortest-word or additional synthesis claim is made. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/selected-linear-cnot-cancellation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/selected-linear-cnot-cancellation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/selected-linear-cnot-cancellation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/selected-linear-cnot-cancellation --check-source-history +``` + +Another CPython 3.12 path can replace the local interpreter. Direct replay +prints `PASS_SELECTED_LINEAR_CNOT_CANCELLATION` in a generated JSON receipt +bound to all six package source hashes. It writes nothing. It checks the +new matrix by row addition and the complete new forward/inverse maps by a +separate explicit-coordinate oracle: 512 addresses at f=1 and 262,144 at +f=2. Three malformed implementations are distinguished. No predecessor +executable or scientific suite is run. + +## Scope, provenance and overlap + +The selected baseline metadata check passed against main +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8, selected +#7000. [SOURCES.json](SOURCES.json) pins that orientation context. The new +word and target matrix are explicit package constants; replay does not +depend on the pending predecessor commit being present in Git history. +The cited source file fixes the comparison and target, rather than acting +as an undeclared executable input. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571878) +asks for the first shorter word. Live claims, open PRs, account history, +merged CNOT/24472 work and main README searches were checked. No overlapping +shorter word for this matrix was found. These bounded searches do not prove +literature novelty. Classical CNOT cancellation is not a new theorem. + +No literal tape graph is changed or executed here. Exact instruction counts, +whole-call staging, owner return, precision and complete MOVE composition +remain separate obligations. No selected frontier, recursive invoice or +five-framework-assumption claim changes. Credit Jerry Chen / CubeJerry's +#7430 and its #3834/#5188/#6992 native/compiler lineage. Independent human +and formal proof-kernel review are unclaimed. + +## Code bounds + +The checker has no recursion, network, subprocess or filesystem writes. +There are at most 27 gates and nine coordinates; the largest streamed +address domain has 262,144 elements. Only one nine-coordinate input/output +pair is live per iteration. Every function is under 60 physical lines. +Exception-based checks remain enabled under optimization. The source-hash +reader admits six fixed package files of at most 128 KiB each and assumes +the package stays stable during replay. Normal and optimized warning-strict +execution and AST inspection are the local diagnostics. + +Power-of-ten rule 3 deviation: CPython allocates integers, tuples and lists +during this offline finite checker. Fixed gate/address/file bounds and a +120-second registered timeout bound its work and live data. A fixed-storage +port is required before use in a steady service. No compiler configuration +or shared verifier code is changed. Build the Lever led to the rerunnable +word certificate; Prove It Works led to the separate complete-address oracle. + +## Open next questions + +1. Integrate the 25-gate word into #7430's literal compiler and obtain fresh + graph, full-array and history receipts. First replace only its frozen left + word and regenerate that graph. The complete literal replay and source + binder remain the blockers to claiming an instruction-count improvement. +2. Is 25 optimal for this exact matrix? First derive a gate-count lower bound + or run a separately budgeted bounded synthesis. This package stops at its + first strict improvement and supplies neither a search nor an optimum. + +[TASK.json](TASK.json) records the changed card and structured next questions. diff --git a/research/selected-linear-cnot-cancellation/SOURCES.json b/research/selected-linear-cnot-cancellation/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/research/selected-linear-cnot-cancellation/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/selected-linear-cnot-cancellation/TASK.json b/research/selected-linear-cnot-cancellation/TASK.json new file mode 100644 index 0000000000..8deb96dc01 --- /dev/null +++ b/research/selected-linear-cnot-cancellation/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "An explicit 25-CNOT word for the selected MOVE24472 left binary map, improving the cited 27-gate word, with a scoped all-positive-column proof.", + "scope_change_reason": "The formal-interface card is narrowed to a constructive finite binary-map side result. No proof assistant or all-size physical caller binding is claimed.", + "bottleneck_link": "The selected native monomial needs this exact binary permutation. Two adjacent identical CNOTs can be removed, reducing its elementary gate passes before physical compiler integration.", + "budget_minutes": 60, + "stop_rule": "Ship the first strict verified gate-count improvement; do not extend synthesis.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: exact matrix identity, complete forward/inverse f=1 and f=2 address censuses, three controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What exact literal tape instructions and history does the shorter word save?", + "why_it_matters": "Gate counts alone do not supply the complete physical bill.", + "first_step": "Replace the left frozen word in PR7430 and regenerate its literal graph and full-array receipts.", + "blocked_by": "No updated literal compiler graph or full tape execution is supplied." + }, + { + "question": "Is the 25-CNOT word optimal for this exact matrix?", + "why_it_matters": "A lower bound would distinguish a strict improvement from a shortest word.", + "first_step": "Derive a source-specific lower bound or budget a bounded synthesis.", + "blocked_by": "This package stops at the first improvement and runs no optimal synthesis." + } + ] +} diff --git a/research/selected-linear-cnot-cancellation/VERIFY.json b/research/selected-linear-cnot-cancellation/VERIFY.json new file mode 100644 index 0000000000..896a3a1a6d --- /dev/null +++ b/research/selected-linear-cnot-cancellation/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new matrix identity; complete f=1 and f=2 address and inverse maps; spectator preservation; three rejection controls; generated source-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new matrix identity; complete f=1 and f=2 address and inverse maps; spectator preservation; three rejection controls; generated source-hash receipt." + } + ] +} diff --git a/research/selected-linear-cnot-cancellation/verify.py b/research/selected-linear-cnot-cancellation/verify.py new file mode 100644 index 0000000000..52141a67f5 --- /dev/null +++ b/research/selected-linear-cnot-cancellation/verify.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Certify the shorter selected left-map word; standard library, no writes.""" + +import hashlib +import json +from pathlib import Path + + +TARGET = (3, 5, 9, 17, 32, 65, 129, 1, 256) +# Temporal order; each pair means row[target] ^= row[control]. +WORD = ( + (7, 0), (6, 0), (4, 0), (3, 0), (2, 0), + (0, 1), (1, 0), (2, 1), (1, 2), (2, 1), + (3, 2), (2, 3), (3, 2), (4, 3), (3, 4), + (4, 3), (5, 4), (4, 5), (5, 4), (6, 5), + (5, 6), (6, 5), (7, 6), (6, 7), (7, 6), +) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def word_matrix(word): + require(len(word) <= 27, "word exceeds the fixed certificate domain") + rows = [1 << i for i in range(9)] + for target, control in word: + require(0 <= target < 9 and 0 <= control < 9, "invalid coordinate") + require(target != control, "a CNOT needs two coordinates") + rows[target] ^= rows[control] + return tuple(rows) + + +def apply_word(coordinates, word): + require(len(coordinates) == 9, "nine coordinates required") + result = list(coordinates) + for target, control in word: + result[target] ^= result[control] + return tuple(result) + + +def direct_map(x): + """Separate, explicit coordinate oracle, without interpreting WORD.""" + return (x[0] ^ x[1], x[0] ^ x[2], x[0] ^ x[3], x[0] ^ x[4], + x[5], x[0] ^ x[6], x[0] ^ x[7], x[0], x[8]) + + +def check_complete_addresses(f): + require(f in (1, 2), "finite census is registered only for f=1,2") + mask = (1 << f) - 1 + count = 1 << (9 * f) + inverse = tuple(reversed(WORD)) + for address in range(count): + coordinates = tuple((address >> (f * i)) & mask for i in range(9)) + actual = apply_word(coordinates, WORD) + require(actual == direct_map(coordinates), "complete address mismatch") + require(actual[8] == coordinates[8], "spectator changed") + require(apply_word(actual, inverse) == coordinates, "inverse mismatch") + return count + + +def check_controls(): + require(word_matrix(WORD[1:]) != TARGET, "extra deletion escaped") + swapped = tuple((control, target) for target, control in WORD) + require(word_matrix(swapped) != TARGET, "control-direction mutant escaped") + x = (2, 0, 0, 0, 0, 0, 0, 0, 0) + low = apply_word(tuple(value & 1 for value in x), WORD) + first_column_only = tuple((x[i] & 2) | low[i] for i in range(9)) + require(first_column_only != direct_map(x), "one-column mutant escaped") + return 3 + + +def package_hashes(): + root = Path(__file__).resolve().parent + result = {} + for name in FILES: + require((root / name).stat().st_size <= 131072, "source exceeds cap") + data = (root / name).read_bytes() + require(len(data) <= 131072, "package source exceeds hash bound") + result[name] = hashlib.sha256(data).hexdigest() + return result + + +def main(): + require(len(WORD) == 25, "new gate count changed") + require(word_matrix(WORD) == TARGET, "matrix identity failed") + counts = {str(f): check_complete_addresses(f) for f in (1, 2)} + controls = check_controls() + print(json.dumps({ + "status": "PASS_SELECTED_LINEAR_CNOT_CANCELLATION", + "claim_type": "finite certificate and scoped all-column proof", + "new_left_gate_count": len(WORD), + "cited_predecessor_left_gate_count": 27, + "matrix_rows": TARGET, + "complete_addresses_and_inverse_checks": counts, + "rejected_mutants": controls, + "package_sha256": package_hashes(), + "no_new_kappa": True, + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()