diff --git a/research/turyn-positive-redundancy/PROOF.md b/research/turyn-positive-redundancy/PROOF.md new file mode 100644 index 0000000000..f00894b760 --- /dev/null +++ b/research/turyn-positive-redundancy/PROOF.md @@ -0,0 +1,103 @@ +# Exact cost of positive redundant Turyn encoders + +This scoped result was produced by Nick Petalas. Apache-2.0. + +## Contract + +Let the port labels be vectors ell_i in F_2^h. For a real column v, charge + + c(v) = dim_F2 span {ell_i : v_i != 0}. + +Consider an exact factorization K = A H A^T with finitely many real encoder +columns and a real symmetric positive definite metric H. The bill is the sum +of c(a_j). Zero columns cost zero; R counts only nonzero columns. The metric +and scalar work are granted free. This is an algebraic encoder support bill, +not a complete physical or recursive invoice. Positive sums of outer products +are the diagonal-metric case; a dense metric can couple different columns. + +## Range lemma + +For every such factorization, range(K) = range(A) and rank(K) = rank(A). +Indeed, for every real x, + + x^T K x = (A^T x)^T H (A^T x). + +Positive definiteness makes this zero exactly when A^T x = 0. If Kx = 0 +then x^T Kx = 0, while A^T x = 0 implies Kx = 0 directly. Thus +ker(K) = ker(A^T). Taking orthogonal complements proves the range identity. +The argument permits dependent columns, any finite redundancy, arbitrary +real coefficients and a dense positive definite metric. + +## Fixed-kernel cost theorem + +Suppose K is positive semidefinite, rank(K) = r > 0, and every nonzero +v in range(K) has c(v) = h. +Then every positive definite factorization with R nonzero columns satisfies + + R >= r, sum_j c(a_j) = h R. + +Every column lies in range(K), so every nonzero column costs h. Also +rank(A) <= R. These prove both conclusions. + +Every integer R >= r is attainable. A positive semidefinite K of rank r +has a real Gram factor K = U U^T with r independent columns. Replace the +first column by t = R-r+1 identical copies. Give each duplicate weight 1/t +and every other column weight 1 in a diagonal H. The resulting A H A^T +is still K, every column is nonzero and H is positive definite. Hence +the minimum bill at prescribed R is exactly hR. No coefficient-height or +physical-cost bound is asserted by this construction. + +## Turyn specialization and predecessor premises + +DominikScholz's [PR598](https://github.com/CrocSwap/integer-mult-bounds/pull/598) +supplies two results that this package cites without replaying: + +1. The full canonical Turyn product kernel has 23,040 ports and real rank + 512. It is the Gram kernel of the 512 tensor coordinates, up to a positive + normalization. See `research/leech-lattice/TURYN.txt`, "Product kernel". +2. Under the existing direct-sum 27-bit labels, every nonzero real tensor + encoder has label-support rank 27. See the final section of + `research/turyn-port-labels/PROOF.txt` and its README's explicit restriction + to rank-minimal factorizations and encoders in the tensor column space. + +The tensor-coordinate matrix has full column rank, so its column space is +range(K). Applying the theorem gives the exact algebraic optimum + + B(R) = 27 R for every integer R >= 512. + +No factorization in this class exists with R < 512. The optimum over all +finite positive definite factorizations is therefore 13,824. Every nonzero +redundant column adds exactly 27. The cited tensor Gram factor attains the +minimum, and duplication attains every larger R. The extension to arbitrary +positive redundancy is new here; the geometry, rank and support theorem +remain the predecessor's results. The elementary Gram range identity is +classical, and no general linear-algebra priority is claimed. + +## Why the metric hypothesis matters + +Let u = (1,1)^T, K = u u^T and the port labels be e_1,e_2. Every nonzero +vector in range(K) has label-support rank two. + +* For A = I_2 and H = [[1,1],[1,1]], the equality K = A H A^T holds, but + H is singular positive semidefinite. Each column of A costs one and lies + outside range(K). The formula hR would predict four instead of the actual + two. Thus a singular positive semidefinite coupling metric is outside + the theorem. +* For A = [u,e_1,e_1] and H = diag(1,1,-1), the same K is obtained. + The outside columns cancel. Its bill is four rather than hR = six. + This escapes confinement but does not supply a cheaper Turyn decoder. + +A diagonal nonnegative metric can discard its zero-weight terms and apply +the theorem to the positive-weight terms. A singular dense metric cannot +generally discard original columns individually, as the first example shows. +Asymmetric factorizations and signed cancellations remain open routes. + +## Verification boundary + +The proof is all-size real linear algebra. The verifier checks new bounded +rational examples, attaining duplications, dense positive definite metric +changes and the boundary counterexamples. Finite checks do not prove the +all-size theorem or re-establish the cited PR598 premises. Independent human +and formal proof-kernel review are unclaimed. No physical supplier, new kappa, +selected-frontier update or complete multiplication theorem follows. All five +selected framework assumptions remain separate. diff --git a/research/turyn-positive-redundancy/README.md b/research/turyn-positive-redundancy/README.md new file mode 100644 index 0000000000..cd1611aaf8 --- /dev/null +++ b/research/turyn-positive-redundancy/README.md @@ -0,0 +1,114 @@ +# Positive redundancy cannot lower the fixed-label Turyn encoder bill + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +For the full Turyn product kernel with its existing 27-bit labels, the exact +encoder support bill with R nonzero columns is B(R)=27R for every R>=512, +when K=A H A^T and H is positive definite. No such factorization exists with +R<512. The minimum over all finite positive redundancy is therefore 13,824. +Each additional nonzero column costs exactly 27, even with a dense positive +definite coupling metric. The metric and scalar operations are granted free. + +DominikScholz's [PR598](https://github.com/CrocSwap/integer-mult-bounds/pull/598) +proves rank 512 and support rank 27 for every nonzero tensor encoder, then +bounds rank-minimal factorizations. This package cites those results as +premises. The new step extends the bill to arbitrary positive redundancy. +Its proof uses the classical positive Gram range identity. No general +linear-algebra priority is claimed, and no predecessor scientific suite is +replayed. [PROOF.md](PROOF.md) gives the theorem, attainers and exact limits. + +This is a historical changed-geometry side result under the current decoder +card, rather than a changed selected P104 supplier. The complete signed +invoice, physical/native realization, ownership, restoration, precision, +compiler, analytic recovery and the five selected assumptions remain outside +scope. No new kappa or complete multiplication theorem is claimed. Independent +human and formal proof-kernel review are unclaimed. + +## Reproduce + +From the repository root with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/turyn-positive-redundancy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/turyn-positive-redundancy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/turyn-positive-redundancy +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/turyn-positive-redundancy --check-source-history +``` + +Another CPython 3.12 executable can replace the absolute interpreter path. +Each direct command prints PASS_TURYN_POSITIVE_REDUNDANCY and generates a +SHA256 receipt for all six package files and the three cited source texts. +The registered launcher also prints PASS_REGISTERED_RESEARCH_PACKAGE. +Authentication of the texts is separate from proving their mathematical +premises. The direct scientific replay needs no Git or network. + +## Evidence and verification design + +The executed domains are 2,511 two-by-two Gram cases from all 81 ternary +encoder matrices and 31 positive definite metrics, 80 rectangular fixtures, +160 fixed-kernel attainers, two metric boundary counterexamples, nine +rejecting controls and one zero-column control. The two-by-two rank histogram +is 31 zero, 992 rank-one and 1,488 rank-two cases. These are enumerated test +cases, not claims about the number of Turyn objects. + +The verifier checks new exact rational examples, including singular encoder +matrices, dense positive definite metrics, attaining duplicate columns and +changes of metric coordinates. Two literal counterexamples reject extending +the individual-column conclusion to singular or indefinite coupling metrics. +Zero columns and invalid support hypotheses have separate controls. The +all-size result comes from the written proof, not finite enumeration. + +The full-label support premise for the small fixtures is checked independently +of the encoder columns: for each nonzero binary label functional, restricting +the kernel to rows on which it is one must retain full real rank. This is +equivalent to saying no nonzero range vector has its active labels in that +functional's kernel. It does not enumerate or test the Turyn ports. + +All loops are bounded by fixed finite domains. Matrices have at most 32 rows +or columns including concatenations; label width is at most five. Functions +are shorter than 60 lines, there is no recursion or dynamic code execution, +and failures use explicit exceptions that remain active under optimization. +Files read for authentication and receipts are each bounded to one MiB. +Warning-strict normal and optimized replays are the available diagnostics. +No new static-analysis configuration or external dependency is needed. + +Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python +allocates integers, Fractions, lists and dictionaries during this bounded +finite replay. Fixed dimensions and coefficient grids, streamed cases, no +retained case history and a 120-second registered timeout constrain resources. +Normal and optimized replays check the same domains. A physical implementation +would need a separate fixed-capacity arithmetic and storage analysis. + +## Open next questions + +1. Can signed or asymmetric factorizations beat 13,824 with these labels? + Start with explicit outside-range columns, an exact full kernel identity + and every support charge. No such factorization or scalar word is supplied. +2. Can a singular positive semidefinite metric save complete circuit cost? + Price its application and output restoration before counting sparse columns + as a gain. The two-port example only demonstrates the theorem's boundary. + +Structured questions and blockers are in [TASK.json](TASK.json). + +## Credit, provenance and overlap + +Credit DominikScholz / PR598 for the explicit opening, geometry, kernel, labels, +rank and support theorem; R. J. Turyn, J. H. Conway, N. J. A. Sloane, Gabriele +Nebe and the geometry/native lineage retained by that package. The classical +Gram range identity and duplication construction are methods, not general +priority claims. The original source files and their credit are unchanged. + +[SOURCES.json](SOURCES.json) pins the three premise texts and the task and +selected-record provenance at canonical main +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. The source's +historical nominal kappa is not the selected result. The selected record at +this base is PR6030 with kappa 0.003125804. + +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362323) +reserves the positive-redundancy question. Live open PRs, handoffs, local +reservations, recent account work, current main and merged object/formula +searches were checked. The cached refresh covered 387 open PRs and 6,319 +Discussion records, with complete remote pagination; its local note coverage +was sparse, 106 of 8,917 HEAD paths. Direct Git searches supplemented those +omissions, including the predecessor's text files. Unpublished work and +arbitrary historical diffs are outside that coverage. diff --git a/research/turyn-positive-redundancy/SOURCES.json b/research/turyn-positive-redundancy/SOURCES.json new file mode 100644 index 0000000000..275be8f8d7 --- /dev/null +++ b/research/turyn-positive-redundancy/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/leech-lattice/TURYN.txt", + "usage": "input", + "git_blob": "9a167e169c7762e7ecc9e75465b67e29102a4678", + "sha256": "8e9e2fff58bf6304f86c2365c3263bc19b2c9332647cce250e52aeffab333fe9" + }, + { + "path": "research/turyn-port-labels/PROOF.txt", + "usage": "input", + "git_blob": "35350a61d166a6e6d12a4c6b9f4d1d18dd13d89c", + "sha256": "926af92411e16decd9663efdcf3f97b27926cc6dc57ea799e6d217f01d2d8b0e" + }, + { + "path": "research/turyn-port-labels/README.txt", + "usage": "input", + "git_blob": "86612c51e5c43cb9374e6df4443aac2ac09287a2", + "sha256": "d53d200a850e5a92ecb46f860a95e8ba14574c17d9599312fd05b16a8f1db3ff" + } + ] +} diff --git a/research/turyn-positive-redundancy/TASK.json b/research/turyn-positive-redundancy/TASK.json new file mode 100644 index 0000000000..85b7848d62 --- /dev/null +++ b/research/turyn-positive-redundancy/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Exact encoder support bill B(R)=27R for the fixed-label full Turyn kernel, with R nonzero columns and a positive definite coupling metric.", + "scope_change_reason": "The card asks for a complete signed-invoice decoder improvement. This is a historical geometry side result that settles the positive-redundancy subclass of PR598's explicitly open redundant-encoder direction. It supplies no changed P104 itinerary or complete supplier.", + "bottleneck_link": "Narrows one changed-decoder route: increasing positive Gram redundancy cannot lower this fixed-label support bill. Signed/asymmetric or changed-label models remain open; the selected P104 bottleneck is not improved.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified scoped improvement; do not search signed factorizations after proving the positive case.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-size argument; verify.py generates exact finite corroboration and a nine-file SHA256 receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an exact signed or asymmetric factorization of the same full Turyn kernel beat 13,824 under the existing labels?", + "why_it_matters": "These factorizations can have encoder columns outside the tensor range and are not excluded by the positive result.", + "first_step": "Exhibit explicit outside-range columns and an exact complete kernel identity, then enumerate every column's binary label-support rank.", + "blocked_by": "No such lower-bill factorization or fully charged scalar realization is supplied." + }, + { + "question": "Can a singular positive semidefinite coupling metric yield a cheaper complete encoder circuit for the same kernel?", + "why_it_matters": "The two-port example escapes individual-column confinement, but factoring or applying its metric can restore the cost.", + "first_step": "Price one exact source/metric/output circuit including all coupling operations and compare its full encoder and decoder bill.", + "blocked_by": "An algebraic coupling metric is granted free here; no physical implementation or cost contract is provided." + } + ], + "source_question": { + "source": "PR #598", + "author": "DominikScholz", + "path": "research/turyn-port-labels/README.txt", + "question": "Redundant real factorizations outside the tensor column space are excluded from the rank-minimal encoder bound." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362323", + "playbook": "Autonomous local run", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/turyn-positive-redundancy/VERIFY.json b/research/turyn-positive-redundancy/VERIFY.json new file mode 100644 index 0000000000..3b4d29c87a --- /dev/null +++ b/research/turyn-positive-redundancy/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/leech-lattice/TURYN.txt", + "research/turyn-port-labels/PROOF.txt", + "research/turyn-port-labels/README.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact positive Gram range/support cases, attaining redundancy families, metric boundary counterexamples, source hashes and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit checks and generated nine-file hash receipt under optimized Python." + } + ] +} diff --git a/research/turyn-positive-redundancy/verify.py b/research/turyn-positive-redundancy/verify.py new file mode 100644 index 0000000000..19be244f76 --- /dev/null +++ b/research/turyn-positive-redundancy/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of positive redundant encoders. + +Produced by Nick Petalas. Apache-2.0. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LIMIT = 32 +INPUTS = ( + "research/leech-lattice/TURYN.txt", + "research/turyn-port-labels/PROOF.txt", + "research/turyn-port-labels/README.txt", +) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def shape(a): + need(1 <= len(a) <= LIMIT, "row bound") + n = len(a[0]) + need(1 <= n <= LIMIT and all(len(row) == n for row in a), "column bound") + need(all(type(x) in (int, Q) for row in a for x in row), "exact coefficients") + return len(a), n + + +def transpose(a): + shape(a) + return [list(column) for column in zip(*a)] + + +def mul(a, b): + _, n = shape(a) + m, _ = shape(b) + need(n == m, "product shape") + return [[sum(x*y for x, y in zip(row, column, strict=True)) + for column in zip(*b)] for row in a] + + +def eye(n): + need(1 <= n <= LIMIT, "identity bound") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def rank(a): + if not a: + return 0 + m, n = shape(a) + work = [[Q(x) for x in row] for row in a] + pivot_row = 0 + for j in range(n): + pivot = next((i for i in range(pivot_row, m) if work[i][j]), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + divisor = work[pivot_row][j] + work[pivot_row] = [x/divisor for x in work[pivot_row]] + for i in range(pivot_row+1, m): + scale = work[i][j] + work[i] = [x-scale*y for x, y in zip(work[i], work[pivot_row], strict=True)] + pivot_row += 1 + return pivot_row + + +def det(a): + n, m = shape(a) + need(n == m, "square determinant") + work = [[Q(x) for x in row] for row in a] + answer = Q(1) + for j in range(n): + pivot = next((i for i in range(j, n) if work[i][j]), None) + if pivot is None: + return Q(0) + if pivot != j: + work[j], work[pivot] = work[pivot], work[j] + answer = -answer + divisor = work[j][j] + answer *= divisor + for i in range(j+1, n): + scale = work[i][j]/divisor + work[i] = [x-scale*y for x, y in zip(work[i], work[j], strict=True)] + return answer + + +def positive(h): + n, m = shape(h) + need(n == m and h == transpose(h), "symmetric metric") + need(all(det([row[:k] for row in h[:k]]) > 0 for k in range(1, n+1)), + "positive definite metric") + + +def confinement(a, h, k): + n, r = shape(a) + need(shape(h) == (r, r) and shape(k) == (n, n), "factorization shape") + positive(h) + need(mul(mul(a, h), transpose(a)) == k, "factorization endpoint") + rk = rank(k) + need(rank(a) == rk, "equal Gram and encoder ranks") + joined = [x+y for x, y in zip(k, a, strict=True)] + need(rank(joined) == rk, "encoder confinement") + return rk + + +def binary_rank(labels): + basis = {} + for label in labels: + for pivot in range(4, -1, -1): + if not (label >> pivot) & 1: + continue + if pivot in basis: + label ^= basis[pivot] + else: + basis[pivot] = label + break + return len(basis) + + +def full_support(k, labels, h): + n, m = shape(k) + need(n == m and len(labels) == n and 1 <= h <= 5, "support shape") + need(all(type(x) is int and 0 <= x < 2**h for x in labels), "binary labels") + rk = rank(k) + need(rk > 0, "nonzero kernel") + for functional in range(1, 2**h): + rows = [row for row, label in zip(k, labels, strict=True) + if (label & functional).bit_count() % 2] + need(rank(rows) == rk, "full-support range hypothesis") + return rk + + +def bill(a, labels): + _, n = shape(a) + costs = [binary_rank([label for row, label in zip(a, labels, strict=True) if row[j]]) + for j in range(n)] + nonzero = sum(any(row[j] for row in a) for j in range(n)) + return sum(costs), nonzero + + +def small_gram_cases(): + counts = {"0": 0, "1": 0, "2": 0} + metrics = [[[a, b], [b, c]] for a, b, c in product(range(1, 4), range(-3, 4), range(1, 4)) + if a*c > b*b] + for values in product(range(-1, 2), repeat=4): + a = [list(values[:2]), list(values[2:])] + # Independent two-by-two rank oracle, including singular and zero A. + oracle = 2 if values[0]*values[3] != values[1]*values[2] else int(any(values)) + for h in metrics: + k = mul(mul(a, h), transpose(a)) + rk = confinement(a, h, k) + need(rk == oracle, "two-by-two rank oracle") + counts[str(rk)] += 1 + return {"metrics": len(metrics), "cases_by_rank": counts} + + +def rectangular_cases(): + count = 0 + for n, r, seed in product(range(1, 5), range(1, 6), range(4)): + a = [[((i+1)*(j+1)+seed) % 5-2 for j in range(r)] for i in range(n)] + c = [[(2*i+j+seed) % 5-2 for j in range(r)] for i in range(r)] + h = mul(transpose(c), c) + for i in range(r): + h[i][i] += 1 + confinement(a, h, mul(mul(a, h), transpose(a))) + count += 1 + return count + + +def duplication(u, extra): + _, r = shape(u) + a = [[row[0]]*(extra+1)+row[1:] for row in u] + h = eye(r+extra) + for i in range(extra+1): + h[i][i] = Q(1, extra+1) + return a, h + + +def attaining_cases(): + count = 0 + for h, r in product(range(1, 6), range(1, 5)): + u = [[int(i == j) for j in range(r)] for _ in range(h) for i in range(r)] + labels = [1 << block for block in range(h) for _ in range(r)] + k = mul(u, transpose(u)) + need(full_support(k, labels, h) == r, "repeated-coordinate premise") + for extra in range(4): + a, metric = duplication(u, extra) + for coupled in (False, True): + p, inverse = eye(r+extra), eye(r+extra) + if coupled and r+extra > 1: + p[0][-1], inverse[0][-1] = 2, -2 + candidate = mul(a, p) + transformed = mul(mul(inverse, metric), transpose(inverse)) + need(confinement(candidate, transformed, k) == r, "attainer rank") + cost, nonzero = bill(candidate, labels) + need(nonzero == r+extra and cost == h*nonzero, "exact redundancy tariff") + count += 1 + return count + + +def boundary_cases(): + k = [[1, 1], [1, 1]] + need(full_support(k, [1, 2], 2) == 1, "boundary full-support premise") + examples = [(eye(2), k, 2), ([[1, 1, 1], [1, 0, 0]], + [[1, 0, 0], [0, 1, 0], [0, 0, -1]], 4)] + for a, metric, expected_cost in examples: + need(mul(mul(a, metric), transpose(a)) == k, "boundary exact endpoint") + need(rank([x+y for x, y in zip(k, a, strict=True)]) > rank(k), + "boundary escapes range confinement") + cost, nonzero = bill(a, [1, 2]) + need(cost == expected_cost and cost < 2*nonzero, "boundary refutes hR extension") + return len(examples) + + +def rejection_cases(): + a, k = [[1], [1]], [[1, 1], [1, 1]] + cases = [(a, [[0]], k), (a, [[-1]], k), (a, [[1]], eye(2)), + (eye(2), [[1, 1], [0, 1]], eye(2)), + (eye(2), [[1, 1], [1, 1]], [[1, 1], [1, 1]])] + count = 0 + for a, metric, target in cases: + try: + confinement(a, metric, target) + except ValueError: + count += 1 + else: + raise ValueError("invalid factorization accepted") + for target, labels, h in [(k, [1, 1], 2), (eye(2), [1, 2], 2), + (k, [1, 4], 2), (k, [1], 2)]: + try: + full_support(target, labels, h) + except ValueError: + count += 1 + else: + raise ValueError("invalid support premise accepted") + return count + + +def bounded_bytes(path): + need(path.stat().st_size <= 1024*1024, "file size bound") + raw = path.read_bytes() + need(len(raw) <= 1024*1024, "read size bound") + return raw + + +def authenticate(): + manifest = json.loads(bounded_bytes(HERE/"SOURCES.json")) + need(len(manifest["files"]) <= 8, "source row bound") + pins = {row["path"]: row for row in manifest["files"] if row["usage"] == "input"} + need(set(pins) == set(INPUTS), "explicit theorem-source inputs") + for path in INPUTS: + need(sha256(bounded_bytes(ROOT/path)).hexdigest() == pins[path]["sha256"], + "cited theorem source hash") + + +def main(): + authenticate() + result = {"small_gram": small_gram_cases(), "rectangular_gram": rectangular_cases(), + "fixed_kernel_attainers": attaining_cases(), "metric_boundaries": boundary_cases(), + "rejecting_controls": rejection_cases()} + a = [[1, 0], [1, 0]] + need(confinement(a, eye(2), [[1, 1], [1, 1]]) == 1, "zero-column confinement") + need(bill(a, [1, 2]) == (2, 1), "zero-column tariff") + result["zero_column_controls"] = 1 + print(json.dumps(result, sort_keys=True)) + receipt = {name: sha256(bounded_bytes(HERE/name)).hexdigest() for name in FILES} + receipt.update({path: sha256(bounded_bytes(ROOT/path)).hexdigest() for path in INPUTS}) + print(json.dumps({"generated_sha256_receipt": receipt}, sort_keys=True)) + print("PASS_TURYN_POSITIVE_REDUNDANCY") + + +if __name__ == "__main__": + main()