diff --git a/research/three-block-cancellation-signature/PROOF.md b/research/three-block-cancellation-signature/PROOF.md new file mode 100644 index 0000000000..81e3a0a2a2 --- /dev/null +++ b/research/three-block-cancellation-signature/PROOF.md @@ -0,0 +1,144 @@ +# Cancellation adds a three-block signature + +This is a scoped algebraic proof. It answers Open next question 1 of +SHIN09-git's [#6708](https://github.com/CrocSwap/integer-mult-bounds/pull/6708). +The new proof and construction were produced by Nick Petalas. Apache-2.0. + +## 1. The signature and the generic model + +Partition the rows of an invertible square matrix P into nonempty blocks. +Message j has source mask consisting of the blocks on which column j of P +is nonzero. Its reader mask consists of the blocks on which row j of +P inverse is nonzero. This is the source/reader convention of #6708, +Gonzalo Mier's #3990/#3997 and Nick Petalas's #6691. + +A generic support matrix has one separate algebraically independent +indeterminate in each allowed entry, zero elsewhere. Invertibility and +inverse supports are taken over the rational-function field. The generic +census is the union of signatures over all such structurally invertible +supports, not just the support of one selected numerical witness. + +**Result.** On three blocks of two rows there is an integer unimodular P +whose source masks are all ABC and whose reader masks are + + BC, BC, AC, AC, AB, AB. + +The same matrices realize the same signature over every field. No generic +support matrix has that signature, over any coefficient field. In fact, +for b >= 2 blocks and arbitrary positive block sizes, if every generic +source mask is full then at least b reader masks are full. This generic +lower bound is sharp. + +The counterexample settles the stated six-port existence question. It +does not enumerate all three-block signatures or price a decoder. + +## 2. A field-uniform integer witness + +All displayed blocks are two by two. Put + + T = [ 0 -1 ] T^2 + T + I = 0, det T = 1. + [ 1 -1 ] + +Define the two six-by-six integer matrices + + [ 0 I I ] [ T^2 -T^2 -T ] + B = [ I 0 I ], P = [ -T T -T ]. + [ I T 0 ] [ -T^2 -T T ] + +Direct block multiplication using T^2 + T + I = 0 gives + + P B = B P = I_6. + +For example the first block row of P B is +(-T^2-T, T^2-T^2, T^2-T^2) = (I,0,0). +The remaining block rows follow by the same identity. Both matrices +therefore have integer inverses and are unimodular. This establishes the +identity over every field, including characteristic two; no division by +two is used. + +Every block of P is one of T, -T, T^2, -T^2 and is invertible over every +field. Every column of P consequently has a nonzero restriction to each +of the three row blocks. The diagonal blocks of B are zero and every +off-diagonal block is I or T, also invertible. Each row in block A of B +therefore reads exactly B and C, and likewise for the other blocks. +This proves the claimed signature over every field. + +## 3. Generic inverse supports from a determinant matching + +Here is the classical matching/path description, with conventions fixed +to avoid transposing source and reader masks. + +Choose a determinant matching of a structurally invertible generic +matrix. Write r(j) for the row matched to column j. Relabel column j by +r(j), so the matched entries become diagonal in a matrix Q. On the row +vertices put a directed edge i -> r(j) for every supported P[i,j]. + +**Path fact.** The generic inverse entry P inverse[j,i] is nonzero if and +only if i is reachable from r(j) in this directed graph, allowing the +length-zero path. + +To prove this, first use Q. A simple path from u to v supplies a matching +in Q with row v and column u removed: use the path's edges and the +diagonal matching at the other vertices. Conversely any matching of that +minor, together with the removed row/column, decomposes into a directed +path from u to v and disjoint cycles. Thus the corresponding cofactor +has a determinant matching exactly when the path exists. Each supported +entry is a distinct indeterminate, so different matchings have different +monomials. They cannot cancel, even in characteristic two. A cofactor is +therefore nonzero exactly in this case. Undoing the column relabeling +gives the stated convention for P inverse. The u=v case uses the +diagonal matching in the principal minor. + +This uses the standard structural determinant/cofactor matching method; +it is not a new matching theorem. The new use is the block-mask bound +below. + +## 4. The generic full-reader floor and its sharpness + +Suppose every source mask of P contains all b blocks. Take a source +strongly connected component C of the directed graph above, meaning one +with no edge into it from another component. Such a component exists +because the component graph is a finite directed acyclic graph. + +For any column j with r(j) in C, every block supplies a supported entry +P[i,j]. Each such entry gives an edge i -> r(j). The source property +forces i into C. Thus C meets every block and has at least b vertices. + +For each vertex r(j) in C, strong connectivity gives a path to every +vertex of C. By the path fact, row j of P inverse has a nonzero entry in +each block. The distinct vertices of C correspond to distinct messages. +At least |C| >= b messages therefore have full reader masks. This proves +the bound for every structurally invertible support, irrespective of the +matching chosen. + +For sharpness choose one representative row in each block. Support every +entry of those b rows, and support only the diagonal entry of each other +row. There is a diagonal matching. The representatives form one source +strongly connected component; they reach every row. Every other vertex +has only its self-loop. The path fact gives full reader masks exactly +at the b representatives. All columns have full source masks. Because +b >= 2, the other rows' singleton reader masks are not full. The lower +bound is attained for all positive block sizes. + +For the six-port witness b=3, but no reader mask is full. Hence its +signature is absent from the union over all generic support matrices. +Merely noting cancellation in its own entry support would not prove +this stronger exclusion; the universal bound does. + +## 5. Scope and finite corroboration + +The all-field conclusion and the exclusion of all six-port generic +supports use the proof above. The verifier independently inverts the +integer matrices, checks both products and signatures, and specializes +to F2, F3, F5, F7 and F11. It checks every full-source support for block +sizes (1,1,1), (2,1,1) and (2,2,1), comparing literal cofactor matchings +with graph reachability. It also checks the sharp six-port generic +example and the generic signature of the actual witness support. +These are finite corroborations, not an exhaustive six-port census. + +The predecessor's two-block classification is a cited result, not +replayed or audited. Its theorem remains within its two-block scope. +The new result shows why its generic-signature equality cannot simply +be extended to three blocks. No paid physical preparation, restoration, +delivery, native word, supplier, kappa or multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/three-block-cancellation-signature/README.md b/research/three-block-cancellation-signature/README.md new file mode 100644 index 0000000000..f58d66c891 --- /dev/null +++ b/research/three-block-cancellation-signature/README.md @@ -0,0 +1,116 @@ +# Cancellation adds a three-block decoder signature + +A six-by-six integer unimodular basis realizes a source/reader signature +absent from every generic support pattern. It works over every field, +including F2. This answers Open next question 1 of SHIN09-git's +[#6708](https://github.com/CrocSwap/integer-mult-bounds/pull/6708). +The new contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. +No decoder price, native word, supplier admission or new kappa is claimed. + +## Result + +Divide the six port rows into A={0,1}, B={2,3}, C={4,5}. Every column of +the explicit basis P uses all three blocks. The six rows of its inverse +use exactly BC, BC, AC, AC, AB, AB. All entries are 0, 1 or -1 and both +inverse products are integer identities. + +In contrast, a generic support matrix on b >= 2 nonempty row blocks, +with every column using all b blocks, must have at least b inverse rows +using all b blocks. The bound is sharp for every choice of block sizes. +The proof chooses a source strongly connected component in the directed +graph of a determinant matching. It excludes every generic support, +not just the entry support of P. [PROOF.md](PROOF.md) gives the matrices +and the full argument. + +This is the first improvement being delivered. The remaining signature +classification and any physical use are left below. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/three-block-cancellation-signature +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/three-block-cancellation-signature/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/three-block-cancellation-signature/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/three-block-cancellation-signature --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter. Direct replay +prints a generated receipt bound to the package hashes, followed by +`PASS_THREE_BLOCK_CANCELLATION_SIGNATURE`. It writes no files. No receipt +is handwritten or stored as an asserted output. + +The verifier checks both integer products, independently solves both +inverses with rational elimination, and checks the signature over F2, F3, +F5, F7 and F11. It rejects all 27 single-nonzero-entry omissions from P. +It enumerates all 59,131 full-source supports at block sizes (1,1,1), +(2,1,1) and (2,2,1). The 58,081 structurally invertible supports pass +independent cofactor-matching and graph-reachability checks. Two six-port +patterns corroborate sharpness and the difference between the numerical +witness and its generic support. Five invalid-input controls pass. +The all-size theorem and all-field witness use the written proof; +this is not an exhaustive six-port census. + +## Scope, sources and decision + +The `coverage-law-change` card changes scope to this square-basis +algebraic question. Base main is +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8, +selected #7000. The selected source-binding orientation passes; no +selected scientific replay is performed. The result does not change +the selected record or any of its five inherited assumptions. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538530) +states the same target. Live handoffs, current PRs, recent account work, +local reservations, main README searches, merged searches and the overlap +helper were consulted. The source-reference search found no recent +account PR using #6708. The overlap helper's working-note inventory is +sparse; explicit main-tree searches supplement it. Arbitrary historical +diffs, nested notes and unpublished work remain coverage limits. + +SHIN09-git's two-block classification is cited without auditing or +replaying its scientific checker. It proves rational generic equality +for two blocks and explicitly asks the three-block question settled here. +Its proof and README are pinned in [SOURCES.json](SOURCES.json). The +source/reader model and earlier screens retain Gonzalo Mier's #3990/#3997 +and Nick Petalas's #6691 credit. Structural determinant/cofactor matchings +and the inverse-path description are classical. The new steps are the +sharp block-mask consequence and the field-uniform six-port separation. + +No complete physical producer or consumer is supplied. Preparation, +delivery, arbitrary dirty-state restoration, routing, precision, stock, +compiler closure and a signed invoice remain unpaid obligations. Unknown +costs are not zero. Independent human and formal proof-kernel review, +Lean, Docker and supplier admission are unclaimed. The decision is to +retain this settled algebraic question and stop. + +## Open next questions + +1. Which other three-block signatures lie outside the generic census? + Start with supports of inverse bases having a zero diagonal block; + a complete cancellation-sensitive classification is the blocker. +2. Can a physical caller exploit this signature after all preparation, + delivery and restoration costs? Start with these literal matrices and + one source/reader schedule. No favorable full invoice is supplied. + +## Implementation bounds + +All matrix dimensions are at most six. Matching lists have at most 720 +terms; each cofactor has at most 120. The replay enumerates exactly the +three stated support domains and two six-port patterns. There is no +recursion, subprocess, network access or dynamic source generation. +All functions are below sixty physical lines and internal checks remain +active under optimized Python. The only module dispatch loads the fixed +local model file; the invalid-input table has five fixed call targets. + +Power-of-Ten rule 3 deviation: Python and Fraction allocate during +execution. Fixed dimensions, coefficient fixtures, one support processed +at a time and bounded matching lists limit live memory. A fixed local +module loader is the rule 9 dispatch deviation needed by isolated Python; +the target is `model.py`, with lifetime equal to this process. Rule 10 +uses warning-strict normal/optimized execution; no additional Python +static analyzer is claimed. These are mathematical checks, not physical +memory or tape tariffs. diff --git a/research/three-block-cancellation-signature/SOURCES.json b/research/three-block-cancellation-signature/SOURCES.json new file mode 100644 index 0000000000..d8f162fddc --- /dev/null +++ b/research/three-block-cancellation-signature/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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" + }, + { + "path": "research/two-block-signatures/PROOF.md", + "usage": "input", + "git_blob": "51cb134d77f700c031084311b43cb4c02e17ba68", + "sha256": "47094558499d02e81a26aeb7969efbdfc8d91bc719537e2c36d6cca0cc629179" + }, + { + "path": "research/two-block-signatures/README.md", + "usage": "input", + "git_blob": "7e568edb6c84a6ec3575cd420f42cc66cd7d93c0", + "sha256": "b96207a9dbc79a1b3ff228a8409d7e960425b59a92d5afbe84ff1fef7cfd2096" + } + ] +} diff --git a/research/three-block-cancellation-signature/TASK.json b/research/three-block-cancellation-signature/TASK.json new file mode 100644 index 0000000000..ba6404993a --- /dev/null +++ b/research/three-block-cancellation-signature/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Settle PR6708 Open next question 1 with a field-uniform six-port cancellation signature absent from every generic support pattern, and prove the sharp generic full-reader floor.", + "scope_change_reason": "The card asks for a changed coverage law or decoder. This is a self-contained square-basis signature obstruction and construction; physical delivery and the full supplier gate remain open.", + "bottleneck_link": "Generic support screens miss a realizable three-block interface signature. This is an algebraic side result; any decoder improvement must still pay for a complete physical producer and consumer.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified new signature and generic exclusion; do not extend the census or seek a physical supplier in this package.", + "outcome": "completed", + "evidence": "PROOF.md and standalone normal/optimized verify.py; no predecessor scientific suite is replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which further three-block signatures are absent from the generic census?", + "why_it_matters": "A support-only decoder screen is incomplete.", + "first_step": "Classify inverse bases with a zero diagonal block.", + "blocked_by": "A cancellation-sensitive classification rather than determinant matchings alone." + }, + { + "question": "Can a paid physical caller exploit the six-port signature?", + "why_it_matters": "The matrix identity does not itself improve the supplier invoice.", + "first_step": "Specify one complete chronological source/reader schedule for P and its inverse.", + "blocked_by": "Preparation, delivery, dirty restoration, native, precision, stock and compiler costs." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538530", + "source_question": { + "pr": 6708, + "author": "SHIN09-git", + "package": "research/two-block-signatures", + "question": "Open next question 1: three blocks of two ports, cancellation outside the generic census" + }, + "environment": { + "python": "3.12.15", + "system": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "claim_type": "scoped proof with exact finite corroboration" +} diff --git a/research/three-block-cancellation-signature/VERIFY.json b/research/three-block-cancellation-signature/VERIFY.json new file mode 100644 index 0000000000..a534370db0 --- /dev/null +++ b/research/three-block-cancellation-signature/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/two-block-signatures/PROOF.md", + "research/two-block-signatures/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Integer inverse and all-field signature witness; exhaustive small full-source generic supports with cofactor/path agreement; sharp six-port floor; omission and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Integer inverse and all-field signature witness; exhaustive small full-source generic supports with cofactor/path agreement; sharp six-port floor; omission and invalid-input controls." + } + ] +} diff --git a/research/three-block-cancellation-signature/model.py b/research/three-block-cancellation-signature/model.py new file mode 100644 index 0000000000..a64816b1de --- /dev/null +++ b/research/three-block-cancellation-signature/model.py @@ -0,0 +1,141 @@ +"""Exact matrices and generic support tests. Nick Petalas. Apache-2.0.""" + +from fractions import Fraction +from itertools import permutations, product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + require(1 <= n <= 6, "matrix dimension must be between one and six") + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def multiply(a, b): + n = len(a) + require(1 <= n <= 6 and len(b) == n, "incompatible dimensions") + require(all(len(row) == n for row in a + b), "matrices must be square") + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(n)) + for j in range(n)) for i in range(n)) + + +def inverse(a): + n = len(a) + require(1 <= n <= 6 and all(len(row) == n for row in a), "bad matrix") + aug = [[Fraction(value) for value in a[i]] + list(identity(n)[i]) + for i in range(n)] + for col in range(n): + pivot = next((i for i in range(col, n) if aug[i][col]), None) + require(pivot is not None, "singular matrix") + aug[col], aug[pivot] = aug[pivot], aug[col] + scale = aug[col][col] + aug[col] = [value / scale for value in aug[col]] + for i in range(n): + if i != col: + scale = aug[i][col] + aug[i] = [x - scale * y for x, y in zip(aug[i], aug[col], strict=True)] + require(tuple(tuple(row[:n]) for row in aug) == identity(n), "bad elimination") + return tuple(tuple(row[n:]) for row in aug) + + +def negate(a): + return tuple(tuple(-x for x in row) for row in a) + + +def expand_blocks(a): + return tuple(tuple(a[i // 2][j // 2][i % 2][j % 2] + for j in range(6)) for i in range(6)) + + +def witness(): + unit, zero = identity(2), ((0, 0), (0, 0)) + t = ((0, -1), (1, -1)) + t2 = multiply(t, t) + b = ((zero, unit, unit), (unit, zero, unit), (unit, t, zero)) + p = ((t2, negate(t2), negate(t)), (negate(t), t, negate(t)), + (negate(t2), negate(t), t)) + return expand_blocks(p), expand_blocks(b) + + +def masks(a, b, sizes): + n = sum(sizes) + require(len(a) == len(b) == n and n <= 6, "bad signature dimensions") + require(all(size > 0 for size in sizes), "empty block") + require(all(len(row) == n for row in a + b), "bad signature matrix") + blocks, start = [], 0 + for size in sizes: + blocks.append(tuple(range(start, start + size))) + start += size + source = tuple(sum(1 << k for k, rows in enumerate(blocks) + if any(a[i][j] for i in rows)) for j in range(n)) + reader = tuple(sum(1 << k for k, rows in enumerate(blocks) + if any(b[j][i] for i in rows)) for j in range(n)) + return source, reader + + +def matching_terms(n): + require(1 <= n <= 6, "unsupported generic dimension") + terms = tuple((sum(1 << (i * n + p[i]) for i in range(n)), p) + for p in permutations(range(n))) + cofactors = [] + for removed_row in range(n): + rows = tuple(i for i in range(n) if i != removed_row) + row_terms = [] + for removed_col in range(n): + cols = tuple(j for j in range(n) if j != removed_col) + row_terms.append(tuple(sum(1 << (i * n + col) + for i, col in zip(rows, perm, strict=True)) + for perm in permutations(cols))) + cofactors.append(tuple(row_terms)) + return terms, tuple(cofactors) + + +def generic_inverse(support, n, terms, cofactors): + require(0 <= support < 1 << (n * n), "support outside matrix") + match = next((p for bits, p in terms if support & bits == bits), None) + if match is None: + return None, None + result = tuple(tuple(int(any(support & bits == bits for bits in cofactors[i][j])) + for i in range(n)) for j in range(n)) + return result, match + + +def reach_inverse(support, n, match): + """Alternating paths, computed without the cofactor matching test.""" + row_for_col = [0] * n + for row, col in enumerate(match): + row_for_col[col] = row + reach = [1 << i for i in range(n)] + for i in range(n): + for j in range(n): + if support & (1 << (i * n + j)): + reach[i] |= 1 << row_for_col[j] + for middle in range(n): + for i in range(n): + if reach[i] & (1 << middle): + reach[i] |= reach[middle] + return tuple(tuple((reach[row_for_col[j]] >> i) & 1 for i in range(n)) + for j in range(n)) + + +def full_source_supports(sizes): + n = sum(sizes) + require(1 <= n <= 6 and all(1 <= s <= 2 for s in sizes), "bad support domain") + offsets, start = [], 0 + for size in sizes: + offsets.append(start) + start += size + columns = tuple(sum(bits << offset for bits, offset in zip(parts, offsets, strict=True)) + for parts in product(*(range(1, 1 << size) for size in sizes))) + for choice in product(columns, repeat=n): + yield sum(1 << (i * n + j) for j in range(n) for i in range(n) + if choice[j] & (1 << i)) + + +def support_matrix(support, n): + require(1 <= n <= 6 and 0 <= support < 1 << (n * n), "bad support") + return tuple(tuple((support >> (i * n + j)) & 1 for j in range(n)) + for i in range(n)) diff --git a/research/three-block-cancellation-signature/verify.py b/research/three-block-cancellation-signature/verify.py new file mode 100644 index 0000000000..4156d73b48 --- /dev/null +++ b/research/three-block-cancellation-signature/verify.py @@ -0,0 +1,122 @@ +#!/usr/bin/env python3 +"""Verify the new cancellation witness and generic obstruction. + +Nick Petalas. Apache-2.0. No predecessor scientific verifier is imported. +""" + +import hashlib +import importlib.util +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("signature_model", PACKAGE / "model.py") +if SPEC is None or SPEC.loader is None: + raise RuntimeError("cannot load local model") +model = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(model) + + +def check_witness(): + p, b = model.witness() + model.require(model.multiply(p, b) == model.identity(6), "P B is not identity") + model.require(model.multiply(b, p) == model.identity(6), "B P is not identity") + model.require(model.inverse(p) == b and model.inverse(b) == p, "inverse mismatch") + signature = ((7,) * 6, (6, 6, 5, 5, 3, 3)) + model.require(model.masks(p, b, (2, 2, 2)) == signature, "wrong integer signature") + for prime in (2, 3, 5, 7, 11): + pm = tuple(tuple(x % prime for x in row) for row in p) + bm = tuple(tuple(x % prime for x in row) for row in b) + result = tuple(tuple(x % prime for x in row) for row in model.multiply(pm, bm)) + model.require(result == model.identity(6), "finite-field endpoint failed") + model.require(model.masks(pm, bm, (2, 2, 2)) == signature, "field signature changed") + mutations = 0 + for i in range(6): + for j in range(6): + if p[i][j]: + bad = tuple(tuple(0 if (u, v) == (i, j) else p[u][v] + for v in range(6)) for u in range(6)) + model.require(model.multiply(bad, b) != model.identity(6), "omission survived") + mutations += 1 + return {"P": p, "inverse": b, "source_masks": signature[0], + "reader_masks": signature[1], "finite_fields": [2, 3, 5, 7, 11], + "nonzero_entry_omissions_rejected": mutations} + + +def check_generic(sizes): + n, full = sum(sizes), (1 << len(sizes)) - 1 + terms, cofactors = model.matching_terms(n) + tested = nonsingular = 0 + histogram = {} + for support in model.full_source_supports(sizes): + tested += 1 + inverse, match = model.generic_inverse(support, n, terms, cofactors) + if inverse is None: + continue + nonsingular += 1 + model.require(inverse == model.reach_inverse(support, n, match), "path/cofactor mismatch") + source, reader = model.masks(model.support_matrix(support, n), inverse, sizes) + model.require(source == (full,) * n, "wrong enumeration domain") + count = reader.count(full) + model.require(count >= len(sizes), "generic full-reader floor failed") + histogram[count] = histogram.get(count, 0) + 1 + model.require(sum(histogram.values()) == nonsingular, "lost generic support") + return {"block_sizes": sizes, "tested": tested, "generic_nonsingular": nonsingular, + "full_reader_histogram": histogram} + + +def check_six_port_patterns(): + terms, cofactors = model.matching_terms(6) + p, _ = model.witness() + actual = sum(1 << (i * 6 + j) for i in range(6) for j in range(6) if p[i][j]) + inverse, match = model.generic_inverse(actual, 6, terms, cofactors) + model.require(inverse is not None, "witness support is structurally singular") + model.require(inverse == model.reach_inverse(actual, 6, match), "witness path mismatch") + _, reader = model.masks(model.support_matrix(actual, 6), inverse, (2, 2, 2)) + model.require(reader.count(7) >= 3, "own support evades generic theorem") + representatives = (0, 2, 4) + sharp = sum(1 << (i * 6 + j) for i in range(6) for j in range(6) + if i in representatives or i == j) + inv_sharp, match = model.generic_inverse(sharp, 6, terms, cofactors) + model.require(inv_sharp is not None, "sharp support is singular") + model.require(inv_sharp == model.reach_inverse(sharp, 6, match), "sharp path mismatch") + source, readers = model.masks(model.support_matrix(sharp, 6), inv_sharp, (2, 2, 2)) + model.require(source == (7,) * 6 and readers.count(7) == 3, "floor is not sharp") + return {"actual_support_generic_reader_masks": reader, + "sharp_generic_reader_masks": readers} + + +def check_invalid(): + cases = ((model.identity, (0,)), (model.inverse, (((0,),),)), + (model.matching_terms, (7,)), (model.support_matrix, (-1, 3)), + (model.full_source_supports, ((3, 1),))) + rejected = 0 + for function, args in cases: + try: + result = function(*args) + if function is model.full_source_supports: + tuple(result) + except ValueError: + rejected += 1 + model.require(rejected == len(cases), "invalid input accepted") + return rejected + + +def main(): + receipt = {"claim_type": "scoped proof with exact finite corroboration", + "witness": check_witness(), + "generic_support_domains": [check_generic(sizes) for sizes in + ((1, 1, 1), (2, 1, 1), (2, 2, 1))], + "six_port_patterns": check_six_port_patterns(), + "invalid_inputs_rejected": check_invalid()} + paths = sorted(path for path in PACKAGE.iterdir() if path.is_file()) + model.require(len(paths) <= 16, "unexpected package inventory") + receipt["package_sha256"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in paths} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_THREE_BLOCK_CANCELLATION_SIGNATURE") + + +if __name__ == "__main__": + main()