diff --git a/research/radical-all-field-count/README.md b/research/radical-all-field-count/README.md new file mode 100644 index 0000000000..1e846af58c --- /dev/null +++ b/research/radical-all-field-count/README.md @@ -0,0 +1,185 @@ +# Exact radical reachability counts over every finite field + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped counting proof with finite corroboration. This answers +Open next question 2 of [#4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745), +at `3edea13af13b755932852e9306a714b317630dda`. That predecessor proves the +reachability criterion over arbitrary fields and gives its binary count. +The new result is the exact count over every finite field. No new kappa is +claimed, and the predecessor theorem is used as a cited step, not audited. + +Let K=F_q and R=K direct-sum J be a split unital central K-algebra with +J squared zero and finite d=dim_K J. The alphabet has paid factors I+u y^T, +u in R squared, y in K squared, and common free GL_2(K) maps. For radical +targets M in M_2(J), put z=q^d and + +```text +A_r(z) = product_(i=0,...,r-1) (z-q^i). + +unreachable(q,d) = A_4(z) + q(q^2-1) A_3(z) + + [q^2(q-1)^2/2] A_2(z), +reachable(q,d) = z^4 - unreachable(q,d). (1) +``` + +Every target counted as reachable has exact paid cost two; every remaining +target is unreachable at any finite word length. This cost interpretation +is #4745's theorem. The counts include d=0, when the only target is zero +and its formal cost is still two. Products with r>d vanish because one +factor is zero. + +At q=3,d=2 the counts are **5,697 reachable and 864 unreachable** out of +6,561. At q=3,d=3 they are **250,641 and 280,800** out of 531,441. +At q=4,d=2 they are **52,576 and 12,960** out of 65,536. F_4 here is the +field F_2[t]/(t^2+t+1), not integers modulo four. + +## Proof + +Choose a basis epsilon_1,...,epsilon_d of J and write +M=sum_j A_j epsilon_j, with A_j in the four-dimensional space V=M_2(K). +Use the nondegenerate entrywise pairing on V. By #4745, M is reachable +exactly when some nonzero row phi and column v have phi A_j v=0 for every j. +Equivalently, S=span(A_1,...,A_d)-perpendicular contains a nonzero rank-one +matrix, whose entries are phi_i v_j. Thus M is unreachable exactly when +every nonzero matrix in S is invertible. + +We count such subspaces S by their dimension s. Evaluation T maps to T e_1 +is injective on S, because a nonzero matrix killing e_1 would be singular. +Therefore s<=2. The numbers N_s of possible subspaces are + +```text +N_0=1, N_1=q(q^2-1), N_2=q^2(q-1)^2/2. (2) +``` + +The line count is |GL_2(K)|/(q-1)=q(q^2-1). To prove the plane count, +count ordered bases (A,B) of all allowed planes. Necessarily A is invertible. +Set C=A^-1 B. The plane has no nonzero singular matrix exactly when +det(a I+b C) is nonzero for every (a,b) other than (0,0). For b nonzero, +this says that C has no eigenvalue in K. For a two-by-two matrix this is +equivalent to its characteristic polynomial being irreducible of degree two. + +There are (q^2-q)/2 monic irreducible quadratic polynomials: partition +F_(q^2) minus F_q into its two-element Frobenius orbits. All matrices with +one such polynomial are conjugate to its companion matrix. Its centralizer +is K[C], since any nonzero vector w makes (w,Cw) a basis and a commuting +map is determined by its value on w. The invertible centralizer therefore +has q^2-1 elements. Each conjugacy class has +|GL_2(K)|/(q^2-1)=q^2-q matrices. Hence the number of possible C is +(q^2-q)^2/2. This reasoning works in even characteristic too. + +There are |GL_2(K)| choices for A, and then B=A C is determined. Each +allowed plane is counted by its (q^2-1)(q^2-q) ordered bases. Dividing gives + +```text +N_2 = |GL_2(K)| (q^2-q)^2 / [2(q^2-1)(q^2-q)] + = q^2(q-1)^2/2. +``` + +For each fixed S of dimension s, put W=S-perpendicular. The coefficient +tuple (A_1,...,A_d) must span the fixed (4-s)-dimensional W. Relative to +any basis of W, these tuples are precisely full-row-rank (4-s)-by-d +matrices. Choosing their independent rows gives A_(4-s)(q^d) tuples. +The annihilator S of each tuple is unique, so there is no double counting. +Summing N_s A_(4-s)(z) for s=0,1,2 proves (1). + +For q=2, expansion gives reachable=9z^3-30z^2+42z-20, exactly the +predecessor's binary law. That specialization retains predecessor credit. +The matrix-space and finite-geometry counts in (2) are classical. In +projective language the planes are external lines to the determinant +hyperbolic quadric. See, for example, Tatsuya Fujisaki's +[2003 paper](https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1299-12.pdf) +for that established geometric setting. The contribution here is their +application to the all-field formal-alphabet target count, with the proof +given above; no novelty is claimed for the classical plane enumeration. + +## Evidence and reproduction + +The standard-library verifier imports no predecessor executable. It directly +enumerates coefficient tuples and intersects their literal bilinear-zero +sets. Over q=2 it covers d=0,...,4, over q=3 it covers d=0,...,3, and +over q=4,5,7 it covers d=0,...,2. +These are **6,832,236 target tuples**. Every reachable/unreachable count +agrees with (1). It separately enumerates **5,580 subspaces** by unique +reduced row-echelon bases and checks each for rank-one matrices. The allowed +plane counts at q=2,3,4,5,7 are respectively 2,18,72,200,882. A third +calculation counts matrices with no field eigenvalue and checks the +irreducible-matrix formula used in the proof. + +Seven control groups distinguish a shared chart from separate coefficient +charts, reject three changed counting expressions against literal target +censuses, distinguish F_4 from Z/4Z, and enforce field/domain capacities. +The binary overlap gives (reachable,unreachable)=(244,12) at d=2 and +(3004,1092) at d=3, agreeing numerically with #4745/#4276. At binary d=4, +the new census gives (29836,35700), including the full-span term A_4(16) +that vanishes at every lower dimension. This is a +compatibility check accompanying the new count, not a predecessor review. +All reported census totals are generated by the loops that enumerate them. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/radical-all-field-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/radical-all-field-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/radical-all-field-count +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/radical-all-field-count --check-source-history +``` + +Any CPython 3.12 installation may replace the absolute local path. The marker +is `PASS_RADICAL_ALL_FIELD_COUNT`. Each execution prints a generated JSON +receipt binding all five package files by SHA256 and writes nothing. No +handwritten receipt is committed. Ordinary and optimized Python use the same +explicit checks. The universal claim rests on the written proof and the +cited reachability theorem, not extrapolation from the finite census. + +## Scope, source boundary and implementation decisions + +The algebra is split, has scalar residue K, has two roles, and has J^2=0. +Only targets with all entries in J are counted. Other singular targets, +higher nilpotency, more roles and nonfield residue rings are outside scope. +No request producer, native coefficient preparation, physical routing, +restoration, stock, precision or complete consumer invoice is supplied. +Those costs remain unknown. No supplier admission, complete multiplication +theorem or selected-frontier change follows. Independent human and formal +proof-kernel review are unclaimed. Lean, Docker and selected cold replay +were not run, and no proof-assistant formalization is claimed. + +The formal-interface-lemma card is explicitly changed to this algebraic side +question because #4745 leaves it open. The historical card's first baseline +was attempted and stopped at the omitted sparse input +`research/fresh-helper-thinned/PROOF.md`; it did not pass. This is not a +supplier expansion. The predecessor is an exact-head citation in TASK.json, +not an imported executable or an undeclared dependency on its Git objects. +The package is self-contained computationally. SOURCES.json pins main's +catalogue and selected record as historical provenance only. + +Verifier loops have fixed q<=7, d<=4, four-dimensional vector spaces and +at most 5,764,801 streamed tuples in one census. Only at most 2,401 masks, +64 bits per mask, field tables and one basis/tuple persist during a scan. +No recursive calls, subprocesses, dynamic code or indirect callback targets +are used. Functions remain under 60 lines. Explicit exceptions remain active +under -O, and warnings are errors. CPython allocates integers and containers +while scanning; this is the managed-runtime deviation from Power of Ten +rule 3, bounded by the fixed domains above. No additional static analyzer +is configured or claimed. A larger census must declare fresh capacities. + +## Open next questions + +1. For a named radical target, what is the distribution of its number of + projective bilinear-zero pairs, rather than just whether that number is + zero? Start by classifying intersections of its annihilator with the + determinant quadric. This could price a restricted common-chart choice; + an actual physical choice/emission bill remains missing. +2. What second-order obstruction replaces the criterion when J^3=0? + Start with F_2[x,y]/(x,y)^3 as already proposed in #4745. Products of + radical entries survive, so neither this count nor that predecessor's + square-zero invariant settles the question. + +## Credit + +Produced by Nick Petalas. Nick Petalas's #4745 supplies the arbitrary-field +reachability theorem, binary law and explicit all-field counting question; +#4276/#4243 supply the two-factor and free-map lineage. ToikY's #4334 supplies +the shared-chart interface context. Wentao Li's #4099, following #2513, +supplies the right-vector alphabet. Classical irreducible-polynomial, +matrix-centralizer and finite-geometry counts retain their existing credit. +No predecessor files or credit lines are changed. Apache-2.0. diff --git a/research/radical-all-field-count/SOURCES.json b/research/radical-all-field-count/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/radical-all-field-count/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/radical-all-field-count/TASK.json b/research/radical-all-field-count/TASK.json new file mode 100644 index 0000000000..383b055789 --- /dev/null +++ b/research/radical-all-field-count/TASK.json @@ -0,0 +1,117 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact reachable/unreachable counts for radical two-role right-vector targets over every finite field and every square-zero radical dimension.", + "scope_change_reason": "Open next question 2 of PR4745 explicitly asks for the nonbinary counting law. This is a written algebraic side proof, rather than proof-assistant formalization or an audit.", + "bottleneck_link": "Side result: counts the exact feasible common-chart target set in the restricted right-vector alphabet. It does not price a native implementation or admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved all-field formula and bounded direct corroboration; do not extend the model.", + "outcome": "completed", + "evidence": "README.md proof and verify.py: 6,832,236 literal target tuples, 5,580 subspaces, irreducible matrices and seven control groups.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact distribution of the number of projective bilinear-zero pairs for radical targets?", + "why_it_matters": "A restricted chart choice needs more than a zero/nonzero count.", + "first_step": "Classify annihilator intersections with the determinant quadric.", + "blocked_by": "No physical producer, chart selection or emission invoice is specified." + }, + { + "question": "What second-order obstruction replaces the criterion when J^3=0?", + "why_it_matters": "The square-zero argument does not classify higher nilpotency.", + "first_step": "Use F2[x,y]/(x,y)^3 and retain the product of radical terms in the first-zero-residue expansion.", + "blocked_by": "A new reachability invariant is required; inherited from PR4745, not investigated here." + } + ], + "predecessor_citations": [ + { + "pr": 4745, + "head": "3edea13af13b755932852e9306a714b317630dda", + "path": "research/square-zero-radical-reachability/README.md", + "usage": "Cited reachability theorem and binary counting law; no runtime import or Git-history dependency." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131112", + "overlap": { + "open_pr_records": 521, + "discussion_records": 3679, + "main_base": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "local_note_inventory": "Sparse and incomplete; separate git grep searches cover all main README paths. Live PR bodies and claims checked before claiming." + }, + "claim_type": "scoped counting proof with finite corroboration" +} diff --git a/research/radical-all-field-count/VERIFY.json b/research/radical-all-field-count/VERIFY.json new file mode 100644 index 0000000000..8db66224da --- /dev/null +++ b/research/radical-all-field-count/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All-field count corroboration by literal tuples, rank-one-free subspaces, irreducible matrices and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every explicit scientific check with optimized Python." + } + ] +} diff --git a/research/radical-all-field-count/verify.py b/research/radical-all-field-count/verify.py new file mode 100644 index 0000000000..ebd1881c6d --- /dev/null +++ b/research/radical-all-field-count/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Exact finite-field corroboration of the radical target counting law. + +Produced by Nick Petalas. Apache-2.0. No predecessor executable is imported. +""" + +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + + +FIELDS = (2, 3, 4, 5, 7) +MAX_DIM = {2: 4, 3: 3, 4: 2, 5: 2, 7: 2} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field(q): + require(q in FIELDS, "unsupported field order") + if q == 4: + add = tuple(tuple(a ^ b for b in range(q)) for a in range(q)) + rows = [] + for a in range(q): + row = [] + for b in range(q): + c = (a & 1) * b ^ ((a >> 1) * b << 1) + row.append(c ^ (7 if c & 4 else 0)) + rows.append(tuple(row)) + mul = tuple(rows) + else: + add = tuple(tuple((a + b) % q for b in range(q)) for a in range(q)) + mul = tuple(tuple(a * b % q for b in range(q)) for a in range(q)) + neg = tuple(next(b for b in range(q) if add[a][b] == 0) for a in range(q)) + for a in range(1, q): + require(any(mul[a][b] == 1 for b in range(1, q)), "nonunit in field") + for a, b, c in product(range(q), repeat=3): + require(mul[a][add[b][c]] == add[mul[a][b]][mul[a][c]], "distributivity") + require(mul[mul[a][b]][c] == mul[a][mul[b][c]], "associativity") + return add, mul, neg + + +def determinant(a, add, mul, neg): + return add[mul[a[0]][a[3]]][neg[mul[a[1]][a[2]]]] + + +def bilinear_masks(q, add, mul): + lines = tuple((1, t) for t in range(q)) + ((0, 1),) + masks = [] + for a in product(range(q), repeat=4): + mask = 0 + for bit, (phi, v) in enumerate(product(lines, repeat=2)): + av = (add[mul[a[0]][v[0]]][mul[a[1]][v[1]]], + add[mul[a[2]][v[0]]][mul[a[3]][v[1]]]) + value = add[mul[phi[0]][av[0]]][mul[phi[1]][av[1]]] + if value == 0: + mask |= 1 << bit + masks.append(mask) + require(len(masks) == q ** 4, "coefficient matrix inventory") + return tuple(masks) + + +def direct_census(q, dim, masks): + require(0 <= dim <= MAX_DIM[q], "census capacity") + total = reachable = 0 + for entries in product(masks, repeat=dim): + common = (1 << ((q + 1) ** 2)) - 1 + for mask in entries: + common &= mask + reachable += common != 0 + total += 1 + require(total == q ** (4 * dim), "target enumeration count") + return total, reachable, total - reachable + + +def spaces(q, dim): + """Yield each subspace once by its unique reduced row-echelon basis.""" + require(0 <= dim <= 4, "subspace capacity") + for pivots in combinations(range(4), dim): + slots = tuple((i, j) for i, p in enumerate(pivots) + for j in range(p + 1, 4) if j not in pivots) + for values in product(range(q), repeat=len(slots)): + rows = [[int(j == p) for j in range(4)] for p in pivots] + for (i, j), value in zip(slots, values, strict=True): + rows[i][j] = value + yield tuple(tuple(row) for row in rows) + + +def avoids_rank_one(basis, q, add, mul, neg): + for coeffs in product(range(q), repeat=len(basis)): + if not any(coeffs): + continue + value = [0] * 4 + for c, row in zip(coeffs, basis, strict=True): + for j in range(4): + value[j] = add[value[j]][mul[c][row[j]]] + if determinant(value, add, mul, neg) == 0: + return False + return True + + +def subspace_census(q, add, mul, neg): + total, good = [], [] + for dim in range(5): + seen = accepted = 0 + for basis in spaces(q, dim): + accepted += avoids_rank_one(basis, q, add, mul, neg) + seen += 1 + total.append(seen) + good.append(accepted) + expected = [1, q * (q * q - 1), q * q * (q - 1) ** 2 // 2, 0, 0] + require(good == expected, "rank-one-free subspace formula") + require(total[1] == (q ** 4 - 1) // (q - 1), "projective point count") + require(total[2] == (q * q + 1) * (q * q + q + 1), "plane inventory") + return {"all_by_dimension": total, "rank_one_free_by_dimension": good} + + +def full_rank_tuples(z, q, rank): + result = 1 + for i in range(rank): + result *= z - q ** i + return result + + +def formula(q, dim): + z = q ** dim + terms = [full_rank_tuples(z, q, 4), + q * (q * q - 1) * full_rank_tuples(z, q, 3), + q * q * (q - 1) ** 2 // 2 * full_rank_tuples(z, q, 2)] + unreachable = sum(terms) + return z ** 4 - unreachable, unreachable + + +def irreducible_census(q, add, mul, neg): + count = 0 + for a in product(range(q), repeat=4): + has_eigenvalue = False + for t in range(q): + shifted = (add[a[0]][neg[t]], a[1], a[2], add[a[3]][neg[t]]) + has_eigenvalue |= determinant(shifted, add, mul, neg) == 0 + count += not has_eigenvalue + require(2 * count == (q * q - q) ** 2, "irreducible matrix census") + return count + + +def controls(data): + add, mul, _ = field(3) + masks = bilinear_masks(3, add, mul) + # Lexicographic indices of I and [[0,2],[1,0]] among the 81 matrices. + left, right = masks[28], masks[21] + require(left != 0 and right != 0 and left & right == 0, "shared chart control") + require(formula(3, 2)[1] == 864, "ternary two-coordinate control") + rejected_mutants = 0 + for mutant, reference in ( + (19 * full_rank_tuples(9, 3, 2), data["3"]["target_censuses"][2]["unreachable"]), + (18 * full_rank_tuples(27, 3, 2), data["3"]["target_censuses"][3]["unreachable"]), + (6 * full_rank_tuples(16, 2, 3) + 2 * full_rank_tuples(16, 2, 2), + data["2"]["target_censuses"][4]["unreachable"])): + try: + require(mutant == reference, "wrong plane coefficient or missing line term") + except ValueError: + rejected_mutants += 1 + require(rejected_mutants == 3, "count mutants must be rejected") + a4, m4, _ = field(4) + require(a4[1][1] == 0 and m4[2][2] == 3, "F4 is not Z/4Z") + rejected = 0 + for bad_q in (1, 6, 9): + try: + field(bad_q) + except ValueError: + rejected += 1 + require(rejected == 3, "field boundary rejection") + try: + direct_census(3, 4, masks) + except ValueError: + return {"groups": ["shared chart", "wrong plane coefficient", + "missing line term", "missing zero-subspace term", "F4 field arithmetic", + "unsupported fields", "census capacity"], + "rejected_count_mutants": rejected_mutants, + "rejected_field_inputs": rejected} + raise ValueError("census bound was not enforced") + + +def main(): + output = {"claim_type": "scoped counting proof with finite corroboration", + "fields": {}, "no_new_kappa": True} + for q in FIELDS: + add, mul, neg = field(q) + masks = bilinear_masks(q, add, mul) + data = subspace_census(q, add, mul, neg) + data["irreducible_matrices"] = irreducible_census(q, add, mul, neg) + data["target_censuses"] = [] + for dim in range(MAX_DIM[q] + 1): + total, reachable, unreachable = direct_census(q, dim, masks) + require((reachable, unreachable) == formula(q, dim), "target formula") + if q == 2: + z = 2 ** dim + require(reachable == 9*z**3 - 30*z*z + 42*z - 20, "binary overlap") + data["target_censuses"].append({"dim": dim, "total": total, + "reachable": reachable, + "unreachable": unreachable}) + output["fields"][str(q)] = data + output["controls"] = controls(output["fields"]) + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + output["sha256"] = {name: sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(output, sort_keys=True, indent=2)) + print("PASS_RADICAL_ALL_FIELD_COUNT") + + +if __name__ == "__main__": + main()