diff --git a/research/split-determinant-radical-obstruction/README.md b/research/split-determinant-radical-obstruction/README.md new file mode 100644 index 0000000000..89dd725b86 --- /dev/null +++ b/research/split-determinant-radical-obstruction/README.md @@ -0,0 +1,207 @@ +# A split determinant does not imply radical reachability + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped algebraic proof with finite corroboration.** Over every +field K, let R=K[x,y,z]/(x,y,z)^2. On exactly three roles, allow paid factors +I+uv^T with u in R^3 and v in K^3, and arbitrary free GL_3(K) maps. Put + +```text +A = [[0,1,0], [0,0,1], [0,0,0]], +B = [[0,0,0], [1,0,0], [0,-1,0]], +M = xI_3+yA+zB. +``` + +Then M is unreachable at every finite paid length, although its homogeneous +determinant is the completely split polynomial + +```text +det(XI_3+YA+ZB) = X^3. +``` + +This answers the sufficiency question in Open next question 2 of +[PR #4776](https://github.com/CrocSwap/integer-mult-bounds/pull/4776) +negatively. Its two-generator determinant classification does not extend by +testing determinant splitting alone. A common left eigenrow is an additional +necessary condition. No new kappa, supplier admission or complete multiplication +theorem is claimed. + +## Proof + +### The common-row condition with several radical generators + +The first-zero scalar-prefix argument of +[PR #4773](https://github.com/CrocSwap/integer-mult-bounds/pull/4773) +extends to any finite number of independent square-zero generators. Here is +the extension needed for this example. + +Let R=K[t_0,...,t_s]/(t_0,...,t_s)^2 and let an endpoint on n roles be + +```text +M=t_0 I_n + sum_(j=1)^s t_j A_j. +``` + +If M is reachable in the same alphabet, the A_j have a common nonzero left +eigenrow over K, with a possibly different eigenvalue for each j. + +Conjugation by any G in GL_n(K) preserves the paid alphabet. Moving all free +maps to the right therefore writes an alleged word as M=F_L...F_1 G. The +scalar coefficient of its paid prefix eventually becomes zero. At the first +such step, let H be the preceding nonzero scalar prefix and write + +```text +F_k=I+(a+sum_j t_j b_j)v^T, T=I+av^T, TH=0. +``` + +A rank-one perturbation of I has nullity at most one. Thus T is singular, +v^T a=-1, H=a r^T for some nonzero row r^T, and v^T T=0. In particular +psi=v^T H=-r^T is nonzero. If C_j is the t_j coefficient before this step, +its new value is D_j=T C_j+b_j psi. Consequently + +```text +v^T D_j=alpha_j psi, alpha_j=v^T b_j, for every j=0,...,s. +``` + +After the scalar prefix becomes zero, later radical coefficients contribute +nothing because all products of radical generators vanish. Let S be the +product of the later scalar factors. The final coefficients are S D_j G. +The t_0 coefficient is I_n, so S and D_0 are invertible and alpha_0 is +nonzero. With w^T=v^T S^-1, a nonzero row, we have + +```text +w^T = v^T D_0 G = alpha_0 psi G, +w^T A_j = v^T D_j G = (alpha_j/alpha_0) w^T. +``` + +This proves the condition for arbitrary finite length and arbitrary free +base-field maps. It does not assert that a common eigenrow is sufficient. + +### The counterexample violates that condition + +For the displayed A, A^3=0. If w^T A=lambda w^T and w is nonzero, then +lambda^3=0, hence lambda=0 over a field. Writing w^T=(a,b,c) gives +w^T A=(0,a,b), so every left eigenrow is (0,0,c), with c nonzero. But + +```text +(0,0,c) B=(0,-c,0) +``` + +is not a multiple of (0,0,c), in any characteristic. The two matrices have no +common left eigenrow. The condition just proved excludes M at every length. + +The determinant calculation is over Z[X,Y,Z], so it survives passage to +every field, including characteristic two: + +```text +XI+YA+ZB = [[X,Y,0], [Z,X,Y], [0,-Z,X]], +det(XI+YA+ZB) = X(X^2+YZ)-YZX = X^3. +``` + +The determinant here is the homogeneous polynomial of the coefficient +matrices. The determinant of M inside R is zero and carries no such information. +The example therefore passes precisely the polynomial splitting condition +left open by #4776, while failing the new common-row test. + +## Evidence and reproduction + +The standalone verifier imports no predecessor executable. It performs an +integer polynomial determinant expansion, with all six permutations and all +27 coefficient choices per permutation. No numerical substitutions are used +to infer the identity. + +It enumerates every nonzero row and every possible scalar eigenvalue over +F2, F3, F5, F7 and F11. The nonzero-row counts are respectively +7, 26, 124, 342 and 1,330. In each field the A eigenrows are exactly the +nonzero multiples of the third coordinate row, the B eigenrows are exactly +the nonzero multiples of the first, and their intersection is empty. The +universal conclusion rests on the proof above, rather than this finite list. + +Two reachable controls delete zB or yA. Their literal three-factor +column-replacement words use increasing column order for A and decreasing +order for B. A separate paid-operation interpreter agrees with the target +matrix action on every one of the 4,096 vectors in R^3 over F2 for each +control, giving 8,192 action comparisons. No coordinate is assumed initially +zero. Reversed execution order and each single omitted factor change the +corresponding matrix endpoint. A sign control replaces -E32 by +E32 and +obtains X^3-2XYZ over Z. Ring controls check both mixed and repeated radical +products vanish. + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/split-determinant-radical-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/split-determinant-radical-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/split-determinant-radical-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/split-determinant-radical-obstruction --check-source-history +``` + +Another CPython 3.12 path can replace the local path. Expected scientific +marker: `PASS_SPLIT_DETERMINANT_RADICAL_OBSTRUCTION no_new_kappa`. +Each run generates a stdout receipt with SHA256 hashes of all five package +files and writes nothing. No receipt is hand-written or committed. + +## Scope and limitations + +The ring kills all products of radical generators. Right vectors and free +maps are over K, and there are exactly three physical roles in the example. +Restored auxiliary roles, ring-valued free maps and higher nilpotency are +outside scope. This is an all-length obstruction in the declared formal +alphabet, not a search failure or an exclusion of arbitrary native networks. +No source preparation, physical movement, precision, stock, restoration or +complete supplier invoice is supplied. Those costs remain unknown. +Independent human and formal proof-kernel review are unclaimed. Lean, Docker +and the selected scientific cold replay were not run. + +The code has no recursion, subprocesses, dynamic evaluation or variable search +sizes. Its matrices have three rows. Each field scan has at most 1,330 nonzero +rows and eleven eigenvalues. Each dirty-input loop has exactly 4,096 vectors. +The ring has sixteen elements, and no large table of vectors persists. Every +function is below sixty physical lines. Explicit exceptions keep checks active +under optimized Python; warnings are errors. CPython's managed allocation is +a deviation from fixed steady-state allocation, bounded by these fixed domains. +No external static analyzer or proof kernel is claimed. + +## Credit, provenance and coordination + +Nick Petalas's #4776 supplies the exact two-generator classification and the +explicit three-generator open question. Nick Petalas's #4773 supplies the +first-zero common-row argument extended here. His #4745 supplies the earlier +two-role square-zero context, and #4243 the free-map normal form. Wentao Li's +#4099 following #2513 supplies the right-vector alphabet; ToikY's #4334 +supplies the shared-chart context. These are cited predecessors, not audited +deliverables. No predecessor code or credit line is changed. No general +literature-priority claim is made for the underlying nilpotent matrix pair. +The contribution is its reachability obstruction answering the stated open +question and the common-row extension supporting that conclusion. + +The `formal-interface-lemma` card is explicitly changed to this algebraic +side question. It identifies information a determinant-only interface loses; +it does not discharge a selected assumption or expand a physical construction. +The current source-bound baseline passed after its omitted sparse inputs were +materialized. Its marker is `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`, which is +orientation rather than scientific replay. + +[SOURCES.json](SOURCES.json) pins the original card, selected record and +conceptual predecessor READMEs as provenance at canonical main +`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. There are +no external runtime inputs. Live open PRs, this account's earlier work, +recent handoff claims, active Discussions, local reservations, merged PR +searches and main README terms were inspected. The overlap helper had complete +remote pagination and incomplete sparse local-note coverage. That coverage +does not certify novelty. + +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213489). + +## Open next questions + +1. Is a full common invariant flag necessary for reachability of every + square-zero target with an invertible coefficient? The first-zero argument + yields only one eigenrow. Begin with a tuple having one common eigenrow + but an irreducible quotient; the missing step is a quotient argument that + preserves the paid alphabet and chronology. +2. Can a restored fourth role make this example reachable? Begin with + diag(M,1). Its nonzero scalar endpoint prevents the first-zero argument + used here, so a separate invariant or a literal attaining word is needed. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). +These follow-ups are not investigated here. diff --git a/research/split-determinant-radical-obstruction/SOURCES.json b/research/split-determinant-radical-obstruction/SOURCES.json new file mode 100644 index 0000000000..cc5e6be5a1 --- /dev/null +++ b/research/split-determinant-radical-obstruction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/multirole-radical-pencil/README.md", + "usage": "provenance", + "git_blob": "3e2e9b9ae2c8211b072f0078e0a762de87f465d3", + "sha256": "4f775b02c4f10c4b5394b8520e3837738fb695d255cba56b7639bd02bd1984a1" + }, + { + "path": "research/split-radical-pencil/README.md", + "usage": "provenance", + "git_blob": "c75b9d49627a47c6924ab64b7f4fb065cda7fa4b", + "sha256": "b419063a6de89a36b8ba552e580f73b0af2bbb2104c947db9f4a69f7728a79f2" + } + ] +} diff --git a/research/split-determinant-radical-obstruction/TASK.json b/research/split-determinant-radical-obstruction/TASK.json new file mode 100644 index 0000000000..0d3eb398f8 --- /dev/null +++ b/research/split-determinant-radical-obstruction/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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_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": "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": "Prove that a completely split homogeneous determinant is insufficient for three-generator square-zero radical reachability on three roles, over every field.", + "scope_change_reason": "The selected task is explicitly changed from proof-assistant interface validation to the algebraic open question 2 of PR4776. This is new mathematical work, not a predecessor audit or a claim to close a selected assumption.", + "bottleneck_link": "Algebraic side result: determinant-only screens can admit an unreachable formal helper map. A multi-coefficient common-row condition detects information that the split determinant loses. No physical supplier improvement is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved counterexample with a bounded standalone verifier, and package it without extending the family.", + "outcome": "negative-result", + "evidence": "README.md proves the all-field arbitrary-length obstruction; verify.py expands the determinant over Z, enumerates all eigenrows over five prime fields, and checks two literal reachable controls on 8192 dirty-input actions.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is a full common invariant flag necessary for every reachable square-zero radical target with an invertible coefficient?", + "why_it_matters": "It could give a stronger multi-generator reachability criterion than one common eigenrow.", + "first_step": "Choose a tuple with one common eigenrow and an irreducible quotient; attempt to pass a paid word to that quotient.", + "blocked_by": "A quotient argument preserving the base-field right-vector alphabet and chronology is missing." + }, + { + "question": "Can a restored fourth role make diag(xI_3+yA+zB,1) reachable for the displayed A and B?", + "why_it_matters": "It tests whether restored workspace escapes this exact obstruction.", + "first_step": "Analyze the nonzero scalar endpoint or construct a literal four-role word with the last role restored.", + "blocked_by": "The scalar prefix never has to become zero on all four roles, so the current proof does not apply." + } + ] +} diff --git a/research/split-determinant-radical-obstruction/VERIFY.json b/research/split-determinant-radical-obstruction/VERIFY.json new file mode 100644 index 0000000000..1c53670835 --- /dev/null +++ b/research/split-determinant-radical-obstruction/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": "Exact integer polynomial determinant, five prime-field complete eigenrow domains, two reachable controls on all 4096 binary dirty inputs each, chronology, omission, sign and radical-law controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with explicit exceptions active under optimized Python." + } + ] +} diff --git a/research/split-determinant-radical-obstruction/verify.py b/research/split-determinant-radical-obstruction/verify.py new file mode 100644 index 0000000000..9e02f63793 --- /dev/null +++ b/research/split-determinant-radical-obstruction/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Check the split-determinant counterexample and reachable controls. + +Produced by Nick Petalas. Apache-2.0. +The all-field, arbitrary-length proof is in README.md. No predecessor is run. +""" + +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +I = ((1, 0, 0), (0, 1, 0), (0, 0, 1)) +ZERO = ((0, 0, 0),) * 3 +A = ((0, 1, 0), (0, 0, 1), (0, 0, 0)) +B = ((0, 0, 0), (1, 0, 0), (0, -1, 0)) +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def matrix_product(left, right, q): + return tuple(tuple(sum(left[i][k] * right[k][j] for k in range(3)) % q + for j in range(3)) for i in range(3)) + + +def row_product(row, matrix, q): + return tuple(sum(row[i] * matrix[i][j] for i in range(3)) % q + for j in range(3)) + + +def determinant_polynomial(matrices): + """Expand det(X*M0+Y*M1+Z*M2) over Z, without substitutions.""" + need(len(matrices) == 3, "three coefficient matrices required") + result = {} + for perm in permutations(range(3)): + inversions = sum(perm[i] > perm[j] for i in range(3) + for j in range(i + 1, 3)) + for choices in product(range(3), repeat=3): + exponent = tuple(choices.count(i) for i in range(3)) + coefficient = (-1) ** inversions + for row in range(3): + coefficient *= matrices[choices[row]][row][perm[row]] + result[exponent] = result.get(exponent, 0) + coefficient + return {exponent: value for exponent, value in result.items() if value} + + +def check_obstruction(): + need(determinant_polynomial((I, A, B)) == {(3, 0, 0): 1}, + "new homogeneous determinant must equal X^3 over Z") + census = [] + for q in (2, 3, 5, 7, 11): + need(matrix_product(matrix_product(A, A, q), A, q) == ZERO, + "A must be nilpotent") + need(matrix_product(matrix_product(B, B, q), B, q) == ZERO, + "B must be nilpotent") + rows = 0 + a_rows = [] + b_rows = [] + for row in product(range(q), repeat=3): + if row == (0, 0, 0): + continue + rows += 1 + for scalar in range(q): + scaled = tuple(scalar * value % q for value in row) + if row_product(row, A, q) == scaled: + a_rows.append((row, scalar)) + if row_product(row, B, q) == scaled: + b_rows.append((row, scalar)) + need(set(a_rows) == {((0, 0, t), 0) for t in range(1, q)}, + "A eigenrows must be precisely the third coordinate line") + need(set(b_rows) == {((t, 0, 0), 0) for t in range(1, q)}, + "B eigenrows must be precisely the first coordinate line") + need(not ({row for row, _ in a_rows} & {row for row, _ in b_rows}), + "the new example must have no common left eigenrow") + census.append({"q": q, "nonzero_rows": rows, + "A_eigenpairs": len(a_rows), "B_eigenpairs": len(b_rows), + "common_eigenrows": 0}) + return census + + +def ring_add(left, right): + return tuple(a ^ b for a, b in zip(left, right, strict=True)) + + +def ring_product(left, right): + """Literal multiplication in F2[x,y,z]/(x,y,z)^2.""" + return (left[0] & right[0],) + tuple( + (left[0] & right[i]) ^ (left[i] & right[0]) for i in range(1, 4)) + + +def ring_matrix_product(left, right): + rows = [] + for i in range(3): + row = [] + for j in range(3): + value = (0, 0, 0, 0) + for k in range(3): + value = ring_add(value, ring_product(left[i][k], right[k][j])) + row.append(value) + rows.append(tuple(row)) + return tuple(rows) + + +def ring_identity(): + return tuple(tuple((int(i == j), 0, 0, 0) for j in range(3)) + for i in range(3)) + + +def target_matrix(coefficient, slot): + need(slot in (2, 3), "control uses the y or z generator") + return tuple(tuple((0, int(i == j), + coefficient[i][j] % 2 if slot == 2 else 0, + coefficient[i][j] % 2 if slot == 3 else 0) + for j in range(3)) for i in range(3)) + + +def replacement_factors(target, order): + """Return literal legal factors I+(target_column-e_j)e_j^T.""" + factors = [] + for column in order: + factor = tuple(tuple(target[i][j] if j == column else + (int(i == j), 0, 0, 0) for j in range(3)) + for i in range(3)) + factors.append((column, factor)) + return tuple(factors) + + +def matrix_action(matrix, vector): + image = [] + for row in matrix: + value = (0, 0, 0, 0) + for entry, coordinate in zip(row, vector, strict=True): + value = ring_add(value, ring_product(entry, coordinate)) + image.append(value) + return tuple(image) + + +def paid_action(column, factor, vector): + """Execute v += u*(e_j^T v) without matrix multiplication.""" + old = vector[column] + result = [] + for row in range(3): + delta = ring_add(factor[row][column], (int(row == column), 0, 0, 0)) + result.append(ring_add(vector[row], ring_product(delta, old))) + return tuple(result) + + +def check_reachable_controls(): + elements = tuple(product(range(2), repeat=4)) + comparisons = 0 + for coefficient, slot, order in ((A, 2, (0, 1, 2)), (B, 3, (2, 1, 0))): + target = target_matrix(coefficient, slot) + factors = replacement_factors(target, order) + accumulated = ring_identity() + for _, factor in factors: + accumulated = ring_matrix_product(factor, accumulated) + need(accumulated == target, "generator-deletion control must be reachable") + reversed_product = ring_identity() + for _, factor in reversed(factors): + reversed_product = ring_matrix_product(factor, reversed_product) + need(reversed_product != target, "chronology mutant must change the endpoint") + for omitted in range(3): + partial = ring_identity() + for index, (_, factor) in enumerate(factors): + if index != omitted: + partial = ring_matrix_product(factor, partial) + need(partial != target, "every paid factor is necessary in this word") + for vector in product(elements, repeat=3): + result = vector + for column, factor in factors: + result = paid_action(column, factor, result) + need(result == matrix_action(target, vector), "literal dirty-input action") + comparisons += 1 + return comparisons + + +def check_controls(): + plus_b = ((0, 0, 0), (1, 0, 0), (0, 1, 0)) + need(determinant_polynomial((I, A, plus_b)) == + {(3, 0, 0): 1, (1, 1, 1): -2}, "odd-characteristic sign control") + need(determinant_polynomial((I, A, ZERO)) == {(3, 0, 0): 1}, + "split determinant also occurs in a reachable control") + x, y = (0, 1, 0, 0), (0, 0, 1, 0) + need(ring_product(x, y) == (0, 0, 0, 0), "mixed radical products vanish") + need(ring_product(x, x) == (0, 0, 0, 0), "radical squares vanish") + + +def receipt(census, comparisons): + directory = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + path = directory / name + need(path.stat().st_size <= 131072, "package file capacity exceeded") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return {"claim_type": "scoped algebraic proof with finite corroboration", + "determinant_over_Z": "X^3", "fields": census, + "dirty_input_action_comparisons": comparisons, + "package_sha256": hashes} + + +def main(): + census = check_obstruction() + comparisons = check_reachable_controls() + check_controls() + print(json.dumps(receipt(census, comparisons), sort_keys=True)) + print("PASS_SPLIT_DETERMINANT_RADICAL_OBSTRUCTION no_new_kappa") + + +if __name__ == "__main__": + main()