diff --git a/research/common-prefix-minor-frontier/PROOF.md b/research/common-prefix-minor-frontier/PROOF.md new file mode 100644 index 0000000000..24a38bef77 --- /dev/null +++ b/research/common-prefix-minor-frontier/PROOF.md @@ -0,0 +1,134 @@ +# Sharp adaptive choice among higher-rank tests with shared columns + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let F be any finite field of order q. Fix integers 1 <= k < m and let +t=m-k+1 >= 2. Let G be uniform in GL_m(F), and let U be its first k rows. +Write U=[C B], where C consists of the first k-1 columns and B has t columns. +For each nonzero v in F^t define the rank-k determinant test + + d_v(U) = det [C, Bv]. + +Multiplying v by a nonzero scalar does not change its zero set. A nonempty +family contains at most M projectively distinct vectors, fixed before inspecting +G. A selector may inspect the entire G and choose any member of that family. +It fails precisely when its chosen determinant vanishes. These are actual +k-column tests after a fixed invertible input chart for each v. Each v extends +the first k-1 coordinate vectors to an independent k-tuple. They need not all +be coordinate minors in one common chart. + +Put + + D = product_{j=0}^{k-1} (q^m-q^j), + R = product_{j=0}^{k-2} (q^k-q^j), + A = R q^(kt-2) (q-1) / D. + +An empty product equals one. For every integer M>=1, the maximum failure +probability over such families and selectors is exactly + + P*(q,m,k,M) = 1 - A max(q+1-M, 0). (1) + +In particular q+1 candidates suffice for failure on every matrix. This is +a sharp result for this shared-column family. It is not a bound for arbitrary +rank-k minors, arbitrary matrix distributions or current-dependent families. + +## 1. The top frame is uniform + +There are D full-row-rank k-by-m matrices. Choose the rows in order. After +j independent rows, q^j vectors are forbidden for the next row. Every such +matrix U has exactly + + product_{j=k}^{m-1} (q^m-q^j) + +invertible completions to G, independent of U. Thus U is uniform on those D +matrices. Giving the selector access to the remaining rows changes neither +the set on which some candidate fails nor its probability. A selector that +chooses the first failing candidate whenever one exists attains that union. + +## 2. Separate the common failure from the quotient test + +If rank C < k-1, every d_v vanishes. If rank C=k-1, the quotient F^k/im C +is one-dimensional. Choose an arbitrary isomorphism of that quotient with F. +The quotient of B is a row z in F^t, and + + d_v(U)=0 if and only if z dot v=0. + +Full row rank of U forces z nonzero. For each fixed full-rank C, every +nonzero z has exactly q^((k-1)t) lifts B. This number does not depend on z, +so z is uniform on F^t minus zero conditional on C. Choosing a different +quotient coordinate scales z and leaves all its zero tests unchanged. + +There are R possible full-rank C. Therefore the probability gamma of an +independent shared prefix is + + gamma = R q^((k-1)t) (q^t-1) / D. (2) + +The common-prefix deficiency contributes 1-gamma before any adaptive +choice. No independence between the candidate failure events is assumed. + +## 3. The remaining union is sharp + +This is the one-linear-minor geometry cited from ywz65's #2601. The short +argument is included to make the new reduction self-contained. A nonzero v +defines a hyperplane in F^t. For s distinct such hyperplanes, the first has +q^(t-1) points and each further one adds at most q^(t-1)-q^(t-2), because +its intersection with the first already has q^(t-2) points. Consequently, +for 1<=s<=q+1, their union on nonzero z has fraction at most + + b_s = [q^(t-2)(1+s(q-1))-1] / (q^t-1). (3) + +Equality holds for any s members of the pencil with normals + + (1,a,0,...,0) for a in F, and (0,1,0,...,0). + +Their pairwise intersections are all the same codimension-two subspace, +and their parts outside that subspace are disjoint. All q+1 members cover +F^t. Extra budget cannot improve on probability one. + +Every candidate family has unconditional failure at most + + (1-gamma) + gamma b_M + +until saturation, with the same pencil attaining the bound simultaneously +for every full-rank C. Substituting (2) and (3) and cancelling q^t-1 gives +(1), since + + 1-b_M = q^(t-2)(q-1)(q+1-M)/(q^t-1). + +This proves the theorem for every finite field, including extension fields. +The finite verifier corroborates small cases; it does not supply these +unbounded quantifiers. + +## 4. A concrete higher-rank boundary + +At q=2, m=3, k=2 there are 42 full-row-rank top frames. Six have a zero +shared column. Formula (1) gives failure probabilities 3/7, 5/7 and 1 for +budgets one, two and three. In particular two candidates give 5/7, whereas +twice the single-test rate is 6/7 and the conditional linear-only rate is +2/3. The common failure event must be counted once, and cannot be omitted. +Every frame has four GL_3(F_2) completions, so the corresponding literal +invertible-matrix counts are 72, 120 and 168 out of 168. + +At q=3, m=3, k=2 the rates are 4/13, 7/13, 10/13 and 1. These are examples +of the theorem's new shared-column contract, not measurements of the +selected stopped producer. + +## Scope and credit + +The original step is the higher-rank shared-prefix reduction, its exact +common-deficiency term, and the resulting sharp formula (1). ywz65's +PR #2601 supplies the bounded-choice interface, projective-pencil formula +and higher-rank-intersection question. Adam Gall's PR #2097 supplies the +fresh-row versus current-dependent-selection boundary, with its retained +three-stage-cover, eumemic source527, Rohan Arun, Jeremy Kothe and PR589 +lineage. Matrix completion counts and projective pencils are classical. +No general literature-priority claim is made for these counting methods. + +No actual selected candidate family, eligible-prime proof, current-field +transcript, physical selector, routing, dirty restoration, complete paid +invoice or all-size supplier is supplied. The selected five framework +assumptions remain. This is a scoped written proof with finite exact +corroboration, with no new kappa or complete multiplication theorem. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/common-prefix-minor-frontier/README.md b/research/common-prefix-minor-frontier/README.md new file mode 100644 index 0000000000..4cbdd06053 --- /dev/null +++ b/research/common-prefix-minor-frontier/README.md @@ -0,0 +1,137 @@ +# Sharp adaptive choice among higher-rank minors with shared columns + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped proof with exact finite corroboration. For a uniform +G in GL_m(F_q), let U be its first k rows, where 1<=k=1 candidates is + +```text +1 - A max(q+1-M, 0), +A = q^(kt-2) (q-1) product_{j=0}^{k-2}(q^k-q^j) + / product_{j=0}^{k-1}(q^m-q^j). +``` + +A projective pencil attains it over every finite field. At q=2,m=3,k=2, +the rates for one, two and three choices are 3/7, 5/7 and 1. This resolves +a concrete family in the higher-rank-intersection direction of ywz65's +[PR #2601](https://github.com/CrocSwap/integer-mult-bounds/pull/2601), +Open next question 2. Its linear-minor theorem is cited, not re-audited. +The new step is the exact common-column deficiency term and its combination +with the quotient test. [PROOF.md](PROOF.md) gives the all-field argument. + +These determinant tests correspond to fixed input charts that share their +first k-1 columns. They need not be coordinate minors in one common chart. +The result does not identify the selected caller's actual bad varieties, +construct a physical selector, improve kappa or change the selected frontier. + +## Exact evidence + +The verifier enumerates every full-row-rank matrix and every nonempty +projective candidate family in five domains. Gaussian elimination selects +the full-row-rank frames; the permutation determinant expansion evaluates +every candidate. It computes each family's literal union count and maximizes +over all families within each budget, rather than assuming pencil optimality. + +```text +q m k full-row-rank frames candidate families deficient prefixes +2 3 2 42 7 6 +3 3 2 624 15 48 +4 3 2 3780 31 180 +2 4 2 210 127 42 +2 4 3 2520 7 504 +``` + +That is 7,176 frames and 187 families across the five domains. F_4 uses +F_2[x]/(x^2+x+1), not arithmetic modulo four. Separate literal GL_3 censuses +cover all 168 binary and 11,232 ternary invertible matrices and compare +complete candidate-failure-mask frequencies with their top-frame fibers. +There are seven rejected formula-domain calls and seven semantic comparisons. +All acceptance checks use explicit exceptions and stay active under -O. + +## Reproduce + +From the repository root, with the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/common-prefix-minor-frontier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/common-prefix-minor-frontier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/common-prefix-minor-frontier +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/common-prefix-minor-frontier --check-source-history +``` + +Another CPython 3.12 path can replace the absolute interpreter path. The +verifier writes nothing and emits JSON with `PASS_COMMON_PREFIX_MINOR_FRONTIER`, +the enumerated results and SHA256 hashes of all six package files. Redirect +stdout outside the checkout to retain a generated receipt. Both registered +commands have 60-second limits. Local warning-strict ordinary and optimized +checks, metadata and publication-byte/source-history checks are required. +Hosted CI status is recorded separately in the PR body. + +The direct verifier also runs from a Git-free copy of this package. Exact +source pins are historical provenance only. No predecessor executable is +imported, and there are no external live inputs. + +## Limits and attribution + +The all-finite-field quantifier follows from the written proof. The exhaustive +checks cover only the five stated domains. Arbitrary higher-rank minor families, +nonuniform matrices, current-dependent candidate preparation and a fully charged +selected caller remain outside scope. Physical reads, routes, restoration, +transcript emission, eligible-prime arguments and all five selected framework +assumptions remain open. No native, Lean, Docker or selected scientific cold +replay was run. Independent human and formal proof-kernel review are unclaimed. + +Credit ywz65's #2601 for the question, bounded-choice interface and sharp +linear-minor pencil bound. Credit Adam Gall's #2097 for the fresh-row versus +adaptive-selection boundary, with the retained three-stage-cover, eumemic +source527, Rohan Arun, Jeremy Kothe and PR589 lineage. Finite-field matrix +completion counts and projective pencils are classical; no general literature +priority is claimed for those methods. No predecessor text or code is copied. + +Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The task picker suggested `replay-runtime`. [TASK.json](TASK.json) explicitly +changes it to this algebraic counting side result because the assignment +requires an original result rather than an audit. The selected orientation +passed `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it is metadata orientation, +not scientific evidence for this theorem. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221368) +reserves this exact shared-column question. Live account PRs, current open +PRs and Discussions, merged-PR searches and tracked-main README searches +were checked. The overlap snapshot had 341 open PRs and 5,519 Discussion +records with complete remote pagination. Its local sparse coverage was +incomplete, so direct Git searches supplemented it. Unpublished work and +arbitrary code diffs are outside those checks. + +## Open next questions + +1. Does an actual stopped-cover caller expose a fixed candidate family of + this shared-column form? First export its exact input charts and field + distribution. Such an adapter, eligible-prime coverage, a complete current- + field transcript and the physical selector bill are missing. +2. What is the sharp bound when only k-2 columns are shared? The quotient + then has dimension two, and failure is a two-column determinant rather + than a hyperplane. Start with one specified two-plane candidate family + over F_2 and its literal GL distribution. Its intersection geometry is + not covered by the one-dimensional reduction here. + +## Verifier bounds + +The verifier has no recursion, subprocesses, network use or write path. +Every matrix enumeration has at most 19,683 candidates; matrices have at +most four columns and three rows. Permutation determinants have at most +six terms. Candidate sets have at most seven projective points and 127 +nonempty families. Functions are below 60 physical lines. Package reads +are bounded to 256 KiB each. Warning-strict normal and optimized execution +and in-memory syntax inspection supply diagnostics. + +Python exact integers, lists and runtime calls allocate during this bounded +offline check. These are managed-runtime deviations from Power of Ten static +allocation and indirect-call restrictions. All call targets are fixed, +collections have the stated bounds, and there is no persistent shared state. +Larger executable domains require new capacity bounds before use. diff --git a/research/common-prefix-minor-frontier/SOURCES.json b/research/common-prefix-minor-frontier/SOURCES.json new file mode 100644 index 0000000000..0aeb1a5979 --- /dev/null +++ b/research/common-prefix-minor-frontier/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bounded-row-choice/README.md", + "usage": "provenance", + "git_blob": "883ff97ee8eda15816ca36fcfb1d556670f12e76", + "sha256": "733053426538d3f1370fd48dfc3a3d4ce1fb5504d9322435541a5480fd60c912" + }, + { + "path": "research/bounded-row-choice/PROOF.md", + "usage": "provenance", + "git_blob": "1ea461858a08bcfc570d7810bde1e29869c69810", + "sha256": "3eea3e95cf606ee5ab305678b24b1b31d15b2acb816fb604c2285da74d4ca83a" + } + ] +} diff --git a/research/common-prefix-minor-frontier/TASK.json b/research/common-prefix-minor-frontier/TASK.json new file mode 100644 index 0000000000..421f652a7e --- /dev/null +++ b/research/common-prefix-minor-frontier/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp adaptive failure probability for fixed rank-k determinant tests sharing k-1 source columns under uniform GL_m(F_q).", + "scope_change_reason": "The assignment requires an original result. Extend PR2601 open question 2 by reducing a concrete higher-rank family to its common-deficiency event and quotient pencil; this is an algebraic side result, not a replay-runtime optimization or an audit.", + "bottleneck_link": "Bounded current-field choice requires family-specific bad-variety counting. This supplies one exact higher-rank contract; the actual selected candidate adapter and complete physical bill remain missing.", + "budget_minutes": 60, + "stop_rule": "Stop at the first independently enumerable sharp formula and package it; do not extend to two-dimensional quotients or a new construction.", + "outcome": "completed", + "evidence": "PROOF.md all-finite-field argument; verify.py exhaustive five-domain matrix/family census and literal binary/ternary GL_3 completion checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a selected caller have this shared-column candidate form?", + "why_it_matters": "Only then can this counting law replace its candidate-union estimate.", + "first_step": "Export fixed charts, exact fresh-field distribution and complete transcript for one actual caller.", + "blocked_by": "No selected adapter, eligible-prime proof or complete physical selector bill is supplied." + }, + { + "question": "What is the sharp bound when k-2 columns are shared?", + "why_it_matters": "A two-dimensional quotient would cover a larger class of minor families.", + "first_step": "Specify one two-plane candidate family over F_2 and enumerate its literal GL distribution.", + "blocked_by": "The determinant intersection geometry is no longer a hyperplane pencil." + } + ], + "question_source": { + "pr": 2601, + "author": "ywz65", + "question": "Open next question 2: higher-rank bad-minor intersections", + "head": "9839b45aec3233b6214e01209a2001b514ed4838" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221368", + "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; no selected scientific cold replay", + "overlap": { + "canonical_main": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "open_prs": 341, + "open_prs_fetched_at": "2026-10-27T16:02:48.832900+00:00", + "discussion_records": 5519, + "discussions_fetched_at": "2026-10-27T16:03:58.384020+00:00", + "remote_complete_pagination": true, + "local_sparse_incomplete": true, + "checks": "Live account PR titles/bodies; latest handoff comments and active discussions; main README grep; distinctive merged-PR searches; local batch reservation. No same-question prior work found.", + "limitations": "No unpublished work or arbitrary historical diffs. Sparse notes supplemented by tracked-main searches." + }, + "validation": { + "interpreter": "CPython 3.12.15, macOS arm64", + "direct_warning_strict": "normal and optimized passed", + "registered_replay": "both 60-second commands passed locally", + "direct_seconds": [ + 0.29, + 0.3 + ], + "registered_total_seconds": 0.91, + "mutation_controls": "wrong q exponent, missing common-failure contribution and Z/4 in place of F_4 rejected in disposable optimized CLI copies", + "scope": "Local checks only; hosted CI and independent human/formal review not claimed." + }, + "final_overlap_checkpoint": { + "utc": "2026-10-27T16:09:58.482916+00:00", + "origin_main": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "result": "No overlapping open PR or peer claim; merged candidates #1920/#2021/#3230/#3689 concern different objects. Source #2601 is retained unchanged." + } +} diff --git a/research/common-prefix-minor-frontier/VERIFY.json b/research/common-prefix-minor-frontier/VERIFY.json new file mode 100644 index 0000000000..e6d5c336e0 --- /dev/null +++ b/research/common-prefix-minor-frontier/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All five complete row-frame/family censuses, literal binary and ternary GL_3 fibers, seven domain rejections and seven semantic comparisons." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete mathematical checks with Python assertions disabled." + } + ] +} diff --git a/research/common-prefix-minor-frontier/verify.py b/research/common-prefix-minor-frontier/verify.py new file mode 100644 index 0000000000..bf838873f5 --- /dev/null +++ b/research/common-prefix-minor-frontier/verify.py @@ -0,0 +1,222 @@ +"""Exact finite corroboration of the shared-column minor theorem. Apache-2.0.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from math import prod +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b, q): + return a ^ b if q == 4 else (a + b) % q + + +def multiply(a, b, q): + if q != 4: + return a * b % q + value = 0 + for bit in range(2): + if b & (1 << bit): + value ^= a << bit + if value & 4: + value ^= 7 # F_2[x]/(x^2+x+1). + return value + + +def inverse(a, q): + require(0 < a < q and q in (2, 3, 4), "invalid inverse input") + for b in range(1, q): + if multiply(a, b, q) == 1: + return b + raise ValueError("not a field element") + + +def dot(a, b, q): + value = 0 + for x, y in zip(a, b, strict=True): + value = add(value, multiply(x, y, q), q) + return value + + +def matrix_rank(rows, q): + work = [list(row) for row in rows] + height, width = len(work), len(work[0]) + pivot = 0 + for column in range(width): + found = next((i for i in range(pivot, height) if work[i][column]), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + scale = inverse(work[pivot][column], q) + work[pivot] = [multiply(x, scale, q) for x in work[pivot]] + for i in range(height): + if i != pivot: + factor = work[i][column] + for j in range(width): + term = multiply(factor, work[pivot][j], q) + work[i][j] = add(work[i][j], term if q == 4 else -term, q) + pivot += 1 + if pivot == height: + break + return pivot + + +def determinant(rows, q): + size = len(rows) + value = 0 + for perm in permutations(range(size)): + term = 1 + for i in range(size): + term = multiply(term, rows[i][perm[i]], q) + inversions = sum(perm[j] > perm[i] for i in range(size) for j in range(i)) + if inversions % 2 and q != 4: + term = -term + value = add(value, term, q) + return value + + +def projective_vectors(q, dimension): + points = [] + for vector in product(range(q), repeat=dimension): + first = next((a for a in vector if a), None) + if first == 1: + points.append(vector) + require(len(points) == (q**dimension - 1) // (q - 1), "projective coverage") + return tuple(points) + + +def predicted(q, m, k, budget): + require(q in (2, 3, 4) and 1 <= k < m <= 8, "unsupported formula domain") + require(1 <= budget <= q + 2, "invalid choice budget") + t = m - k + 1 + total = prod(q**m - q**j for j in range(k)) + prefix = prod(q**k - q**j for j in range(k - 1)) + coefficient = Fraction(prefix * q ** (k * t - 2) * (q - 1), total) + return 1 - coefficient * max(0, q + 1 - budget) + + +def bad_mask(rows, q, points): + k = len(rows) + mask = 0 + for index, vector in enumerate(points): + minor = [tuple(row[: k - 1]) + (dot(row[k - 1 :], vector, q),) for row in rows] + if determinant(minor, q) == 0: + mask |= 1 << index + return mask + + +def family_counts(frequencies, number): + counts = [0] * (1 << number) + for family in range(1, 1 << number): + counts[family] = sum(count for mask, count in enumerate(frequencies) if mask & family) + return counts + + +def check_families(counts, points, q, m, k, total): + maxima = {} + witnesses = {} + for budget in range(1, len(points) + 1): + eligible = [i for i in range(1, len(counts)) if i.bit_count() <= budget] + maximum = max(counts[i] for i in eligible) + require(Fraction(maximum, total) == predicted(q, m, k, min(budget, q + 2)), + "wrong sharp higher-rank frontier") + maxima[str(budget)] = maximum + witnesses[str(budget)] = next(i for i in eligible if counts[i] == maximum) + return maxima, witnesses + + +def row_census(q, m, k): + points = projective_vectors(q, m - k + 1) + frequencies = [0] * (1 << len(points)) + prefix_deficient = 0 + total = 0 + for entries in product(range(q), repeat=k * m): + rows = tuple(entries[i * m : (i + 1) * m] for i in range(k)) + if matrix_rank(rows, q) != k: + continue + total += 1 + mask = bad_mask(rows, q, points) + frequencies[mask] += 1 + if matrix_rank(tuple(row[: k - 1] for row in rows), q) < k - 1: + prefix_deficient += 1 + require(mask == len(frequencies) - 1, "deficient prefix must fail every test") + require(total == prod(q**m - q**j for j in range(k)), "full-row-rank count") + t = m - k + 1 + good_prefix = prod(q**k - q**j for j in range(k - 1)) * q ** ((k - 1) * t) * (q**t - 1) + require(total - prefix_deficient == good_prefix, "prefix-deficiency count") + counts = family_counts(frequencies, len(points)) + maxima, witnesses = check_families(counts, points, q, m, k, total) + return {"q": q, "m": m, "k": k, "matrices": total, + "prefix_deficient": prefix_deficient, "families": len(counts) - 1, + "max_bad_counts": maxima, "witness_family_masks": witnesses, + "frequency_sha256": sha256(json.dumps(frequencies).encode()).hexdigest()}, frequencies + + +def gl_census(q, expected_frequencies): + m, k = 3, 2 + points = projective_vectors(q, 2) + frequencies = [0] * (1 << len(points)) + for entries in product(range(q), repeat=9): + rows = tuple(entries[3 * i : 3 * i + 3] for i in range(3)) + if determinant(rows, q) == 0: + continue + require(matrix_rank(rows, q) == 3, "GL determinant/rank disagreement") + frequencies[bad_mask(rows[:k], q, points)] += 1 + completions = q**3 - q**2 + require(frequencies == [completions * x for x in expected_frequencies], + "literal GL fibers are not equal") + return {"q": q, "dimension": m, "matrices": sum(frequencies), + "completions_per_top_frame": completions} + + +def controls(): + rejected = 0 + for args in ((1, 3, 2, 1), (6, 3, 2, 1), (2, 2, 2, 1), + (2, 3, 0, 1), (2, 9, 2, 1), (2, 3, 2, 0), (2, 3, 2, 5)): + try: + predicted(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("out-of-domain formula accepted") + require(multiply(2, 2, 4) == 3 and multiply(2, 3, 4) == 1, "F4 is not Z/4") + require(determinant(((1, 2), (3, 1)), 4) == 0, "F4 determinant control") + require(predicted(2, 3, 2, 1) == Fraction(3, 7), "one-choice boundary") + require(predicted(2, 3, 2, 2) == Fraction(5, 7), "two-choice boundary") + require(predicted(2, 3, 2, 3) == predicted(2, 3, 2, 4) == 1, "saturation") + require(predicted(2, 3, 2, 2) != Fraction(2, 3), "shared deficiency cannot be omitted") + require(predicted(2, 3, 2, 2) != 2 * predicted(2, 3, 2, 1), "union bound not sharp") + return {"invalid_domains_rejected": rejected, "semantic_comparisons": 7} + + +def main(): + require(len(sys.argv) == 1, "this fixed verifier accepts no arguments") + cases = [] + gl_cases = [] + for q, m, k in ((2, 3, 2), (3, 3, 2), (4, 3, 2), (2, 4, 2), (2, 4, 3)): + result, frequencies = row_census(q, m, k) + cases.append(result) + if m == 3 and q in (2, 3): + gl_cases.append(gl_census(q, frequencies)) + receipt = {"status": "PASS_COMMON_PREFIX_MINOR_FRONTIER", "claim_type": "scoped proof", + "row_censuses": cases, "literal_GL_censuses": gl_cases, "controls": controls(), + "python": sys.version, "no_new_kappa": True} + package = Path(__file__).resolve().parent + receipt["sha256"] = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + with (package / name).open("rb") as handle: + data = handle.read(262145) + require(len(data) <= 262144, "package file exceeds read bound") + receipt["sha256"][name] = sha256(data).hexdigest() + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()