diff --git a/research/masked-e8-copy-bill-perturbation/README.md b/research/masked-e8-copy-bill-perturbation/README.md new file mode 100644 index 0000000000..0ee217b6c5 --- /dev/null +++ b/research/masked-e8-copy-bill-perturbation/README.md @@ -0,0 +1,205 @@ +# Scalar perturbation costs at one 93-line E8 puncture + +This package proves that the coordinate completion in ToikY's +[PR #1609](https://github.com/CrocSwap/integer-mult-bounds/pull/1609) +has eight separate COPY ranks of nine for **every complex perturbation scalar**. +It also gives a bound for every fixed eight-term basis whose dual directions +are E8 roots. Its COPY bill can fall by at most one from its own all-pairs +comparator, and can fall only at `c = -2/3` or `c = 2/3`. + +The claim type is a scoped written proof supported by exact finite +certificates. The root-direction classification below is finite evidence used +in that proof. No best completion, all-pairs optimum, physical supplier, new +kappa or complete multiplication theorem is claimed. + +## Fixed object and accounting model + +Represent the 120 E8 root lines by doubled roots `q_i` of squared norm eight, +with first nonzero coordinate positive. Representatives are lexicographically +sorted. Let `r_i = q_i/2`, and fix + +```text +q_j = (2, 2, 0, 0, 0, 0, 0, 0) +v = (1,-1, 2, 0, 0, 0, 0, 0). +``` + +Delete the 27 lines satisfying `q_i dot q_j = 0` and `q_i dot v != 0`. +Call the 93 remaining lines `L`, and let `R` have their rows `r_i`. +This is exactly the puncture and normal of #1609. Its sharp arbitrary-deletion +threshold and neighborhood-span theorem are credited predecessor results; +this package does not rerun the E7-flat census or prove that threshold again. + +The required entries of `D T^T` are those of `2 R R^T` on the diagonal and +on orthogonal root pairs. The binary pairing matrix is + +`N_it = 1` if `(q_i dot q_t)/4` is even, and `0` otherwise. + +For term `k`, let `S_k = supp D_k`, `U_k = supp T_k`. Its price is +`rank_F2 N[S_k,U_k]`. The scalar COPY bill is the sum of those prices. +This is the separate-term model of DreamingOfClouds's #717. It does not +include gathering, restoration, frame changes, hosting or recursive costs. + +## The perturbation family + +Fix any invertible complex `8 x 8` matrix `A`, with columns `a_k`. +Write `b_k` for the columns of `A^{-T}`, so `a_l dot b_k = delta_lk`. +Use ordinary transpose throughout. Define + +```text +D_ik = r_i dot a_k +T_ik(0) = q_i dot b_k +T_jk(c) = (q_j + c v) dot b_k, +``` + +leaving all other rows of `T` unchanged. Then + +`D T(c)^T = 2 R R^T + c (R v) e_j^T`. + +Indeed, `A A^{-1} = I` gives the all-pairs identity at `c=0`, and the +changed row contributes `c R A A^{-1} v`. Every required entry in column +`j` has `r_i dot v = 0` by the deletion rule and `q_j dot v = 0`. +Thus every `c` gives masked exactness. For nonzero `c`, precisely 56 +unmasked entries change, all in column `j`. The verifier checks this +annihilation directly and counts the 56 nonzero products. This extends the +source's `c=1` example; it is not a new construction of the puncture. + +## Coordinate bill for every scalar + +Take `A=I`. The only changing row is + +`T_j(c) = (2+c, 2-c, 2c, 0, 0, 0, 0, 0)`. + +Its support changes only at `-2,0,2`. The verifier checks these three values +and `1` as a representative of their complement, with exact rational +arithmetic and two different binary-rank computations. + +| Scalar class | Nonzero coordinates of `T_j(c)`, numbered 1 to 8 | Eight COPY ranks | Total | +|---|---|---|---:| +| `c = -2` | 2, 3 | `9,9,9,9,9,9,9,9` | 72 | +| `c = 0` | 1, 2 | `9,9,9,9,9,9,9,9` | 72 | +| `c = 2` | 1, 3 | `9,9,9,9,9,9,9,9` | 72 | +| `c` outside `{-2,0,2}` | 1, 2, 3 | `9,9,9,9,9,9,9,9` | 72 | + +These are all support classes over the complex numbers, since each coordinate +is a linear polynomial with its stated single root, or is identically zero. +All other factor entries are constant. Therefore the four exact finite +checks prove COPY72 for every `c`, and the power bill is `8*9^p` for every +positive `p`. Varying only this scalar cannot improve the coordinate bill. + +## A column-deletion lemma + +Fix a source support `S` and a target support `U`. Changing membership of +one target `j` changes `rank N[S,U]` by at most one. Adding a target cannot +lower rank. A loss from the comparator at `c=0` therefore requires + +`q_j dot b_k != 0`, `v dot b_k != 0`, and +`c = -(q_j dot b_k)/(v dot b_k)`. + +Moreover, if column `j` of `N[all 120 lines,U]` is in the span of the other +columns, it remains in that span after restriction to any `S`. Deleting it +then costs zero rank on every `S`. Equality of the ranks with and without +`j` is precisely this column-dependence test. This argument needs no +hypothesis on `S` or on the field of the complex factor coefficients. + +## The root-direction certificate and its consequence + +For each of the 120 root directions `z`, set +`U(z) = {i in L : q_i dot z != 0}`. The verifier computes both ranks using +all 120 source rows, including the deleted ones. This larger row set makes +the column-dependence conclusion valid for every possible source support. +The complete 120-row certificate is printed in its JSON receipt. + +| Rank on `U(z)` | Rank on `U(z) \ {j}` | Root directions | +|---:|---:|---:| +| 8 | 8 | 27 | +| 9 | 8 | 3 | +| 9 | 9 | 90 | + +The three critical directions and their cancellation scalars are exactly + +| Direction `z` | `q_j dot z` | `v dot z` | Scalar cancelling the target coefficient | +|---|---:|---:|---| +| `(2,2,0,0,0,0,0,0)` | 8 | 0 | None | +| `(2,0,2,0,0,0,0,0)` | 4 | 6 | `-2/3` | +| `(0,2,-2,0,0,0,0,0)` | 4 | -6 | `2/3` | + +**Consequence.** Suppose each `b_k` is a nonzero complex multiple of an E8 +root. Let `C_A(c)` be the sum of the eight COPY ranks for the fixed `A`. +Then + +```text +C_A(c) >= C_A(0) if c is outside {-2/3, 2/3}, +C_A(c) >= C_A(0) - 1 for every complex c. +``` + +Proof: each of the 117 noncritical root supports either omits the target +or has a redundant target column for every `S_k`. A cancellation therefore +cannot reduce its price. New support can only increase a price. The critical target-root direction has zero +perturbation coefficient and cannot cancel. At each of the two remaining +scalars only its corresponding critical direction can lose rank, and that +loss is at most one. The dual vectors form a basis, so no two terms use the +same root direction. This proves both inequalities. + +This is a necessary bound, not attainment. A critical direction can still +have a redundant target column after restriction to its actual `S_k`, and +other terms can become more expensive. No lower bound for `C_A(0)` is +claimed, so these inequalities do not determine the best masked decoder. + +## Reproduce and verification limits + +From the repository root, using CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/masked-e8-copy-bill-perturbation/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/masked-e8-copy-bill-perturbation/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/masked-e8-copy-bill-perturbation +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/masked-e8-copy-bill-perturbation --check-source-history +``` + +The last command checks the committed package, so run it after committing. +The direct verifier emits a deterministic JSON receipt with all 120 direction +records and SHA256 hashes of its five package files, followed by +`PASS_MASKED_E8_COPY_BILL_PERTURBATION`. It writes nothing. All assertions +used for acceptance remain active under `-O`. + +The verifier also checks all 512 binary `3 x 3` matrices and their 1,536 +single-column deletions with both rank algorithms. It rejects three invalid +rank inputs, detects a diagonal error from perturbing by `q_j` instead of +`v`, and checks a restriction where a critical direction gives no saving. +The four coordinate representatives each check all 8,649 product entries. + +No other deletion set, non-root dual-direction classification, extra-term +completion, physical word, native admission, selected cold replay, Lean or +Docker run is supplied. Independent human and formal proof-kernel review +are unclaimed. The optional selected-baseline orientation command failed +locally because this sparse checkout omits +`research/global-lambda-lowering/LICENSE`; it is outside this package's +self-contained mathematical inputs. + +Implementation decisions: all loops range over fixed finite sets, at most +120 root lines, eight coordinates or 512 small matrices. Functions are below +60 lines. Python's managed runtime allocates dynamically, a deviation from +Power of Ten rule 3. Matrix dimensions and bit widths are bounded by these +constants, and the script has no solver, network or subprocess. If this is +extended to external inputs, enforce those capacities before allocation. + +## Open next questions + +Can the column-dependence test be characterized for every complex direction +`b`, rather than the 120 root directions? This would identify exactly where +the one-term rank-loss argument still permits scalar savings in a general +fixed basis. A feasible first step is to classify the hyperplane sections +`{i in L : q_i dot b = 0}` and test the target-column dependence of each +complement. The blocker is complete enumeration over complex directions; +a sampled list would establish only sampled coverage. This is a proposed +follow-up, not a result of this package. The structured question is in TASK.json. + +## Credit + +This contribution was produced by Nick Petalas. ToikY's #1609 supplies the +fixed puncture, normal, `c=1` witness and open scalar-variation question. +Philipp / mightyOil's #1191 supplies the local spanning mechanism. +DreamingOfClouds's #717 supplies the separate-term COPY model. The retained +E8 root/decoder lineage, including icekylinx, Joel Pulikkan / GamingPuzzled +and Douglas Colkitt, retains its predecessor credit. No predecessor executable +is imported or modified. New work is Apache-2.0. diff --git a/research/masked-e8-copy-bill-perturbation/SOURCES.json b/research/masked-e8-copy-bill-perturbation/SOURCES.json new file mode 100644 index 0000000000..2d816f50a9 --- /dev/null +++ b/research/masked-e8-copy-bill-perturbation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/masked-e8-puncture-threshold/README.md", + "usage": "provenance", + "git_blob": "e7f35d8fb1eb37461d92edb45c506b1a0d6875a7", + "sha256": "1829d3de39d3a37d06c069821057383f028596640e9d739ded3ce081e489ecc8" + } + ] +} diff --git a/research/masked-e8-copy-bill-perturbation/TASK.json b/research/masked-e8-copy-bill-perturbation/TASK.json new file mode 100644 index 0000000000..3ff9607d0a --- /dev/null +++ b/research/masked-e8-copy-bill-perturbation/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact scalar COPY bill and root-dual-basis perturbation bound at the single 93-line puncture of PR1609.", + "scope_change_reason": "The source open question isolates this scalar variation; this is a scoped side result rather than a complete signed supplier invoice.", + "bottleneck_link": "Tests whether the source mask-only identity can reduce its separately charged COPY ranks before physical construction; no complete supplier or kappa claim.", + "budget_minutes": 60, + "stop_rule": "Ship the exact scalar-support classification and root-direction rank-loss bound; do not search other punctures or optimize non-coordinate completions.", + "outcome": "completed", + "evidence": "verify.py reconstructs four coordinate support classes and all 120 root-direction deletion ranks with two binary-rank algorithms. README.md proves the consequences for every complex scalar.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Characterize target-column dependence for every complex dual direction at this fixed puncture.", + "why_it_matters": "This would extend the necessary scalar-saving test beyond root directions without assuming a physical implementation.", + "first_step": "Classify hyperplane sections of the 93 live roots, then compute the binary pairing rank with and without the target.", + "blocked_by": "Complete coverage of complex hyperplane sections; sampling does not establish it." + } + ], + "overlap": { + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "checked_at_utc": "2026-11-11T08:00:55.590867+00:00", + "open_prs": 466, + "discussion_records": 7089, + "remote_pagination_complete": true, + "local_notes_searched": 183, + "local_notes_at_head": 10178, + "limitations": "Sparse notes; keyword and README searches do not cover arbitrary diffs or unpublished work. Complementary claim 19530146 studies the broader first-failure census and non-coordinate constructions; neither is answered here.", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530120", + "progress": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19537521" + } +} diff --git a/research/masked-e8-copy-bill-perturbation/VERIFY.json b/research/masked-e8-copy-bill-perturbation/VERIFY.json new file mode 100644 index 0000000000..b7d20ec5c0 --- /dev/null +++ b/research/masked-e8-copy-bill-perturbation/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": "Four complete coordinate support classes, all 120 root-direction column-deletion certificates, two binary-rank algorithms, 512 small-matrix controls and wrong-normal rejection." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized replay retains all mathematical acceptance checks." + } + ] +} diff --git a/research/masked-e8-copy-bill-perturbation/verify.py b/research/masked-e8-copy-bill-perturbation/verify.py new file mode 100644 index 0000000000..aa058b0677 --- /dev/null +++ b/research/masked-e8-copy-bill-perturbation/verify.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +"""Exact scalar/support certificates for one fixed 93-line E8 puncture. + +Standard library only. No network, imports from other packages, or file writes. +The JSON receipt binds the result to the five package files. +""" + +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + +DIM = 8 +PORTS = 120 +TARGET = (2, 2, 0, 0, 0, 0, 0, 0) +NORMAL = (1, -1, 2, 0, 0, 0, 0, 0) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + need(len(left) == len(right) == DIM, "wrong vector dimension") + return sum(a * b for a, b in zip(left, right)) + + +def roots(): + """One sign representative of each root line, in lexicographic order.""" + vectors = [] + for i, j in itertools.combinations(range(DIM), 2): + for sign in (1, -1): + row = [0] * DIM + row[i], row[j] = 2, 2 * sign + vectors.append(tuple(row)) + for tail in itertools.product((1, -1), repeat=7): + row = (1,) + tail + if row.count(-1) % 2 == 0: + vectors.append(row) + lines = tuple(sorted(vectors)) + need(len(lines) == len(set(lines)) == PORTS, "wrong root-line inventory") + need(all(dot(q, q) == 8 for q in lines), "wrong doubled-root norm") + return lines + + +def binary_rank(rows, width=PORTS): + """Bounded bit Gaussian elimination; no arithmetic rank heuristic.""" + need(0 <= width <= PORTS and len(rows) <= PORTS, "rank capacity exceeded") + need(all(0 <= r < (1 << width) for r in rows), "invalid binary row") + pivots = [0] * width + result = 0 + for row in rows: + for bit in range(width - 1, -1, -1): + if row & (1 << bit): + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + result += 1 + break + return result + + +def column_rank(rows, width=PORTS): + """Independent transpose-and-XOR span computation.""" + need(len(rows) <= PORTS and 0 <= width <= PORTS, "rank capacity exceeded") + basis = [] + for col in range(width): + vector = sum(((r >> col) & 1) << i for i, r in enumerate(rows)) + for previous in basis: + vector = min(vector, vector ^ previous) + if vector: + basis.append(vector) + return len(basis) + + +def pairing(lines): + rows = [] + for left in lines: + products = [dot(left, right) for right in lines] + need(all(p % 4 == 0 for p in products), "nonintegral root product") + rows.append(sum(int((p // 4) % 2 == 0) << j for j, p in enumerate(products))) + need(binary_rank(rows) == column_rank(rows) == 9, "wrong full pairing rank") + return rows + + +def restricted_rank(mask_rows, sources, targets): + mask = sum(1 << j for j in targets) + rows = [mask_rows[i] & mask for i in sources] + result = binary_rank(rows) + need(result == column_rank(rows), "the binary rank implementations disagree") + return result + + +def puncture(lines): + target = lines.index(TARGET) + orthogonal = [i for i, q in enumerate(lines) if dot(q, TARGET) == 0] + deleted = [i for i in orthogonal if dot(lines[i], NORMAL) != 0] + live = [i for i in range(PORTS) if i not in deleted] + need(len(orthogonal) == 63 and len(deleted) == 27 and len(live) == 93, + "wrong fixed puncture") + neighbourhood = [i for i in live if i == target or dot(lines[i], TARGET) == 0] + need(all(dot(lines[i], NORMAL) == 0 for i in neighbourhood), "normal violates mask") + need(sum(dot(lines[i], NORMAL) != 0 for i in live) == 56, + "wrong nonzero error-column support") + return target, deleted, live + + +def coordinate_factors(lines, live, target, scalar, normal=NORMAL): + left = [[Fraction(x, 2) for x in lines[i]] for i in live] + right = [[Fraction(x) for x in lines[i]] for i in live] + position = live.index(target) + right[position] = [x + scalar * y for x, y in zip(right[position], normal)] + return left, right + + +def error_counts(lines, live, left, right): + masked = 0 + unmasked = 0 + columns = set() + for a, i in enumerate(live): + for b, j in enumerate(live): + actual = sum(x * y for x, y in zip(left[a], right[b])) + expected = Fraction(dot(lines[i], lines[j]), 2) + if actual != expected: + if i == j or dot(lines[i], lines[j]) == 0: + masked += 1 + else: + unmasked += 1 + columns.add(j) + return masked, unmasked, sorted(columns) + + +def coordinate_certificate(lines, mask_rows, live, target): + exceptional = sorted({Fraction(-a, b) for a, b in zip(TARGET, NORMAL) if b}) + need(exceptional == [Fraction(-2), Fraction(0), Fraction(2)], "wrong support breakpoints") + results = [] + patterns = set() + for scalar in (Fraction(-2), Fraction(0), Fraction(2), Fraction(1)): + left, right = coordinate_factors(lines, live, target, scalar) + pattern = tuple(k for k, value in enumerate(right[live.index(target)]) if value) + patterns.add(pattern) + ranks = [] + for k in range(DIM): + sources = [i for a, i in enumerate(live) if left[a][k]] + targets = [i for a, i in enumerate(live) if right[a][k]] + ranks.append(restricted_rank(mask_rows, sources, targets)) + need(ranks == [9] * DIM, "coordinate perturbation changed the COPY bill") + errors = error_counts(lines, live, left, right) + expected_errors = (0, 0, []) if scalar == 0 else (0, 56, [target]) + need(errors == expected_errors, "coordinate identity/error support failed") + results.append({"scalar": str(scalar), "target_support": list(pattern), + "ranks": ranks, "masked_errors": errors[0], + "unmasked_errors": errors[1]}) + need(len(patterns) == 4, "not every scalar support class was checked") + return results + + +def root_direction_certificate(lines, mask_rows, live, target): + histogram = Counter() + critical = [] + entries = [] + for direction in lines: + targets = [i for i in live if dot(lines[i], direction) != 0] + without = [i for i in targets if i != target] + full_rank = restricted_rank(mask_rows, range(PORTS), targets) + removed_rank = restricted_rank(mask_rows, range(PORTS), without) + need(0 <= full_rank - removed_rank <= 1, "one-column rank bound failed") + histogram[(full_rank, removed_rank)] += 1 + entry = {"direction": list(direction), "support_size": len(targets), + "rank": full_rank, "rank_without_target": removed_rank} + entries.append(entry) + if full_rank != removed_rank: + slope = dot(NORMAL, direction) + cancellation = str(Fraction(-dot(TARGET, direction), slope)) if slope else None + critical.append({**entry, "cancellation_scalar": cancellation}) + expected = {TARGET: None, (2, 0, 2, 0, 0, 0, 0, 0): "-2/3", + (0, 2, -2, 0, 0, 0, 0, 0): "2/3"} + actual = {tuple(row["direction"]): row["cancellation_scalar"] for row in critical} + need(actual == expected, "wrong critical root-direction classification") + need(histogram == {(8, 8): 27, (9, 8): 3, (9, 9): 90}, "wrong root-direction spectrum") + return {"spectrum": [{"ranks": list(k), "count": v} for k, v in sorted(histogram.items())], + "critical": critical, "directions": entries} + + +def controls(lines, mask_rows, live, target): + """Small exhaustive rank controls and wrong-perturbation rejection.""" + for encoded in range(1 << 9): + rows = [(encoded >> (3 * i)) & 7 for i in range(3)] + need(binary_rank(rows, 3) == column_rank(rows, 3), "3x3 rank control failed") + for removed in range(3): + shorter = [r & ~(1 << removed) for r in rows] + need(binary_rank(shorter, 3) == column_rank(shorter, 3), + "3x3 deletion rank implementations disagree") + need(0 <= binary_rank(rows, 3) - binary_rank(shorter, 3) <= 1, + "3x3 column-deletion control failed") + for rows, width in (([8], 3), ([0] * 121, 1), ([-1], 1)): + try: + binary_rank(rows, width) + except ValueError: + pass + else: + raise ValueError("invalid binary matrix accepted") + left, right = coordinate_factors(lines, live, target, Fraction(1), TARGET) + need(error_counts(lines, live, left, right)[0] > 0, "diagonal mutation was not rejected") + # Rank loss on all rows is not enough to promise loss after restriction. + exceptional = lines.index((2, 0, 2, 0, 0, 0, 0, 0)) + targets = [i for i in live if dot(lines[i], lines[exceptional])] + need(restricted_rank(mask_rows, [], targets) == + restricted_rank(mask_rows, [], [i for i in targets if i != target]) == 0, + "empty-row no-saving control failed") + return {"binary_matrices": 512, "column_deletions": 1536, + "invalid_inputs_rejected": 3, "wrong_normal_rejected": True, + "restriction_need_not_save": True} + + +def main(): + lines = roots() + mask_rows = pairing(lines) + target, deleted, live = puncture(lines) + coordinate = coordinate_certificate(lines, mask_rows, live, target) + directions = root_direction_certificate(lines, mask_rows, live, target) + checks = controls(lines, mask_rows, live, target) + package = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in names} + receipt = {"claim_type": "scoped proof supported by finite certificates", + "package_sha256": hashes, "target": list(TARGET), "normal": list(NORMAL), + "deleted_lines": [list(lines[i]) for i in deleted], "live_lines": len(live), + "coordinate": coordinate, "root_directions": directions, "controls": checks} + print(json.dumps(receipt, sort_keys=True, separators=(",", ":"))) + print("PASS_MASKED_E8_COPY_BILL_PERTURBATION coordinate=72 support_classes=4 " + "root_directions=120 critical=3 possible_saving_scalars=-2/3,2/3 max_root_basis_saving=1") + + +if __name__ == "__main__": + main()