diff --git a/research/nearest-even-shear-history/README.md b/research/nearest-even-shear-history/README.md new file mode 100644 index 0000000000..ff19ef9ba2 --- /dev/null +++ b/research/nearest-even-shear-history/README.md @@ -0,0 +1,174 @@ +# Exact history for nearest-even rounded shears + +For a fixed rational matrix A, retain the integer source x and return +`z = R(y + A*x)`, where y is an arbitrary independent integer destination and +R rounds each whole sum to its nearest integer, breaking half ties toward the +even integer. The minimum fixed binary history needed to reconstruct every y +is exactly + +``` +tau(A) = max over integer x of #{i : (A*x)_i is a half integer}. +``` + +A half integer means an integer plus 1/2. For `A = B/2` with B integral, tau +is the maximum Hamming weight in the binary linear code `im(B mod 2)`. +Even rational and binary rank one can require arbitrarily many history bits. +This is a scoped mathematical proof with exact finite corroboration, with no +physical history circuit, completed native child or new kappa. + +## Contract and quantified result + +Let A have m rows and n columns, with m,n positive and finite. Its coefficients +are fixed rationals. The map is + +`F_A : Z^n x Z^m -> Z^n x Z^m, (x,y) -> (x,R(y+A*x))`. + +There is no overflow, saturation, variable grid or hidden transcript. The +decoder knows A and the retained source x. A history is an extra value from +one fixed finite alphabet, and may depend on both x and y. All additional +input-dependent metadata counts as history. The guarantee is worst case, +without an average-length or input-distribution assumption. + +For fixed x, write t(x) for its number of half-integer coordinates. Every +nonempty fiber over `(x,z)` has exactly `2^t(x)` elements. The smallest sufficient +history alphabet therefore has exactly `2^tau(A)` values. The smallest fixed +bit budget is tau(A), attained by the explicit decoder below. This is an +injective encoding statement, not a reversible machine on a full dirty +auxiliary state space. + +F_A itself is a bijection exactly when every reduced denominator of every +entry of A is odd. Thus an integral dyadic A needs no history, while every +nonintegral dyadic A loses some information on the full entrance grid. A common +absolute grid precision does not change this statement after rescaling to +integer units, with the same unrestricted source and destination contract. + +## Proof + +Fix a scalar offset a. Away from half integers there is a unique nearest +integer, so `R(y+a)=y+R(a)` for all integer y. This coordinate is a bijective +integer translation. + +If `a=k+1/2`, only even output integers z are possible. Each such z has exactly +the two preimages `y=z-k-1` and `y=z-k`. Their unrounded sums are z-1/2 and +z+1/2, which both round to the even integer z. No other integer y is within +distance 1/2. Destination coordinates are independent once x is retained. +Multiplying coordinate fiber sizes proves the exact `2^t(x)` statement. + +Let D be the least common multiple of all reduced entry denominators. Changing +x by D times an integer vector changes A*x by an integer vector, preserving +its half-integer positions. Thus tau(A) is attained on `(Z/DZ)^n`. A nonempty +fiber at a maximizing source has `2^tau(A)` elements, which fewer history +values cannot distinguish, by the pigeonhole principle. + +For the matching upper bound, enumerate the half-integer coordinates in row +order. At offset `k_i+1/2`, store the bit `b_i=y_i-(z_i-k_i-1)`. The decoder +returns `z_i-k_i-1+b_i`. At every other coordinate it returns +`z_i-R((A*x)_i)`. The retained source identifies the tie coordinates, so no +tie-location transcript is needed. Pack the t(x) bits in the low positions +of a tau(A)-bit history and pad the unused bits with zero. This reconstructs +every signed integer destination. + +For the bijectivity classification, a sum of rationals with odd denominators +still has odd reduced denominator and cannot be a half integer. Conversely, +choose a row whose least common denominator d is even, and write it as +`(b_1,...,b_n)/d`. Minimality of d gives `gcd(d,b_1,...,b_n)=1`. Bezout's +identity supplies an integer vector x with `sum b_j*x_j = d/2 mod d`. +That row then has a half-integer offset. Hence tau is zero exactly for +odd-denominator matrices. When tau is zero, every source fiber is a bijective +translation; otherwise F_A has a collision. + +Finally, if `A=B/2`, a coordinate is a half integer exactly when the corresponding +coordinate of `B*x mod 2` is one. Every binary source residue occurs, proving +the maximum-codeword-weight formula. + +## Sharp consequences + +For m copies of the single coefficient 1/2, x=1 makes every coordinate a tie. +The rational and binary ranks are both one, yet the fiber at the all-zero +output contains every `y in {-1,0}^m`. Exactly m history bits are necessary +and sufficient for every m>=1. + +Rank also fails to determine the answer with dimensions fixed. The matrices +`B0=[[1,0],[1,1],[0,1]]` and `B1=[[1,0],[0,1],[0,1]]` both have rational and +binary rank two. The image weights of B0 are zero or two; B1 attains weight +three. Thus `tau(B0/2)=2` and `tau(B1/2)=3`. + +## Reproduction and evidence + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/nearest-even-shear-history/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nearest-even-shear-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nearest-even-shear-history --check-source-history +``` + +Both VERIFY.json commands are timed by the package runner. One enables isolated +optimized execution. All semantic checks remain active without assertions. +The direct verifier prints a generated JSON receipt with the hashes of all five +package files and writes nothing into the checkout. The written proof establishes +the unbounded theorem; finite enumeration corroborates it. + +The independent literal oracle minimizes exact rational distance and breaks +ties by parity. The encoder instead uses an integer-division rounder. Destination +residues modulo two give a complete finite fiber oracle because +`R(v+2)=R(v)+2`. All source residues modulo the exact denominator are enumerated. + +CPython 3.12.15 checks 682 binary matrices, with 5,003 source cases and 37,294 +literal destination cases; 668 rational fixtures, with 12,891 source cases and +50,128 literal destination cases; 38,759 signed exact history round trips; and +13 malformed-input/history/image rejections. The binary domain contains every +matrix of each shape from 1-by-1 through 3-by-3. Rational fixtures include a +signed scalar menu, a complete mixed-denominator 2-by-2 menu and all 2-by-2 +quarter-integral matrices with numerators zero through three. Rational fixtures +may repeat equal reduced coefficients. Additional controls check signed half +ties, the eight-element rank-one fiber, and increment/whole-sum distinctions. + +The replay API caps matrices at eight rows and six columns and each periodic +corroboration at 4,096 source residues. All loops have finite fixture/dimension +bounds. There is no recursion. Python/Fraction allocation is a managed-runtime +deviation from fixed-memory rules; the live fiber Counter has at most 256 +entries. Every function is under 60 lines. Explicit invariant checks remain +enabled with optimization. Warnings-as-errors run in both registered commands; +no additional static analyzer is configured for this package. + +## Sources, scope and credit + +This contribution was produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. New work is Apache-2.0. + +Ali Romman's [PR #5838](https://github.com/CrocSwap/integer-mult-bounds/pull/5838), +head `a7fe04425abb083842686f29c54ca0fed6252d31`, distinguishes independently +adverse completed defects from an actual rounder with stronger correlations. +Its open question motivates this deterministic side result. Its error numbers +and source word are not replayed or newly claimed. SOURCES.json records the +exact README blob and SHA256 used as question context. + +ywz65's [PR #2555](https://github.com/CrocSwap/integer-mult-bounds/pull/2555) +already gives a scalar whole-sum tie collision and the distinct positive +increment-rounding translation contract. Its unchanged README is pinned as +historical provenance. Rounding's general information loss, the pigeonhole +principle, Bezout's identity and binary linear codes are standard facts. +The new result is the exact rational-shear fiber/history classification, +its attaining encoding and the maximum-codeword-weight specialization. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216882) +records the question. The original `joint-query-controller` card is explicitly +changed to this local arithmetic/cleanup theorem. Neither predecessor verifier +is imported. Source context is provenance, not a live computational dependency. + +No history lifetime, physical register count, instruction count or reversible +uncomputation cost is proved. Restricted reachable inputs, different tie rules, +round-the-increment updates, extra retained outputs or discarded sources change +the contract. No full P104 word, native recipe, rounded supplier, selected cold +replay, compiler, tapes, Lean, outer arithmetic or complete multiplication +theorem has been implemented or verified. The five selected assumptions remain. + +## Open next questions + +Can one actual completed P104 child retain and uncompute its required tie +history within its complete physical bill? The encoding alone does not supply +a zero-return native workspace. First freeze the actual rounding sites, +entrance lattice and returned fields of one child, derive its fibers, then +price a history lifecycle. The missing completed physical child and history +restoration machine block that step. Structured details are in TASK.json. diff --git a/research/nearest-even-shear-history/SOURCES.json b/research/nearest-even-shear-history/SOURCES.json new file mode 100644 index 0000000000..8d47d3e71b --- /dev/null +++ b/research/nearest-even-shear-history/SOURCES.json @@ -0,0 +1,33 @@ +{ + "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/dirty-prefix-full-grid/README.md", + "usage": "provenance", + "git_blob": "083fc7dc64ac554703d215f3de2923bd187bb81a", + "sha256": "409f8ab4d70d52fe1422f3a85c76482729535d6fe57bdf45a78e868a6ec45a00" + } + ], + "question_source": { + "pull_request": 5838, + "author": "Ali Romman", + "head": "a7fe04425abb083842686f29c54ca0fed6252d31", + "path": "research/p104-gauge-error-covariance/README.md", + "git_blob": "6e32f5c58c390d32fa2d72f1bf72fcdf2151d4d6", + "sha256": "0c621274810b65505f86f574efabf2568f8fca74a509af9129b55173451bdadd", + "usage": "Question and model context only; no executable or numerical result imported." + } +} diff --git a/research/nearest-even-shear-history/TASK.json b/research/nearest-even-shear-history/TASK.json new file mode 100644 index 0000000000..2f5a59c91a --- /dev/null +++ b/research/nearest-even-shear-history/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ], + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Prove the exact minimum fixed history for whole-sum nearest-even rational shears on arbitrary integer grids, including the half-integral binary-code formula.", + "scope_change_reason": "The card concerns a completed caller. PR5838 explicitly leaves deterministic rounding correlations open. This side result isolates the information that this concrete rounded primitive loses before any native/caller construction.", + "bottleneck_link": "An actual deterministic rounded child must preserve enough information for its required inverse/cleanup. A local relative-error bound does not certify injectivity. This is a necessary information contract, not an improved supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sharp history theorem and independently enumerated corroboration; do not extend into native or full-word construction.", + "outcome": "completed", + "evidence": "README.md contains the quantified proof and attaining encoding; verify.py enumerates complete small fibers and independently reconstructs signed inputs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual completed P104 child retain and uncompute the required tie history within its complete physical bill?", + "why_it_matters": "The information encoding alone does not implement a reversible native child or zero-return workspace.", + "first_step": "Freeze one physical child, its actual rounding sites, entrance lattice and retained output; derive its fibers before adding a history lifecycle.", + "blocked_by": "No physical completed child or history-restoration machine is supplied here." + } + ], + "question_source": { + "pull_request": 5838, + "author": "Ali Romman", + "head": "a7fe04425abb083842686f29c54ca0fed6252d31", + "path": "research/p104-gauge-error-covariance/README.md", + "git_blob": "6e32f5c58c390d32fa2d72f1bf72fcdf2151d4d6", + "sha256": "0c621274810b65505f86f574efabf2568f8fca74a509af9129b55173451bdadd", + "usage": "Question and model context only; no executable or numerical result imported." + }, + "overlap_coverage": { + "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "own_prs": 200, + "open_prs_initial": 100, + "helper_open_prs": 459, + "helper_discussion_records": 5402, + "helper_local_notes_searched": 200, + "helper_local_notes_omitted": 7645, + "limits": "Targeted merged/readme searches and live PR bodies are bounded; unpublished work, all diffs and all historical PRs are not exhaustively searched." + } +} diff --git a/research/nearest-even-shear-history/VERIFY.json b/research/nearest-even-shear-history/VERIFY.json new file mode 100644 index 0000000000..d96026ab3d --- /dev/null +++ b/research/nearest-even-shear-history/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete small rational/binary fibers, code-weight identity, signed history inverse and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact finite coverage with optimization, isolation and warnings as errors." + } + ] +} diff --git a/research/nearest-even-shear-history/verify.py b/research/nearest-even-shear-history/verify.py new file mode 100644 index 0000000000..310205947b --- /dev/null +++ b/research/nearest-even-shear-history/verify.py @@ -0,0 +1,222 @@ +"""Exact finite corroboration of the written nearest-even shear theorem.""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import product +from math import lcm +from pathlib import Path +import json +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows): + require(type(rows) is tuple and 1 <= len(rows) <= 8, "row bound") + require(all(type(row) is tuple for row in rows), "row type") + width = len(rows[0]) + require(1 <= width <= 6, "column bound") + require(all(len(row) == width for row in rows), "ragged matrix") + require(all(type(a) in (int, Fraction) for row in rows for a in row), + "exact rational entries required") + return tuple(tuple(Fraction(a) for a in row) for row in rows) + + +def vector(values, size): + require(type(values) is tuple and len(values) == size, "vector shape") + require(all(type(value) is int for value in values), "integer vector") + + +def nearest_even(a): + """Integer division, including negative arguments and exact half ties.""" + floor, remainder = divmod(a.numerator, a.denominator) + comparison = 2 * remainder - a.denominator + return floor + int(comparison > 0 or (comparison == 0 and floor % 2 == 1)) + + +def oracle_round(a): + """Independent distance minimization; even parity breaks equal distances.""" + floor = a.numerator // a.denominator + return min((floor, floor + 1), key=lambda z: (abs(a - z), z % 2)) + + +def offsets(a, x): + vector(x, len(a[0])) + return tuple(sum((c * v for c, v in zip(row, x)), Fraction()) for row in a) + + +def forward(a, x, y): + vector(y, len(a)) + return tuple(nearest_even(v + s) for v, s in zip(y, offsets(a, x))) + + +def encode(a, x, y): + z = forward(a, x, y) + history = 0 + used = 0 + for yi, zi, shift in zip(y, z, offsets(a, x)): + if shift.denominator == 2: + floor = shift.numerator // 2 + bit = yi - (zi - floor - 1) + require(bit in (0, 1) and zi % 2 == 0, "tie encoding invariant") + history |= bit << used + used += 1 + return z, history, used + + +def decode(a, x, z, history): + vector(z, len(a)) + shifts = offsets(a, x) + used = sum(s.denominator == 2 for s in shifts) + require(type(history) is int and 0 <= history < 2 ** used, "history range") + y = [] + cursor = 0 + for zi, shift in zip(z, shifts): + if shift.denominator == 2: + require(zi % 2 == 0, "unreachable odd tie output") + y.append(zi - shift.numerator // 2 - 1 + ((history >> cursor) & 1)) + cursor += 1 + else: + y.append(zi - nearest_even(shift)) + require(cursor == used, "history consumption") + return tuple(y) + + +def periodic_theorem(a): + denominator = lcm(*(c.denominator for row in a for c in row)) + cases = denominator ** len(a[0]) + require(cases <= 4096, "finite corroboration source bound") + maximum = 0 + source_cases = 0 + fiber_cases = 0 + for x in product(range(denominator), repeat=len(a[0])): + ties = sum(s.denominator == 2 for s in offsets(a, x)) + counts = Counter() + # Even modulus two preserves nearest-even parity and every whole fiber. + for y in product(range(2), repeat=len(a)): + literal = tuple(oracle_round(v + s) % 2 + for v, s in zip(y, offsets(a, x))) + counts[literal] += 1 + fiber_cases += 1 + require(set(counts.values()) == {2 ** ties}, "literal fiber size") + require(len(counts) == 2 ** (len(a) - ties), "literal image size") + maximum = max(maximum, ties) + source_cases += 1 + odd_rows = all(c.denominator % 2 == 1 for row in a for c in row) + require((maximum == 0) == odd_rows, "odd-denominator classification") + return maximum, source_cases, fiber_cases + + +def binary_census(): + totals = Counter() + for height in range(1, 4): + for width in range(1, 4): + for flat in product(range(2), repeat=height * width): + b = tuple(flat[i * width:(i + 1) * width] for i in range(height)) + a = matrix(tuple(tuple(Fraction(c, 2) for c in row) for row in b)) + maximum, sources, fibers = periodic_theorem(a) + code = {tuple(sum(c * v for c, v in zip(row, x)) % 2 for row in b) + for x in product(range(2), repeat=width)} + require(maximum == max(map(sum, code)), "binary code weight") + totals.update(matrices=1, source_cases=sources, fiber_cases=fibers) + return totals + + +def rational_census(): + totals = Counter() + for denominator in range(1, 13): + for numerator in range(-6, 7): + a = matrix(((Fraction(numerator, denominator),),)) + _, sources, fibers = periodic_theorem(a) + totals.update(matrices=1, source_cases=sources, fiber_cases=fibers) + menu = (Fraction(-1, 2), Fraction(1, 3), Fraction(1, 2), Fraction(2, 3)) + for flat in product(menu, repeat=4): + a = matrix((flat[:2], flat[2:])) + _, sources, fibers = periodic_theorem(a) + totals.update(matrices=1, source_cases=sources, fiber_cases=fibers) + for flat in product(range(4), repeat=4): + a = matrix(tuple(tuple(Fraction(c, 4) for c in flat[i:i + 2]) + for i in (0, 2))) + _, sources, fibers = periodic_theorem(a) + totals.update(matrices=1, source_cases=sources, fiber_cases=fibers) + return totals + + +def signed_roundtrips(): + fixtures = ( + ((Fraction(1, 2),),) * 3, + ((Fraction(1, 2), 0), (Fraction(1, 2), Fraction(1, 2)), (0, Fraction(1, 2))), + ((Fraction(1, 2), 0), (0, Fraction(1, 2)), (0, Fraction(1, 2))), + ((Fraction(-3, 4), Fraction(1, 3)), (Fraction(5, 6), Fraction(-1, 2))), + ((Fraction(1, 3), Fraction(-2, 5)),), + ) + checked = 0 + for rows in fixtures: + a = matrix(rows) + for x in product(range(-3, 4), repeat=len(a[0])): + for y in product(range(-3, 4), repeat=len(a)): + z, history, used = encode(a, x, y) + require(z == tuple(oracle_round(v + s) + for v, s in zip(y, offsets(a, x))), "round oracle") + require(used == sum(s.denominator == 2 for s in offsets(a, x)), + "exact history length") + require(decode(a, x, z, history) == y, "signed reconstruction") + checked += 1 + return checked + + +def rejection_controls(): + bad_matrices = ((), ((1,), (1, 2)), ((True,),), ((0.5,),), + ((0,),) * 9, ((0,) * 7,), ([1],)) + rejected = 0 + for rows in bad_matrices: + try: + matrix(rows) + except ValueError: + rejected += 1 + else: + raise ValueError("malformed matrix accepted") + a = matrix(((Fraction(1, 2),),)) + invalid = (((1,), (1,), 0), ((1,), (0,), 2), ((1,), (0,), -1), + ((1,), (0,), True), ((True,), (0,), 0), ((1,), (False,), 0)) + for x, z, history in invalid: + try: + decode(a, x, z, history) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid history/image accepted") + a = matrix(((Fraction(1, 2),),) * 3) + preimages = [y for y in product((-1, 0), repeat=3) if forward(a, (1,), y) == (0, 0, 0)] + require(len(preimages) == 8 and len(preimages) > 2 ** 2, "three-bit lower witness") + require(forward(a, (1,), (-1, -1, -1)) != (-1, -1, -1), "whole-sum control") + require(nearest_even(Fraction(-1, 2)) == nearest_even(Fraction(1, 2)) == 0, + "signed half ties") + return rejected + + +def main(): + binary = binary_census() + rational = rational_census() + roundtrips = signed_roundtrips() + rejected = rejection_controls() + triangle = matrix(((Fraction(1, 2), 0), + (Fraction(1, 2), Fraction(1, 2)), (0, Fraction(1, 2)))) + repeated = matrix(((Fraction(1, 2), 0), (0, Fraction(1, 2)), (0, Fraction(1, 2)))) + require(periodic_theorem(triangle)[0] == 2, "rank-two history two") + require(periodic_theorem(repeated)[0] == 3, "rank-two history three") + package = Path(__file__).resolve().parent + files = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in files} + receipt = dict(status="PASS_NEAREST_EVEN_SHEAR_HISTORY", python=platform.python_version(), + binary=dict(binary), rational=dict(rational), signed_roundtrips=roundtrips, + rejected_inputs=rejected, same_rank_history_bits=[2, 3], package_sha256=hashes) + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()