From 3edea13af13b755932852e9306a714b317630dda Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:01:43 +0100 Subject: [PATCH] feat(research): classify square-zero radical reachability --- .../README.md | 190 +++++++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 68 ++++++ .../VERIFY.json | 35 +++ .../verify.py | 230 ++++++++++++++++++ 5 files changed, 553 insertions(+) create mode 100644 research/square-zero-radical-reachability/README.md create mode 100644 research/square-zero-radical-reachability/SOURCES.json create mode 100644 research/square-zero-radical-reachability/TASK.json create mode 100644 research/square-zero-radical-reachability/VERIFY.json create mode 100644 research/square-zero-radical-reachability/verify.py diff --git a/research/square-zero-radical-reachability/README.md b/research/square-zero-radical-reachability/README.md new file mode 100644 index 0000000000..32456b6050 --- /dev/null +++ b/research/square-zero-radical-reachability/README.md @@ -0,0 +1,190 @@ +# Exact reachability of square-zero radical right-vector targets + +This contribution was produced by Nick Petalas. It answers the singular-target +question in [#4601](https://github.com/CrocSwap/integer-mult-bounds/pull/4601), +starting with its suggested algebra F₂[x,y]/(x,y)². The main result is a +**scoped proof**, with exact finite corroboration. No new κ is claimed. + +Let K be any field and R = K ⊕ J a unital K-algebra with K central and J² = 0. +The ideal J may have any dimension. A paid factor is I + u yᵀ with u ∈ R² +and y ∈ K². Arbitrary GL₂(K) maps are free anywhere in a word. Factors may +be singular. These are the formal alphabet and free-map convention of +Wentao Li's #4099 and Nick Petalas's #4243/#4276. + +For every radical target M ∈ M₂(J), the exact answer is + +```text +cost(M) = 2 if some nonzero φ ∈ (K²)* and v ∈ K² satisfy φ M v = 0; +cost(M) = ∞ otherwise. +``` + +In particular, a third or later factor never enlarges the reachable radical +set. This is a theorem for arbitrary finite words, not a bounded search failure. +It does not classify all singular targets outside M₂(J), nonsplit extensions, +higher nilpotency or more than two roles. + +For K = F₂ and finite d = dim J, write z = 2^d. The exact number of reachable +radical targets is + +```text +R_d = 9 z³ − 30 z² + 42 z − 20. +U_d = z⁴ − R_d. +``` + +The exact pairs (reachable, unreachable) for d = 0,1,2,3 are +(1,0), (16,0), (244,12), (3004,1092). The d = 2 value agrees numerically +with the 12 unreachable targets reported by #4276; it is a calibration point, +not new credit. The quantified criterion and counting law are the additions. + +## Proof of the criterion + +All products below use algebraic order; execution on column vectors is from +right to left. A bar denotes scalar residue modulo J. Every paid factor has +scalar residue of rank at least one, since it fixes the kernel of its +base-field right row. Consequently a radical target needs at least two paid +factors, even when M = 0. Free factors alone have invertible residue. + +**Necessity.** Read any realizing word in execution order, including its free +maps. Start at I. There is a first event where the accumulated scalar residue +becomes zero. The preceding product P has residue P₀ of rank one. The event +cannot be a free map. Write its paid factor as + +```text +Q = Q₀ + u₁ yᵀ, Q₀ = I + u₀ yᵀ, +P = P₀ + P₁, P₁ ∈ M₂(J), u₁ ∈ J × J. +``` + +Since Q₀ P₀ = 0 and neither residue is zero, Q₀ has rank one. +Choose a nonzero row φ annihilating Q₀. Choose a nonzero column v in the +kernel of the one-row matrix yᵀP₀. The square-zero relation gives + +```text +QP = Q₀P₁ + u₁ yᵀP₀, +φ(QP)v = 0. +``` + +Thus the first radical product has a common bilinear zero. Once the residue +is zero, later multiplication by Q₀ + Q₁ acts as Q₀ on that radical product, +because Q₁ times a radical matrix is zero. If Q₀ is invertible, transport φ +by Q₀⁻¹. If it is rank one, take φ to annihilate its image. A later free map +is the invertible case. This preserves the existence of a nonzero pair +(φ,v) at every remaining event, and proves necessity for the final M. + +**Sufficiency.** Given φMv = 0, choose G,H ∈ GL₂(K) with first row of G equal +to φ and second column of H equal to v. Then + +```text +N = GMH = [[a,0],[c,d]], +C₁ = [[a,0],[c,1]] = I + (a−1,c)ᵀ e₁ᵀ, +C₂ = [[1,0],[0,d]] = I + (0,d−1)ᵀ e₂ᵀ, +M = G⁻¹ C₁ C₂ H⁻¹. +``` + +Both C₁,C₂ are paid factors. This is the triangular construction behind +#4276's two-factor criterion. Together with the lower bound it gives cost +exactly two. The new necessity argument excludes every longer word when no +common zero exists. + +## Proof of the binary counting law + +Choose a basis of J and write M = Σ_j A_j ε_j, with A_j ∈ M₂(F₂). Use the +nondegenerate entrywise pairing on the four-dimensional matrix space. Let +W = span(A₁,...,A_d) and S = W-perpendicular. The common-zero criterion is +that S contains a nonzero rank-one tensor φᵀvᵀ, with entries φ_i v_j. +Thus M is unreachable exactly when every nonzero element of S is invertible. + +Such a subspace S has dimension at most two: evaluation T ↦ T e₁ is injective +on S and takes values in F₂². There is one zero subspace and six allowable +one-dimensional subspaces, generated by the six invertible 2×2 matrices. +There are exactly two allowable planes. To count them, normalize any nonzero +A ∈ S to I by left multiplication. The other generator B must have B and +I+B invertible, so its characteristic polynomial is x²+x+1. There are exactly +two such binary matrices: their diagonal entries differ and both off-diagonal +entries are one. Together with I they form the same normalized plane. +Therefore each invertible A determines one allowable plane, and each plane +is counted by its three nonzero elements, giving 6/3 = 2 planes. + +For a fixed S of dimension s, the ordered d coefficient matrices must span +the fixed (4−s)-space W. There are Π_{i=0}^{3−s}(2^d−2^i) such tuples, by +counting full-row-rank (4−s)-by-d binary matrices. The product is zero when +d < 4−s. Hence + +```text +U_d = (z−1)(z−2)(z−4)(z−8) + + 6(z−1)(z−2)(z−4) + 2(z−1)(z−2). +``` + +Expanding and subtracting from z⁴ proves the stated R_d. The rank-metric and +finite-vector-space counting tools are classical; their application to this +formal-alphabet reachability question is the scoped contribution. + +## Evidence and reproduction + +Run from the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/square-zero-radical-reachability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/square-zero-radical-reachability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/square-zero-radical-reachability +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/square-zero-radical-reachability --check-source-history +``` + +Another CPython 3.12 interpreter may replace the absolute local path. The +verifier writes nothing. It emits a generated SHA-256 receipt binding all +package files and declared inputs, then PASS_SQUARE_ZERO_RADICAL_REACHABILITY. +It compares the entire literal two-factor/free-endpoint image with the +criterion on all radical targets for d = 0,1,2,3, and reconstructs every +accepted target by the displayed word. The alphabet enumeration does not use +the criterion. It independently derives the count polynomial by +inclusion-exclusion over all 511 nonempty subsets of the nine rank-one +bilinear forms. It checks all first-zero transitions for d = 1, plus six +controls for obstruction, separate coefficient charts, reversed/dropped paid +factors, a changed count coefficient and the dimension bound. Checks remain +active under optimized Python. This finite evidence corroborates the written +proof; it is not proof-kernel verification of its quantifiers. + +## Limitations and implementation decisions + +The algebra must be split with residue exactly K, two roles and J² = 0. +Free maps and right vectors are common across all radical coordinates. Separate +charts for each coordinate would wrongly accept the irreducible-pencil control. +Every paid factor has its full formal price. Native preparation, routing, +precision, restoration, stock and a complete supplier bill are unknown. No +physical caller, admission, complete multiplication theorem or selected-frontier +change is supplied. Independent human and formal proof-kernel review are +unclaimed. No Lean, Docker or selected-construction replay was run. + +The verifier has fixed dimension at most three, at most 766 distinct paid +factors and at most 4096 radical targets. Functions remain below 60 lines. +Power-of-ten rule 3 has a bounded managed-runtime deviation: Python allocates +sets, tuples and integer objects during enumeration. Fixed loop domains bound +the stored matrix sets by 4096 entries; this offline standard-library checker +has no steady-state service or persistent resources. A future larger census +must specify fresh memory/runtime bounds instead of increasing MAX_DIM silently. +Warning-strict ordinary and optimized replays supply the available diagnostics; +no separate static analyzer is required by the package environment. + +## Open next questions + +1. Does the common-zero obstruction lift through a local algebra with J³ = 0, + and what additional second-order condition is needed? Start with + F₂[x,y]/(x,y)³ and the same residue-first-zero expansion. Products of radical + entries no longer vanish, so the present invariant alone does not suffice. +2. What is the exact finite-field counting law over F_q for q > 2? The criterion + already holds. Count subspaces of M₂(F_q) containing no rank-one matrix, + including the two-dimensional field-spread case, before any larger census. + +These follow-ups are not claimed or investigated here. Structured questions +and blockers are in TASK.json. + +## Credit and source boundary + +Produced by Nick Petalas. Nick Petalas's #4276 supplies the exact two-factor +criterion, its triangular factorization and the 12-target binary calibration; +#4243 supplies the free-map normal form. ToikY's #4334 develops the shared-chart +field-product interface. Nick Petalas's #4601 explicitly leaves singular +reachability open; its invertible-target theorem is not used as a lemma here. +Wentao Li's #4099 supplies the right-vector alphabet and column bound, building +on #2513. Exact unchanged main-source pins are in SOURCES.json. The original +connector-alphabet-change card is explicitly changed to this algebraic side +question, as in the predecessor right-vector packages. Apache-2.0. diff --git a/research/square-zero-radical-reachability/SOURCES.json b/research/square-zero-radical-reachability/SOURCES.json new file mode 100644 index 0000000000..034d625a64 --- /dev/null +++ b/research/square-zero-radical-reachability/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "input", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + }, + { + "path": "research/right-vector-two-factor-criterion/README.md", + "usage": "input", + "git_blob": "8952fc9ae8a6e1144e5a0008141121aee66aec69", + "sha256": "e00d4352a98b02c5046d8796ba4ef2afd3c6a78d66b4398d23794ebd8147580d" + } + ] +} diff --git a/research/square-zero-radical-reachability/TASK.json b/research/square-zero-radical-reachability/TASK.json new file mode 100644 index 0000000000..4124058aa3 --- /dev/null +++ b/research/square-zero-radical-reachability/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify all radical two-role right-vector targets over split square-zero K-algebras; prove exact cost 2 or unreachable and a closed binary count for every radical dimension.", + "scope_change_reason": "Take the explicit singular-target open question of PR4601 rather than extend the native connector alphabet. This is a formal-alphabet side result, not supplier admission.", + "bottleneck_link": "Separates reachable singular formal interfaces from targets no longer word can implement; native conversion and complete supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified common-zero criterion and its count; do not extend to higher nilpotency, more roles or a native implementation.", + "outcome": "completed", + "evidence": "README proof; complete literal two-factor images for radical dimensions 0..3; independent 511-subset counting polynomial; first-zero transition and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which additional obstruction appears when J cubed is zero but J squared is nonzero?", + "why_it_matters": "Decides whether longer words enlarge the radical image once first-order truncation fails.", + "first_step": "Expand the first zero residue event over F2[x,y]/(x,y)^3.", + "blocked_by": "Products of radical entries survive; no second-order invariant is supplied." + }, + { + "question": "What is the closed reachability count over every finite field Fq?", + "why_it_matters": "Turns the arbitrary-field criterion into an exact distribution beyond binary coefficients.", + "first_step": "Count rank-one-free subspaces of M2(Fq) and their ordered spanning tuples.", + "blocked_by": "The binary plane count does not classify all higher-field subspaces." + } + ] +} diff --git a/research/square-zero-radical-reachability/VERIFY.json b/research/square-zero-radical-reachability/VERIFY.json new file mode 100644 index 0000000000..5211cd6195 --- /dev/null +++ b/research/square-zero-radical-reachability/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-two-factor-criterion/PROOF.md", + "research/right-vector-two-factor-criterion/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact literal radical images, all-dimension binary count, first-zero transitions and rejecting controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all scientific checks with assertions disabled." + } + ] +} diff --git a/research/square-zero-radical-reachability/verify.py b/research/square-zero-radical-reachability/verify.py new file mode 100644 index 0000000000..9391b82c93 --- /dev/null +++ b/research/square-zero-radical-reachability/verify.py @@ -0,0 +1,230 @@ +"""Exact binary checks for the square-zero radical reachability theorem. + +Only the standard library is used. All scientific checks survive -O. +The literal alphabet enumeration does not use the common-zero criterion. +""" + +import hashlib +import itertools +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MAX_DIM = 3 +LINES = ((1, 0), (0, 1), (1, 1)) +FREE = tuple((a, b, c, d) for a, b, c, d in itertools.product(range(2), repeat=4) + if a * d ^ b * c) +IDENTITY = (1, 0, 0, 1) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ring_table(dim): + """Element bit 0 is scalar; remaining bits encode the square-zero ideal.""" + require(type(dim) is int and 0 <= dim <= MAX_DIM, "dimension outside bound") + size = 1 << (dim + 1) + return tuple(tuple(((b if a & 1 else 0) ^ (a if b & 1 else 0) + ^ (a & b & 1)) for b in range(size)) for a in range(size)) + + +def multiply(a, b, table): + return (table[a[0]][b[0]] ^ table[a[1]][b[2]], + table[a[0]][b[1]] ^ table[a[1]][b[3]], + table[a[2]][b[0]] ^ table[a[3]][b[2]], + table[a[2]][b[1]] ^ table[a[3]][b[3]]) + + +def residue(a): + return tuple(x & 1 for x in a) + + +def common_zero(a): + """Return a base-field row/column witness, or None.""" + for phi, v in itertools.product(LINES, repeat=2): + value = ((a[0] if phi[0] and v[0] else 0) + ^ (a[1] if phi[0] and v[1] else 0) + ^ (a[2] if phi[1] and v[0] else 0) + ^ (a[3] if phi[1] and v[1] else 0)) + if value == 0: + return phi, v + return None + + +def inverse(a): + require(a in FREE, "inverse requires a binary free map") + return (a[3], a[1], a[2], a[0]) + + +def triangular_word(a, witness, table): + """Return G^-1, C1, C2, H^-1 in algebraic product order.""" + phi, v = witness + g = next(g for g in FREE if g[:2] == phi) + h = next(h for h in FREE if (h[1], h[3]) == v) + n = multiply(multiply(g, a, table), h, table) + require(n[1] == 0, "common-zero chart") + c1 = (n[0], 0, n[2], 1) + c2 = (1, 0, 0, n[3]) + return inverse(g), c1, c2, inverse(h) + + +def product(word, table): + require(0 <= len(word) <= 4, "word outside replay bound") + acc = IDENTITY + for factor in word: + acc = multiply(acc, factor, table) + return acc + + +def paid_factors(size): + require(2 <= size <= 16 and size & (size - 1) == 0, "ring size bound") + return tuple(sorted({(1 ^ (a if y[0] else 0), a if y[1] else 0, + b if y[0] else 0, 1 ^ (b if y[1] else 0)) + for a, b in itertools.product(range(size), repeat=2) + for y in LINES})) + + +def literal_two_factor_radicals(table): + """Enumerate Q1 Q2 S without using any pivot or common-zero test.""" + factors = paid_factors(len(table)) + binary = ring_table(0) + groups = {} + for factor in factors: + groups.setdefault(residue(factor), []).append(factor) + targets = set() + pairs = 0 + for r1, r2 in itertools.product(groups, repeat=2): + if multiply(r1, r2, binary) != (0, 0, 0, 0): + continue + for q1, q2 in itertools.product(groups[r1], groups[r2]): + middle = multiply(q1, q2, table) + pairs += 1 + for free in FREE: + targets.add(multiply(middle, free, table)) + require(all(residue(a) == (0, 0, 0, 0) for a in targets), "radical filter") + return targets, pairs + + +def check_dimension(dim): + table = ring_table(dim) + literal, pairs = literal_two_factor_radicals(table) + criterion = set() + for a in itertools.product(range(0, len(table), 2), repeat=4): + witness = common_zero(a) + if witness is not None: + criterion.add(a) + require(product(triangular_word(a, witness, table), table) == a, + "attaining two-factor word") + require(literal == criterion, "literal alphabet and criterion disagree") + z = 1 << dim + check_formula(z, len(literal), (-20, 42, -30, 9, 0)) + return {"dimension": dim, "total": z ** 4, "reachable": len(literal), + "unreachable": z ** 4 - len(literal), "literal_pairs": pairs} + + +def check_formula(z, actual, coefficients): + require(len(coefficients) == 5 and 1 <= z <= 8, "polynomial bounds") + require(actual == sum(c * z ** i for i, c in enumerate(coefficients)), + "binary all-dimension counting law") + + +def binary_rank(vectors): + require(len(vectors) <= 9 and all(0 <= v < 16 for v in vectors), "rank bound") + pivots = [0] * 4 + for value in vectors: + for bit in range(3, -1, -1): + if value >> bit & 1: + if pivots[bit]: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return sum(bool(p) for p in pivots) + + +def check_counting_arrangement(): + """Independent inclusion-exclusion over nine rank-one bilinear forms.""" + tensors = tuple((phi[0] * v[0] | phi[0] * v[1] << 1 + | phi[1] * v[0] << 2 | phi[1] * v[1] << 3) + for phi, v in itertools.product(LINES, repeat=2)) + coefficients = [0] * 5 + for mask in range(1, 1 << 9): + vectors = tuple(tensors[i] for i in range(9) if mask >> i & 1) + coefficients[4 - binary_rank(vectors)] += (-1) ** (mask.bit_count() + 1) + require(coefficients == [-20, 42, -30, 9, 0], "arrangement polynomial") + return coefficients + + +def check_zero_transition(): + """Exhaust all first-zero transitions for dim J = 1.""" + table = ring_table(1) + rank_one = tuple(a for a in itertools.product(range(2), repeat=4) + if a != (0, 0, 0, 0) and a not in FREE) + checked = 0 + for p0 in rank_one: + for q in paid_factors(4): + if multiply(residue(q), p0, table) != (0, 0, 0, 0): + continue + for perturbation in itertools.product((0, 2), repeat=4): + p = tuple(a ^ b for a, b in zip(p0, perturbation)) + result = multiply(q, p, table) + require(common_zero(result) is not None, "first-zero invariant") + checked += 1 + return checked + + +def check_controls(dimensions): + table = ring_table(2) + obstruction = (2, 4, 4, 6) + require(common_zero(obstruction) is None, "irreducible pencil control") + coefficients = ((1, 0, 0, 1), (0, 1, 1, 1)) + require(all(common_zero(a) is not None for a in coefficients), + "componentwise charts would wrongly accept obstruction") + witness = (2, 0, 4, 6) + word = triangular_word(witness, common_zero(witness), table) + require(product((word[0], word[2], word[1], word[3]), table) != witness, + "reversed paid factors control") + require(product((word[0], word[1], word[3]), table) != witness, + "dropped paid factor control") + try: + check_formula(8, dimensions[3]["reachable"], (-19, 42, -30, 9, 0)) + except ValueError: + pass + else: + raise ValueError("changed polynomial constant was accepted") + try: + ring_table(MAX_DIM + 1) + except ValueError: + pass + else: + raise ValueError("dimension exhaustion was accepted") + return 6 + + +def receipt(results): + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + paths = [PACKAGE / name for name in names] + manifest = json.loads((PACKAGE / "VERIFY.json").read_text(encoding="utf-8")) + paths.extend(ROOT / name for name in manifest["inputs"]) + hashes = {str(path.relative_to(ROOT)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in paths} + return {"files": hashes, "results": results} + + +def main(): + dimensions = [check_dimension(d) for d in range(MAX_DIM + 1)] + results = {"dimensions": dimensions, + "arrangement": check_counting_arrangement(), + "first_zero_transitions": check_zero_transition(), + "controls": check_controls(dimensions)} + print(json.dumps(receipt(results), sort_keys=True)) + print("PASS_SQUARE_ZERO_RADICAL_REACHABILITY dimensions=0..3 " + "reachable=1,16,244,3004 unreachable=0,0,12,1092 no_new_kappa") + + +if __name__ == "__main__": + main()