diff --git a/research/functional-pairing-lift/PROOF.md b/research/functional-pairing-lift/PROOF.md new file mode 100644 index 0000000000..bc21a193d2 --- /dev/null +++ b/research/functional-pairing-lift/PROOF.md @@ -0,0 +1,130 @@ +# A simultaneous lift for functional decoder pairings + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped proof, with finite exact corroboration. + +## Statement + +Let B be a v-by-v binary matrix with B_ii=1. Suppose each row has at most +one off-diagonal one. There is an integer matrix S with the same support, +diagonal one, and all nonzero entries in {1,-1}, such that every square +minor of S is 0, 1 or -1. Consequently, for every pair of row and column +sets R,A and every field K, + + rank_K S[R,A] = rank_F2 B[R,A]. + +The same conclusion holds when the column condition replaces the row +condition. One signing works simultaneously for all rectangular blocks. +No support sets need to be supplied to the construction. + +For any field K, let p_t,q_t belong to K^T, with finite T, and suppose + + p_t dot q_t != 0, + p_t dot q_s = 0 whenever t != s and B_ts = 1. + +Put R_j={t:p_tj != 0}, A_j={t:q_tj != 0}. Then + + sum_j rank_F2 B[R_j,A_j] >= v. + +For each B in the stated class the bound is attained if the number of +totals is unrestricted. This does not assert attainment with T=3. + +## Constructing the signing + +Write f(i)=j for the off-diagonal one in row i, leaving f(i) undefined +when there is none. Its directed cycles have distinct vertices and length +k>=2. Distinct cycles are vertex-disjoint because each vertex has at most +one successor. + +Start with S=B over the integers. On each directed cycle of length k, +choose its least-indexed vertex i and replace S_i,f(i) by (-1)^k. +All other supported entries remain one. In particular, even cycles need +no change; odd cycles receive one minus sign. The cycle-edge product is +always (-1)^k. + +The implementation first removes vertices of indegree zero, then walks +the remaining cycles. Each vertex enters the removal queue at most once, +and each remaining vertex is walked once. Given successor lists this is +linear work and storage in v. Reading and returning a dense matrix takes +O(v^2) work and storage. The implementation caps v at 256; the written +theorem has no such bound. + +## Every minor is zero or a unit + +Consider any square submatrix. If it has a zero row or column its +determinant is zero. If a row or column has just one nonzero, expand along +it. The multiplier is 1 or -1. Repeat, reducing the order each time. +The empty determinant is one. + +If a nonempty square core remains with every row and column of degree at +least two, each row has exactly two nonzeros, since every original row +had at most two. Counting entries shows that each column also has degree +exactly two. Both supported entries of every remaining row are present, +including its original diagonal. Thus the remaining row set is contained +in the remaining column set. Equal cardinalities make those sets equal. +The remaining successor map is a permutation without fixed points. +Its components are complete directed cycles from the original f. + +For a cycle of length k, the corresponding block has precisely two +nonzero determinant terms: the diagonal product 1 and the cycle product +with permutation sign (-1)^(k-1). Its determinant is + + 1 + (-1)^(k-1) (-1)^k = 0. + +After simultaneous row and column reordering the core is a nonempty +block diagonal union of such blocks, so its determinant is zero. +Undoing the leaf expansions proves that every minor is 0, 1 or -1. + +This is an elementary total-unimodularity argument. No historical novelty +is claimed for total unimodularity or the leaf-expansion method. The new +decoder reduction is the simultaneous functional-pairing lift and its +all-T consequence in the retained cost model. + +## Field-independent ranks + +Reduction of S modulo two is B. A nonzero integer minor of S is 1 or -1, +which stays nonzero in every field. A zero minor stays zero. The largest +nonzero minor therefore has the same order over every field, including +F2. Apply this separately to every rectangular submatrix. The empty-row +and empty-column cases have rank zero. Transposition proves the column +version without a new signing argument. + +## The decoder cost floor + +This step is the Hadamard/lift rank argument credited to #1590 and #2111. +It is included to state exactly what the new sufficient lift permits. +Let M_ts=p_t dot q_s. The matrix M Hadamard S is diagonal with nonzero +diagonal, hence has rank v over K. It is also + + sum_j diag(p_:j) S diag(q_:j). + +The j-th summand has rank rank_K S[R_j,A_j]: removing its zero rows and +columns leaves invertible diagonal rescalings. Rank subadditivity and +the simultaneous rank identity give + + v <= sum_j rank_K S[R_j,A_j] + = sum_j rank_F2 B[R_j,A_j]. + +For tightness with unrestricted T, choose T=v and p_t=q_t=e_t. Then +M=I is compatible with every unit-diagonal B, and each of the v terms +has binary block rank one. This only establishes tightness of the bound +over the union of all finite-T decoder classes. + +## Scope and consequences + +The theorem excludes every pairing in this sparse class from beating v, +including three-total configurations with full-support points, arbitrary +coefficients and repeated geometric points or lines. It strengthens the +available list of sufficient reductions; it does not solve #2111's +general lift problem or claim a new theorem for arbitrary pairings. + +The condition is on the chosen pairing B, not just a selected subset of +its incidences. A configuration whose entire allowed off-diagonal pattern +has outdegree at most one inherits the bound for every admissible B. +Otherwise, excluding its functional pairings alone need not exclude a +cheaper nonfunctional pairing. No decoder, native word, paid supplier, +physical restoration, recursive invoice or improvement to kappa follows. + +The full multiplication theorem's native, ownership, compiler, +precision/tape and analytic assumptions are not discharged. No formal +proof-kernel or independent human review is claimed. diff --git a/research/functional-pairing-lift/README.md b/research/functional-pairing-lift/README.md new file mode 100644 index 0000000000..ab1f07105c --- /dev/null +++ b/research/functional-pairing-lift/README.md @@ -0,0 +1,107 @@ +# Functional decoder pairings cannot beat cost v + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped proof with exact finite corroboration. Independent human +and formal proof-kernel review are unclaimed. + +For every binary pairing B with unit diagonal and at most one off-diagonal +one per row, an explicit integer signing preserves the rank of every +rectangular submatrix, simultaneously, over every field. The transposed +class has the same property. Consequently every exact decoder compatible +with B has total binary COPY-rank cost at least v, for any finite number +of totals and over any coefficient field. The bound is attained with v +coordinate totals. Attainment with three totals is not asserted. + +The construction puts one minus sign on each odd directed successor cycle. +Every square minor of the resulting matrix is 0, 1 or -1. The proof uses +leaf expansion and the retained Hadamard/lift rank argument. See +[PROOF.md](PROOF.md) for all quantifiers and the field-independent proof. + +This adds a sufficient reduction to DreamingOfClouds's PR #2111, Open next +question 8. It does not replay its examples or signing searches. Classical +total unimodularity and the predecessor's Hadamard rank argument retain +their credit; no historical novelty is claimed for those tools. The new +contribution is this explicit sparse-class reduction and its checker. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/functional-pairing-lift/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/functional-pairing-lift/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/functional-pairing-lift +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/functional-pairing-lift --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter. The scientific +marker is `PASS_FUNCTIONAL_PAIRING_LIFT`. Direct replay reads the pinned +PR2111 README but executes no predecessor code. It needs no Git or network. +The generic source-history check additionally needs the retained Git history. + +Every functional matrix of orders one through four is enumerated. The +checker compares binary and exact rational ranks on all rectangular +submatrices and computes every square minor by an independent Leibniz +formula. Larger cycles, paths, stars and disjoint-pair families through +order sixteen have prefix/suffix rectangular-rank checks. Nontrivial +two-total cycle decoders and coordinate-total attainments are checked. +Malformed inputs, the capacity boundary and an unsigned odd-cycle lift +distinguish the hypotheses. The generated [RESULT.json](RESULT.json) +records counts and binds every proof, code and metadata file by SHA256. +Normal replay writes no files. `--emit NEW_EXTERNAL_PATH` creates a new +receipt without overwriting an existing file. + +## Limits and implementation bounds + +The row or column condition is imposed on the complete chosen pairing, +not a subset of its edges. General pairings and the general three-total +lift conjecture remain open. This is a mathematical cost obstruction, +not a new decoder, native word, supplier invoice, kappa or selected-frontier +update. Physical ownership, restoration, routing, precision, compiler and +analytic recovery obligations remain separate. No selected cold replay, +Lean or Docker run is part of the claim. + +The signer caps dense input order at 256 and uses no recursion, subprocess, +network, mutable global cache or predecessor import. All loops have bounds +from that cap or fixed census limits. Each function is below sixty lines. +Explicit exceptions remain active under `-O`; warning errors are enabled +in both registered commands. No external static analyzer is claimed. + +Power of Ten rule 3 deviation: CPython allocates integer, Fraction and +collection objects during execution. This one-shot exact checker cannot +disable those allocations. The signer retains O(256^2) cells, the complete +census works on matrices of order at most four, and the larger fixtures +have order at most sixteen. It retains one current submatrix at a time. +The endpoint and oversize controls check the input bound. A future native +steady-operation implementation would need fixed-capacity storage before +removing this deviation. + +## Sources and overlap + +The exact base is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision +8. [SOURCES.json](SOURCES.json) pins the source README, historical card and +selected record. The current baseline binding check passed; it is not a +scientific supplier replay. The card's scope change is in [TASK.json](TASK.json). + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267785) +and reservation followed live open-PR, recent-account, handoff, main README +and merged-PR searches. Targeted terms included functional pairing, +pseudoforest, cactus, one off-diagonal contact and directed-cycle decoder. +The cached overlap scan omits sparse local notes; explicit Git searches +covered all main README paths for the distinctive terms. This is bounded +overlap evidence, not a novelty certificate or coverage of unpublished work. + +Credit DreamingOfClouds #2111 for the model, lift hierarchy and open reduction +question; #1590 for the exact decoder and Hadamard/lift lemma; and #446/#595 +for the underlying cost model. The E8/P104, native, helper, caller and +compiler sources retain their predecessor credit. Existing files and +their credit lines are unchanged. + +## Open next questions + +1. Can a named second contact preserve simultaneous ranks? Specify its + entire pairing graph and first overlapping cycles. The one-successor + argument does not decide this larger class. +2. Can the reduction prune a new decoder search? Start with its complete + chosen pairing and preserve all nonfunctional candidates. This package + supplies no search integration or physical supplier. diff --git a/research/functional-pairing-lift/RESULT.json b/research/functional-pairing-lift/RESULT.json new file mode 100644 index 0000000000..38a701d865 --- /dev/null +++ b/research/functional-pairing-lift/RESULT.json @@ -0,0 +1,28 @@ +{ + "claim_type": "scoped-proof", + "controls": 9, + "exhaustive": { + "cycles": 146, + "identity_decoder_attainments": 288, + "matrices": 288, + "rectangular_ranks": 67332, + "square_minors": 18486 + }, + "larger": { + "matrices": 48, + "rectangular_ranks": 27680, + "two_total_decoders": 12 + }, + "schema": "functional-pairing-lift/v1", + "sha256": { + "PROOF.md": "396d3f4e5bb8feac2651f4ee8b751201f4d114609b87df0f9c101b362550b6ea", + "README.md": "a41871da12d74573f36ee387538fb2e30b9ffa3374af0c862c7c80b608a13d04", + "SOURCES.json": "b36c6bfc31466eb8d52fe37ee03a5fc59f48fda17257eaf44be4ad7fb6b46a69", + "TASK.json": "5a302b775567ade9fad1eccdb2006adba5e855b19287e6186b82c28ed9136abb", + "VERIFY.json": "24f0f9ab9d61c6dc66a10b580c140d83c59f3f71b34f8801654f4dd1806415db", + "verify.py": "f270f69f3b82f09fb56f886f4841f2148c776c7a91d809cf37a69e334272d8bd" + }, + "source_sha256": { + "research/three-total-decoders/README.md": "a812bb80e480a3f2f446e0f0f77300606e4337e4a888c141a7f4380ca15bef07" + } +} diff --git a/research/functional-pairing-lift/SOURCES.json b/research/functional-pairing-lift/SOURCES.json new file mode 100644 index 0000000000..488062cfb9 --- /dev/null +++ b/research/functional-pairing-lift/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/three-total-decoders/README.md", + "usage": "input", + "git_blob": "229c79d6e9908b3cd2508206d711b5b3dd44c4ea", + "sha256": "a812bb80e480a3f2f446e0f0f77300606e4337e4a888c141a7f4380ca15bef07" + } + ] +} diff --git a/research/functional-pairing-lift/TASK.json b/research/functional-pairing-lift/TASK.json new file mode 100644 index 0000000000..17f354bd60 --- /dev/null +++ b/research/functional-pairing-lift/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "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": "Construct a simultaneous rank-preserving integer signing for unit-diagonal binary pairings with at most one off-diagonal one per row or per column; deduce cost at least v for every finite number of exact decoder totals over every field.", + "scope_change_reason": "A new algebraic sufficient reduction answers a bounded part of PR2111 Open next question 8. It is a scoped side result, not a complete changed supplier itinerary.", + "bottleneck_link": "Exclude a precisely stated sparse pairing class from attempts to reduce the decoder COPY-rank bill; dense pairings and physical realization remain open.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved sparse-class lift and its decoder consequence, after bounded exact corroboration and package checks. Do not extend the class.", + "outcome": "completed", + "evidence": "PROOF.md gives the unbounded theorem. verify.py enumerates every functional matrix through order four, every rectangular submatrix rank and every square minor, plus larger families and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one add a second off-diagonal contact in a named row while retaining a simultaneous rank-preserving lift?", + "why_it_matters": "This would exclude a larger sparse decoder class.", + "first_step": "Specify the entire new pairing graph and inspect its first overlapping cycles.", + "blocked_by": "The one-successor leaf/cycle proof no longer applies." + }, + { + "question": "Can the functional-pairing reduction prune a new decoder synthesis search without losing better nonfunctional pairings?", + "why_it_matters": "It could reduce search work on low-cost decoder candidates.", + "first_step": "Declare the search domain and use this theorem only on complete chosen pairing matrices.", + "blocked_by": "No synthesis integration or physical supplier is provided." + } + ] +} diff --git a/research/functional-pairing-lift/VERIFY.json b/research/functional-pairing-lift/VERIFY.json new file mode 100644 index 0000000000..feaad0443f --- /dev/null +++ b/research/functional-pairing-lift/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/three-total-decoders/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive functional pairings through order four, simultaneous rectangular ranks, all square minors, larger families, exact decoder fixtures, source and receipt hashes, rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite checks under optimized Python; explicit exceptions retain every check." + } + ] +} diff --git a/research/functional-pairing-lift/verify.py b/research/functional-pairing-lift/verify.py new file mode 100644 index 0000000000..d46a801616 --- /dev/null +++ b/research/functional-pairing-lift/verify.py @@ -0,0 +1,256 @@ +"""Exact checks for the functional-pairing signing theorem. Apache-2.0.""" + +import argparse +from fractions import Fraction +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +MAX_ORDER = 256 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def signing(matrix): + """Return a same-support TU signing; reject outside the row-functional class.""" + n = len(matrix) + require(1 <= n <= MAX_ORDER, "order outside 1..256") + require(all(len(row) == n for row in matrix), "matrix must be square") + require(all(type(x) is int and x in (0, 1) for row in matrix for x in row), + "entries must be binary integers") + require(all(matrix[i][i] == 1 for i in range(n)), "diagonal must be one") + successor = [-1] * n + indegree = [0] * n + for i, row in enumerate(matrix): + edges = [j for j, value in enumerate(row) if value and j != i] + require(len(edges) <= 1, "more than one off-diagonal one in a row") + if edges: + successor[i] = edges[0] + indegree[edges[0]] += 1 + queue = [i for i in range(n) if indegree[i] == 0] + for cursor in range(n): + if cursor == len(queue): + break + j = successor[queue[cursor]] + if j != -1: + indegree[j] -= 1 + if indegree[j] == 0: + queue.append(j) + signed = [list(row) for row in matrix] + seen = set() + cycles = [] + for start in range(n): + if indegree[start] == 0 or start in seen: + continue + cycle = [] + vertex = start + for _ in range(n): + require(vertex >= 0 and vertex not in seen, "invalid cycle core") + cycle.append(vertex) + seen.add(vertex) + vertex = successor[vertex] + if vertex == start: + break + require(vertex == start and len(cycle) >= 2, "cycle did not close") + signed[start][successor[start]] = (-1) ** len(cycle) + cycles.append(cycle) + return signed, cycles + + +def binary_rank(matrix): + basis = {} + for row in matrix: + value = sum((int(x) & 1) << j for j, x in enumerate(row)) + for _ in range(len(row)): + if value == 0: + break + pivot = value.bit_length() - 1 + if pivot not in basis: + basis[pivot] = value + break + value ^= basis[pivot] + return len(basis) + + +def rational_rank(matrix): + if not matrix: + return 0 + work = [[Fraction(x) for x in row] for row in matrix] + pivot_row = 0 + for col in range(len(work[0])): + pivot = next((i for i in range(pivot_row, len(work)) if work[i][col]), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + divisor = work[pivot_row][col] + work[pivot_row] = [x / divisor for x in work[pivot_row]] + for i in range(pivot_row + 1, len(work)): + multiplier = work[i][col] + if multiplier: + work[i] = [x - multiplier * y + for x, y in zip(work[i], work[pivot_row])] + pivot_row += 1 + if pivot_row == len(work): + break + return pivot_row + + +def determinant(matrix): + """Independent Leibniz oracle, used only at orders zero through four.""" + n = len(matrix) + require(n <= 4 and all(len(row) == n for row in matrix), "minor too large") + total = 0 + for permutation in itertools.permutations(range(n)): + inversions = sum(permutation[i] > permutation[j] + for i in range(n) for j in range(i + 1, n)) + term = (-1) ** inversions + for i, j in enumerate(permutation): + term *= matrix[i][j] + total += term + return total + + +def restrict(matrix, rows, columns): + return [[matrix[i][j] for j in columns] for i in rows] + + +def functional_matrices(n): + choices = [[-1] + [j for j in range(n) if j != i] for i in range(n)] + for successors in itertools.product(*choices): + matrix = [[int(i == j) for j in range(n)] for i in range(n)] + for i, j in enumerate(successors): + if j != -1: + matrix[i][j] = 1 + yield matrix + + +def exhaustive_checks(): + totals = {"matrices": 0, "rectangular_ranks": 0, "square_minors": 0, + "identity_decoder_attainments": 0, "cycles": 0} + for n in range(1, 5): + subsets = [tuple(i for i in range(n) if mask >> i & 1) + for mask in range(1 << n)] + for matrix in functional_matrices(n): + signed, cycles = signing(matrix) + totals["matrices"] += 1 + totals["cycles"] += len(cycles) + require(all(bool(x) == bool(y) for a, b in zip(matrix, signed) + for x, y in zip(a, b)), "support changed") + for rows in subsets: + for columns in subsets: + old = restrict(matrix, rows, columns) + new = restrict(signed, rows, columns) + require(binary_rank(old) == rational_rank(new), "rank mismatch") + totals["rectangular_ranks"] += 1 + if len(rows) == len(columns): + require(determinant(new) in (-1, 0, 1), "non-TU minor") + totals["square_minors"] += 1 + cost = sum(binary_rank([[matrix[i][i]]]) for i in range(n)) + require(cost == n, "identity decoder must attain v") + totals["identity_decoder_attainments"] += 1 + return totals + + +def cycle_fixture(n): + return [[int(j == i or j == (i + 1) % n) for j in range(n)] + for i in range(n)] + + +def larger_checks(): + result = {"matrices": 0, "rectangular_ranks": 0, "two_total_decoders": 0} + for n in range(5, 17): + cycle = cycle_fixture(n) + path = [[int(j == i or j == i + 1) for j in range(n)] for i in range(n)] + star = [[int(j == i or (i != 0 and j == 0)) for j in range(n)] + for i in range(n)] + pairs = [[int(j == i or j == (i ^ 1)) for j in range(n)] + for i in range(n)] + for matrix in (cycle, path, star, pairs): + signed, _ = signing(matrix) + result["matrices"] += 1 + choices = [tuple(range(k)) for k in range(n + 1)] + choices += [tuple(range(k, n)) for k in range(n + 1)] + for rows, columns in itertools.product(choices, repeat=2): + require(binary_rank(restrict(matrix, rows, columns)) == + rational_rank(restrict(signed, rows, columns)), + "larger rectangular rank mismatch") + result["rectangular_ranks"] += 1 + points = [(1, i + 1) for i in range(n)] + lines = [(((i - 1) % n) + 1, -1) for i in range(n)] + for i, j in itertools.product(range(n), repeat=2): + value = sum(a * b for a, b in zip(points[i], lines[j])) + require(value != 0 if i == j else not cycle[i][j] or value == 0, + "two-total fixture violates exactness") + cost = 2 * binary_rank(cycle) + require(cost == 2 * n - 2 and cost >= n, "two-total cycle cost") + result["two_total_decoders"] += 1 + return result + + +def rejection_checks(): + bad = [[], [[0]], [[True]], [[1, 1]], [[1, 1, 1], [0, 1, 0], [0, 0, 1]]] + count = 0 + for matrix in bad: + try: + signing(matrix) + except ValueError: + count += 1 + else: + raise ValueError("invalid matrix was accepted") + unsigned = cycle_fixture(3) + signed, _ = signing(unsigned) + require(determinant(unsigned) == 2 and determinant(signed) == 0, + "odd-cycle sign control must discriminate") + require(binary_rank(unsigned) == 2 and rational_rank(unsigned) == 3, + "unsigned lift must fail rank agreement") + require(signing([[int(i == j) for j in range(MAX_ORDER)] + for i in range(MAX_ORDER)])[1] == [], "capacity endpoint") + try: + signing([[1]] * (MAX_ORDER + 1)) + except ValueError: + count += 1 + else: + raise ValueError("oversize input was accepted") + return count + 3 + + +def receipt(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + source_rows = [row for row in sources["files"] if row["usage"] == "input"] + root = HERE.parents[1] + for row in source_rows: + require(hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() == + row["sha256"], "cited source bytes changed") + files = ("verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json") + return {"schema": "functional-pairing-lift/v1", "claim_type": "scoped-proof", + "exhaustive": exhaustive_checks(), "larger": larger_checks(), + "controls": rejection_checks(), + "sha256": {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in files}, + "source_sha256": {row["path"]: row["sha256"] for row in source_rows}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="create a new receipt outside the package") + args = parser.parse_args() + result = receipt() + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.emit: + require(not args.emit.resolve().is_relative_to(HERE.parents[1]), + "receipt output must be outside the checkout") + with args.emit.open("x", encoding="utf-8") as stream: + require(stream.write(payload) == len(payload), "incomplete receipt write") + else: + require((HERE / "RESULT.json").read_text() == payload, "receipt differs") + print("PASS_FUNCTIONAL_PAIRING_LIFT " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()