diff --git a/research/multirole-radical-pencil/README.md b/research/multirole-radical-pencil/README.md new file mode 100644 index 0000000000..3e2e9b9ae2 --- /dev/null +++ b/research/multirole-radical-pencil/README.md @@ -0,0 +1,238 @@ +# A multi-role square-zero radical pencil obstruction + +**Scoped proof, with finite corroboration. No new kappa.** Over any field K, +let R = K[x,y]/(x,y)^2. Paid factors on n roles are I + u v^T, where u is +in R^n and v is in K^n. Arbitrary GL_n(K) maps are free and may occur anywhere. +If A in M_n(K) has no left eigenvector over K, then + +```text +M = xI + yA +``` + +is unreachable by any finite word. This is an arbitrary-length obstruction, +not a failed bounded search. Extra roles restored to the identity are outside +the statement. + +An explicit three-role instance over F2 is + +```text + [0 0 1] +A = [1 0 1], A^3 + A + I = 0. + [0 1 0] +``` + +The polynomial t^3+t+1 has no binary root. The verifier also enumerates all +512 binary three-by-three matrices and finds 48 with no binary left +eigenvector. Each of the corresponding 48 pencils is unreachable by the +theorem. This is not a count of every unreachable pencil. + +This package was produced by Nick Petalas. Apache-2.0. + +## What changes and predecessor credit + +[PR #4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745), exact +head `3edea13af13b755932852e9306a714b317630dda`, gives the complete two-role +square-zero radical criterion and introduces its first-zero scalar-prefix +argument. Its README limits that classification to two roles. This package +uses the same idea to obtain a necessary condition at arbitrary role count. +It does not audit or replay #4745 and does not assert a multi-role converse. + +The free-map normal form is from Nick Petalas's +[PR #4243](https://github.com/CrocSwap/integer-mult-bounds/pull/4243). +The right-vector alphabet and column bound are Wentao Li's +[PR #4099](https://github.com/CrocSwap/integer-mult-bounds/pull/4099), following +[PR #2513](https://github.com/CrocSwap/integer-mult-bounds/pull/2513). +ToikY's #4334 and Nick Petalas's #4276/#4601/#4749 are the related two-role +general-target and invertible-target successors. No predecessor code or +finite enumeration is imported. The proof below is self-contained. + +The `connector-alphabet-change` card is **changed** to an algebraic side +question in the existing alphabet. It is not a new legally priced connector. +The card's first working control passed with `pairings=945`, `queries=74`. +That control is orientation, not evidence for this theorem. + +## Proof + +Write a ring-valued matrix uniquely as P_0 + xP_x + yP_y, with all three +coefficient matrices over K. Products obey + +```text +(TP)_0 = T_0 P_0 +(TP)_x = T_0 P_x + T_x P_0 +(TP)_y = T_0 P_y + T_y P_0. +``` + +### Normalize free maps + +For G in GL_n(K), conjugation sends I+u v^T to +I+(Gu)(v^T G^-1), still a paid factor. Move every free map to the right. +An alleged word for M therefore has the form + +```text +M = F_L ... F_1 G = P G. +``` + +Consequently P_0=0, P_x=G^-1 and P_y=A G^-1. In particular P_x is invertible. + +### The first zero scalar prefix + +Let k be the first index at which the scalar part of F_k ... F_1 is zero. +It exists since P_0=0. Immediately before it the scalar prefix H is nonzero. +Write + +```text +F_k = I + (a + xb + yc) v^T, +T = I + a v^T. +``` + +Here TH=0. A rank-one perturbation of I has nullity at most one. Since +H is nonzero, T is singular, rank(H)=1, v^T a=-1, and v^T T=0. +The kernel of T is K a, so H=a r^T for a nonzero row r^T. Thus +psi = v^T H = -r^T is nonzero. + +Let C_x,C_y be the radical coefficient matrices before this step. Immediately +after the step they are + +```text +D_x = T C_x + b v^T H, +D_y = T C_y + c v^T H. +``` + +Multiplication by v^T kills the first summands, giving + +```text +v^T D_x = alpha psi, alpha = v^T b, +v^T D_y = beta psi, beta = v^T c. +``` + +This common-row identity is the essential restriction imposed by the +base-field right vector. No assumption on earlier radical coefficients was +made. + +### Later factors cannot remove the restriction + +After the first zero scalar prefix, the scalar prefix stays zero. Radical +parts of every later factor multiply a zero scalar prefix and contribute +nothing. If S is the product of their scalar parts, the final coefficients are + +```text +P_x = S D_x = G^-1, +P_y = S D_y = A G^-1. +``` + +Invertibility of P_x forces both S and D_x to be invertible. Hence alpha is +nonzero, because v^T is nonzero and v^T D_x cannot vanish. Put +w^T = v^T S^-1 and lambda = beta/alpha. Then w^T is nonzero and + +```text +w^T A G^-1 = w^T P_y + = v^T D_y + = lambda v^T D_x + = lambda w^T P_x + = lambda w^T G^-1. +``` + +Cancel G^-1 on the right. We obtain w^T A = lambda w^T, a left eigenvector +over K. Its absence excludes the alleged word, irrespective of its length. + +For the displayed binary A, a left eigenvalue would be 0 or 1. Multiplying +A^3+A+I=0 by its nonzero left eigenvector would give +(lambda^3+lambda+1)w^T=w^T=0. This contradiction proves the explicit instance. + +## Finite corroboration and controls + +The standard-library verifier executes the following bounded checks. They +corroborate the proof; they are not an enumeration of arbitrary-length words. + +- All 28 singular rank-two scalar factors on three binary roles and all + seven nonzero compatible scalar prefixes per factor give 196 pairs. + For each pair, the verifier checks all 512 preceding single-coefficient + matrices and all eight radical columns. The common-row identity holds in + all **802,816** cases. Exactly **150,528** have an invertible new coefficient; + each has a nonzero common-row multiplier. The identity is checked for one + arbitrary coefficient at a time, so it applies separately to x and y. +- Every one of the 512 possible A is tested against all seven nonzero binary + rows and both scalar eigenvalues. There are **48** eigenvalue-free matrices. + All 168 free conjugations of the displayed companion remain eigenvalue-free + and give **24** distinct conjugates. +- Three literal reachable controls are each executed on all 512 dirty ring + vectors, giving **1,536** chronological action comparisons. They are a rootful + upper-triangular pencil, the single-coefficient target yA, and the collapsed + target x(I+A) obtained if y is identified with x. The latter two show why an + invertible first coefficient and independent radical variables matter. +- Two exact chronology controls reject reversing the first-zero product and + omitting its radical contribution. The second error would miss a full-rank + coefficient produced at a singular scalar step. + +Every run prints a generated receipt bound to the SHA256 of all five package +files. No receipt is stored or hand-written. All checks use explicit exceptions +and remain active under `-O`. + +## Reproduction + +From the repository root, with CPython 3.12 and no third-party dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/multirole-radical-pencil/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/multirole-radical-pencil/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/multirole-radical-pencil +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/multirole-radical-pencil --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. Each +registered command has a 120-second timeout and takes less than one second +locally. Expected final marker: + +```text +PASS_MULTIROLE_RADICAL_PENCIL transitions=802816 full_rank=150528 excluded_pencils=48 no_new_kappa +``` + +## Limits and implementation bounds + +This is a necessary condition only. A scalar eigenvalue is not proved +sufficient. The ring has two independent radical generators with all their +products zero. Right vectors and free maps must be over K. Arbitrary +ring-valued free maps, higher radical nilpotency, and restored auxiliary roles +are outside scope. No native supplier, recursive cost, precision, stock or +complete multiplication theorem is supplied. Independent human and formal +proof-kernel review are unclaimed. No Lean, Docker or selected operator replay +was run. + +The code has no recursion, accepts no variable search sizes, and bounds every +loop by the displayed finite domains. Its largest table has 4,096 integers; +the receipt reads at most 128 KiB from each of five fixed paths. Python's +managed allocations depart from fixed steady-state allocation. Their domains +and lifetimes are bounded here. No shared code or interpreter configuration +changes are needed. + +## Open next questions + +1. Is a base-field eigenvalue sufficient when n>=3? Start with the direct sum + of a scalar block and the binary companion of t^2+t+1. The proof gives one + common row but no recursive criterion on its quotient. +2. Can an extra role restored to the identity make the displayed pencil + reachable? Start with diag(xI_3+yA,I_1). Its nonzero scalar endpoint is the + precise reason the present first-zero proof does not apply. + +The structured questions, relevance, first steps and blockers are also in +[TASK.json](TASK.json). These follow-ups are not investigated here. + +## Source and overlap scope + +The originating card and selected record are pinned at +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. The clean branch was created from +the refreshed canonical main `1f87c3578ae546c8f903f7f4d83dc2e2fb99650b`; the +guidance and selected record are unchanged between those commits. Open +predecessor #4745 is a credited conceptual source, not an imported executable +or a required unmerged Git object. The theorem and verifier are self-contained. + +Before claiming, live open PRs, this account's recent PRs, the latest handoffs, +active Discussions, local reservations, and distinctive merged/main +searches were checked. The overlap helper's cached remote pagination was +complete at approximately 19:22 UTC; its sparse local-note coverage was +incomplete and cannot certify novelty. The related two-role all-field count, +cube-zero example, rank-one-residue census and polynomial-ring cost claims +study different questions. The main two-role predecessor's twelve unreachable +radical targets are not rechecked or recounted here. + +Claim: [handoff post](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131197). diff --git a/research/multirole-radical-pencil/SOURCES.json b/research/multirole-radical-pencil/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/multirole-radical-pencil/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/multirole-radical-pencil/TASK.json b/research/multirole-radical-pencil/TASK.json new file mode 100644 index 0000000000..41ccf2808e --- /dev/null +++ b/research/multirole-radical-pencil/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": "For any field K and any role count, prove that xI+yA over K[x,y]/(x,y)^2 is unreachable at every finite paid length when A has no K-valued left eigenvector. Give the binary three-role cubic companion and exact finite corroboration.", + "scope_change_reason": "The card asks for a changed connector operation with a completed budget. This contribution instead extends the two-role square-zero question of PR4745 to a necessary condition at arbitrary role count in the same formal right-vector alphabet. It is a scoped algebraic side result, not a priced interface.", + "bottleneck_link": "A general-target rank estimate does not imply reachability in the base-field right-vector alphabet. The obstruction rejects a whole family before searching paid words; physical supplier costs are not inferred.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved multi-role obstruction and its bounded reproducer; leave sufficiency and restored auxiliary roles open.", + "outcome": "negative-result", + "evidence": "Written arbitrary-field and arbitrary-word-length proof; 802816 binary single-coefficient first-zero transition checks, including 150528 invertible cases; direct enumeration excludes 48 of 512 binary three-role pencils; 1536 chronological dirty-input comparisons and two chronology controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is a base-field eigenvalue sufficient for reachability of xI+yA when n>=3, or do nonsplit invariant factors still obstruct it?", + "why_it_matters": "The present theorem is a necessary condition only; a complete criterion could avoid unbounded word searches.", + "first_step": "Test the three-role direct sum of one scalar block and the companion of t^2+t+1 over F2.", + "blocked_by": "The first-zero step supplies one common row but does not recursively control its quotient." + }, + { + "question": "Can extra roles restored to the identity make an excluded radical pencil reachable?", + "why_it_matters": "Physical dirty auxiliary roles change the scalar endpoint from zero to a nonzero projector.", + "first_step": "Study diag(xI3+yA,I1) for the displayed cubic companion with the same restricted right vectors.", + "blocked_by": "The proof uses a zero full scalar endpoint and does not apply to this padding." + } + ] +} diff --git a/research/multirole-radical-pencil/VERIFY.json b/research/multirole-radical-pencil/VERIFY.json new file mode 100644 index 0000000000..12f6acef6d --- /dev/null +++ b/research/multirole-radical-pencil/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 802816 binary first-zero coefficient transitions, 48 excluded pencils, free conjugacy, literal dirty-input controls and chronology rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete finite corroboration with Python assertions disabled; all mathematical guards use explicit exceptions." + } + ] +} diff --git a/research/multirole-radical-pencil/verify.py b/research/multirole-radical-pencil/verify.py new file mode 100644 index 0000000000..5bf6f73465 --- /dev/null +++ b/research/multirole-radical-pencil/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the multi-role radical-pencil obstruction. + +Produced by Nick Petalas. Apache-2.0. +Only F2, three roles and two independent square-zero coefficients are executed. +The arbitrary-field, arbitrary-length argument is in README.md. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +N = 3 +SIDE = 1 << N +STATES = 1 << (N * N) +IDENTITY = sum(1 << (N * i + i) for i in range(N)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def row_times(vector, matrix): + result = 0 + for i in range(N): + if vector >> i & 1: + result ^= matrix >> (N * i) & (SIDE - 1) + return result + + +def column_times(matrix, vector): + return sum(((row_times(1 << i, matrix) & vector).bit_count() % 2) + << i for i in range(N)) + + +def multiply(left, right): + return sum(row_times(row_times(1 << i, left), right) << (N * i) + for i in range(N)) + + +def outer(column, row): + return sum(row << (N * i) for i in range(N) if column >> i & 1) + + +def rank(matrix): + basis = [0] * N + result = 0 + for i in range(N): + value = row_times(1 << i, matrix) + for pivot in range(N - 1, -1, -1): + if value >> pivot & 1: + if basis[pivot]: + value ^= basis[pivot] + else: + basis[pivot] = value + result += 1 + break + return result + + +def eigenpairs(matrix): + return [(v, scalar) for v in range(1, SIDE) for scalar in range(2) + if row_times(v, matrix) == scalar * v] + + +def ring_multiply(left, right): + """Matrix product over F2[x,y]/(x,y)^2, represented by three matrices.""" + a, x, y = left + b, u, v = right + return (multiply(a, b), multiply(a, u) ^ multiply(x, b), + multiply(a, v) ^ multiply(y, b)) + + +def action(matrix, vector): + """Act directly on three ring elements encoded as bits 1,x,y.""" + a, x, y = matrix + c, u, v = (sum(((entry >> bit) & 1) << i + for i, entry in enumerate(vector)) for bit in range(3)) + images = (column_times(a, c), + column_times(a, u) ^ column_times(x, c), + column_times(a, v) ^ column_times(y, c)) + return tuple(sum(((images[bit] >> i) & 1) << bit for bit in range(3)) + for i in range(N)) + + +def check_first_zero_transitions(): + """Check every single radical-coefficient instance of the first-zero step.""" + rows = tuple(tuple(row_times(v, m) for m in range(STATES)) + for v in range(SIDE)) + invertible = tuple(rank(m) == N for m in range(STATES)) + cases = 0 + full_rank = 0 + scalar_pairs = 0 + for u in range(1, SIDE): + for y in range(1, SIDE): + if (u & y).bit_count() % 2 != 1: + continue + scalar = IDENTITY ^ outer(u, y) + need(rank(scalar) == N - 1, "singular factor rank") + need(rows[y][scalar] == 0, "left kernel") + products = tuple(multiply(scalar, c) for c in range(STATES)) + for psi in range(1, SIDE): + previous = outer(u, psi) + need(rank(previous) == 1, "last nonzero scalar prefix rank") + need(multiply(scalar, previous) == 0, "first zero prefix") + need(rows[y][previous] == psi, "common row") + scalar_pairs += 1 + for c in range(STATES): + for ux in range(SIDE): + coefficient = products[c] ^ outer(ux, psi) + alpha = (y & ux).bit_count() % 2 + need(rows[y][coefficient] == alpha * psi, + "first-zero coefficient row identity") + cases += 1 + if invertible[coefficient]: + need(alpha == 1, "invertible coefficient has nonzero row") + full_rank += 1 + return scalar_pairs, cases, full_rank + + +def check_pencils(): + # Companion of t^3+t+1, with columns e2, e3, e1+e2. + companion = (0b100 << 0) | (0b101 << 3) | (0b010 << 6) + need(multiply(companion, multiply(companion, companion)) + ^ companion ^ IDENTITY == 0, "companion polynomial") + need(not eigenpairs(companion), "explicit pencil is obstructed") + excluded = [m for m in range(STATES) if not eigenpairs(m)] + need(len(excluded) == 48, "exhaustive eigenvalue-free matrix count") + free = [m for m in range(STATES) if rank(m) == N] + need(len(free) == 168, "GL3 size") + conjugates = set() + for g in free: + inverses = [h for h in free if multiply(g, h) == IDENTITY] + need(len(inverses) == 1, "unique free inverse") + h = inverses[0] + need(multiply(h, g) == IDENTITY, "two-sided free inverse") + conjugate = multiply(g, multiply(companion, h)) + need(not eigenpairs(conjugate), "free conjugacy preserves obstruction") + conjugates.add(conjugate) + need(len(conjugates) == 24, "companion conjugacy orbit") + return companion, len(excluded), len(conjugates) + + +def check_reachable_controls(companion): + # A rootful upper triangular pencil, attained by three legal column factors. + upper = (1 << 1) | (1 << 5) + word = (IDENTITY, 0, 0) + factors = [] + for i in range(N): + basis = 1 << i + column = sum(((upper >> (N * j + i)) & 1) << j for j in range(N)) + factor = (IDENTITY ^ outer(basis, basis), outer(basis, basis), + outer(column, basis)) + factors.append(factor) + word = ring_multiply(factor, word) + need(word == (0, IDENTITY, upper), "rootful pencil word") + need(bool(eigenpairs(upper)), "eigenvalue hypothesis is discriminating") + # The x coefficient cannot be dropped from the theorem's hypotheses. + y_identity = (IDENTITY, 0, 0) + x_identity = (IDENTITY, 0, 0) + x_factors, y_factors = [], [] + for i in range(N): + diagonal = outer(1 << i, 1 << i) + yf = (IDENTITY ^ diagonal, 0, diagonal) + xf = (IDENTITY ^ diagonal, diagonal, 0) + x_factors.append(xf) + y_factors.append(yf) + y_identity = ring_multiply(yf, y_identity) + x_identity = ring_multiply(xf, x_identity) + only_y = ring_multiply((companion, 0, 0), y_identity) + collapsed = ring_multiply((IDENTITY ^ companion, 0, 0), x_identity) + need(only_y == (0, 0, companion), "singular first coefficient control") + need(collapsed == (0, IDENTITY ^ companion, 0), "identified radicals control") + comparisons = 0 + for vector in product(range(8), repeat=N): + expected = tuple((((vector[i] & 1) << 1) + ^ ((((vector[i + 1] & 1) << 2) if i < N - 1 else 0))) + for i in range(N)) + need(execute(factors, vector) == expected, "independent dirty action") + constants = sum((entry & 1) << i for i, entry in enumerate(vector)) + only_y_expected = column_times(companion, constants) + collapsed_expected = column_times(IDENTITY ^ companion, constants) + need(execute(y_factors + [(companion, 0, 0)], vector) + == tuple(((only_y_expected >> i) & 1) << 2 for i in range(N)), + "singular-coefficient dirty action") + need(execute(x_factors + [(IDENTITY ^ companion, 0, 0)], vector) + == tuple(((collapsed_expected >> i) & 1) << 1 for i in range(N)), + "identified-radicals dirty action") + comparisons += 3 + return comparisons + + +def execute(factors, vector): + need(len(factors) <= 4, "bounded control word") + for factor in factors: + vector = action(factor, vector) + return vector + + +def check_chronology_controls(): + y = 1 + scalar = IDENTITY ^ outer(1, y) + psi = 1 + coefficient = multiply(scalar, IDENTITY) ^ outer(1, psi) + need(coefficient == IDENTITY, "radical term restores full coefficient rank") + need(rank(multiply(scalar, IDENTITY)) == 2, "omitted radical term rejected") + swap = outer(1, 2) ^ outer(2, 1) ^ outer(4, 4) + correct = multiply(scalar, swap) + reversed_order = multiply(swap, scalar) + need(row_times(y, correct) == 0, "correct chronological annihilator") + need(row_times(y, reversed_order) != 0, "reversed chronology rejected") + return 2 + + +def main(): + scalar_pairs, cases, full_rank = check_first_zero_transitions() + need((scalar_pairs, cases, full_rank) == (196, 802816, 150528), + "complete bounded transition census") + companion, excluded, conjugates = check_pencils() + dirty = check_reachable_controls(companion) + chronology = check_chronology_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + receipt = {"file_sha256": {name: file_hash(package / name) + for name in names}, + "scalar_pairs": scalar_pairs, "coefficient_cases": cases, + "invertible_cases": full_rank, "excluded_binary_pencils": excluded, + "companion_conjugates": conjugates, "dirty_action_checks": dirty, + "chronology_controls": chronology, "claim_type": "scoped proof"} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_MULTIROLE_RADICAL_PENCIL transitions=802816 full_rank=150528 " + "excluded_pencils=48 no_new_kappa") + + +def file_hash(path): + with path.open("rb") as stream: + data = stream.read(131073) + need(len(data) <= 131072, "package source exceeds receipt bound") + return sha256(data).hexdigest() + + +if __name__ == "__main__": + main()