diff --git a/research/rounded-half-shear-walsh/CODE-BOUNDS.md b/research/rounded-half-shear-walsh/CODE-BOUNDS.md new file mode 100644 index 0000000000..367f892ff8 --- /dev/null +++ b/research/rounded-half-shear-walsh/CODE-BOUNDS.md @@ -0,0 +1,38 @@ +# Executable bounds + +The verifier is read-only and uses Python 3.12's standard library. No source +module from another package is imported. Every mathematical acceptance check +uses an explicit exception and survives optimized execution. + +- There is no recursion, subprocess, network request, dynamic evaluation or + callback registration. The normal exit prints one generated JSON receipt; + any failed invariant raises an exception and fails the command. +- Every matrix has exactly four rows and columns. Every word has exactly + three stages. All products use fixed loops of length four or three. +- Each census has twelve orientations and exactly 65,536 inputs per + orientation. It streams the inputs and stores twelve ten-bin histograms, + twelve witnesses and one hash state. It does not retain the input corpus. +- The primary public evaluator checks exactly four integer inputs, with + absolute values below 2^128, and distinct integer indices in 0..3. Booleans + are rejected. Internal census calls have the stronger fixed domain 0..15. +- The independent interpreter is a fixed-corpus executable, not a public + arbitrary-matrix API. Its matrices are constructed locally from twelve + fixed index pairs. Its Fraction oracle has 256 inputs per pair. +- Receipt hashing reads exactly eight package files and one declared context + input, each guarded at one MiB. All filesystem read failures propagate. + The primary checks the context's pinned SHA256 before its census. +- All functions are below sixty physical lines. Warning-strict normal and + optimized runs, source compilation and AST inspection are the available + local diagnostics. No separate linter or type checker is configured here. + +Power of Ten rule 3 has a managed-runtime deviation in both Python files. +Python allocates integers, tuples, Fraction values and hash/JSON buffers +dynamically. The fixed matrix/corpus sizes, streaming census, input bit bound +and one-MiB receipt-input limits bound live state. These are certificate +programs, not fixed-allocation runtime kernels. A fixed-capacity rewrite is +required before deploying them in a setting that prohibits allocation. + +Python has no exposed raw-pointer dereference or compiler-preprocessing step +on these paths. Direct local function calls and shallow immutable matrix rows +are the corresponding inspected mechanisms. The only file writes are stdout +receipts; callers put them outside the checkout. diff --git a/research/rounded-half-shear-walsh/PROOF.md b/research/rounded-half-shear-walsh/PROOF.md new file mode 100644 index 0000000000..d174c96a41 --- /dev/null +++ b/research/rounded-half-shear-walsh/PROOF.md @@ -0,0 +1,144 @@ +# Sharp error for one rounded half-shear + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let R be componentwise nearest-integer rounding with ties to even. Coordinates +are numbered 0,1,2,3. Define + +```text +2A = [[1, 1, 0, 0], 2B = [[1, 0, 1, 0], + [1,-1, 0, 0], [0, 1, 0, 1], + [0, 0, 1, 1], [1, 0,-1, 0], + [0, 0, 1,-1]] [0, 1, 0,-1]]. +``` + +For any distinct t,s in {0,1,2,3}, put S=I+E_ts/2 and + +```text +y=R(Ax), z=R(Sy), F(x)=R(Bz), T=BSA, x in Z^4. +``` + +Then + +```text +max_(x in Z^4) ||F(x)-Tx||_infinity = 9/8. +``` + +The middle rounding is part of the program. The comparator contains the same +half-shear without rounding. On grid h Z^4, using R_h(v)=h R(v/h) at each +rounding, the sharp error is 9h/8 for every h>0. + +## Universal upper bound + +Write delta=y-Ax, epsilon=z-Sy and eta=F(x)-Bz. Each coordinate of delta and +eta is in {0,+1/2,-1/2}. Only epsilon_t can be nonzero, and it is in the +same three-element set. The endpoint error is exactly + +```text +F(x)-Tx = BS delta + B epsilon + eta. +``` + +Nearest-even rounding of a half-integer has the implication + +```text +delta_i != 0 implies y_i is even. +``` + +For any output whose B-pair does not contain t, the middle update is absent. +If eta_j=0, the error is at most 1/2. Otherwise that pair of stored integer +inputs has odd sum or difference. At least one input is odd, so its delta +is zero. The error is at most 1/4+1/2=3/4. + +For an affected output, put p=t xor 2. With the actual B-row signs +alpha,beta in {+1,-1}, the error is + +```text +(alpha delta_t + beta delta_p + alpha delta_s/2 + + alpha epsilon_t)/2 + eta_j. +``` + +This identity also covers s=p. Its repeated occurrence does not create an +independent error variable. + +If epsilon_t=0, the triangle bound is + +```text +(1/2 + 1/2 + 1/4)/2 + 1/2 = 9/8. +``` + +Suppose epsilon_t is nonzero. Since y_t,y_s are integers, y_s must be odd. +Consequently delta_s=0. The middle operation rounded a half-integer to even, +so z_t is even. If eta_j=0, the remaining error is at most +(1/2+1/2+1/2)/2=3/4. If eta_j is nonzero, z_t and z_p have opposite parity. +Thus z_p=y_p is odd, and delta_p=0. The error is at most +(1/2+1/2)/2+1/2=1. This proves the upper bound for every integer input, +without a search assumption. + +## Attainment + +The following explicit inputs attain the bound. The final column is one +coordinate of 8(F(x)-Tx). Every row is evaluated by both integer and dense +interpreters during the full residue checks. + +| t | s | x | output coordinate j | error times eight | +|---:|---:|---|---:|---:| +| 0 | 1 | (1,4,0,1) | 0 | -9 | +| 0 | 2 | (0,1,0,13) | 0 | -9 | +| 0 | 3 | (0,1,0,3) | 2 | -9 | +| 1 | 0 | (1,2,0,3) | 3 | 9 | +| 1 | 2 | (0,1,0,3) | 3 | 9 | +| 1 | 3 | (0,1,0,13) | 1 | 9 | +| 2 | 0 | (0,3,0,7) | 0 | 9 | +| 2 | 1 | (0,3,0,1) | 2 | 9 | +| 2 | 3 | (0,1,1,4) | 0 | -9 | +| 3 | 0 | (0,3,0,1) | 3 | -9 | +| 3 | 1 | (0,3,0,7) | 1 | -9 | +| 3 | 2 | (0,1,1,10) | 1 | 9 | + +For example, t=0,s=1,x=(1,4,0,1) gives +y=(2,-2,0,0), z=(1,-2,0,0), F(x)=(0,-1,0,-1), and +8Tx=(9,-8,5,-4). Hence the complete error times eight is (-9,0,-5,-4). +The middle rounding is exact in this extremizer. Its possible nonzero +error elsewhere still needs the preceding case analysis. + +## Complete finite reduction + +Nearest-even rounding commutes with every even integer translation. Replace +x by x+16v, for arbitrary v in Z^4. At the first stage the displacement +16Av is coordinatewise divisible by eight, so y shifts by exactly 16Av. +After S, the displacement is divisible by four, so z shifts by exactly +16SAv. After B, the displacement is even, so F shifts by exactly 16BSAv. +The linear comparator has that same displacement. Thus the entire error +vector is periodic modulo 16 in each input coordinate. + +Both verifiers enumerate all 12*16^4=786,432 pair/input cases. The primary +uses explicit butterflies and a closed signed half-rounding formula. The +separate interpreter multiplies three dense integer matrices and chooses +the nearer integer by two distances. It also compares 3,072 complete output +error vectors with Python Fraction rounding. The canonical stream of all +3,145,728 signed eighth-unit error coordinates is hashed in both checks. +This is a finite certificate, and the parity argument supplies an independent +all-input upper bound. Neither is a formal-kernel proof. + +Period eight is insufficient. For t=0,s=1, the inputs (0,0,0,2) and +(8,0,0,2) give error vectors times eight (-4,4,4,-4) and (4,4,-4,-4). +The integer-shear period must therefore not be reused silently here. + +## Scope and predecessors + +Josie Elliston's #6140 poses the interleaved-grid-shear question. Jerry Chen / +CubeJerry's #6146 proves the different exact-integer-shear law and supplies +the two-axis model and parity context. Nick Petalas's #6129 pure-stage law +is background. No predecessor theorem, scientific code or census is replayed +as this contribution. The upper bound and half-shear witnesses above are new +work for the stated program; nearest-even parity and translation facts are +elementary and carry no literature-priority claim. + +The theorem covers one positive half-shear, two distinct real Walsh axes, +exact arithmetic before each specified rounding and sufficient range. +Negative/other rational coefficients, complex gates, additional stages, +cross-fiber operations and a production compiler binding remain outside it. +There is no physical cost, reversible-history implementation, native supplier, +precision saving, kappa improvement or complete multiplication theorem. diff --git a/research/rounded-half-shear-walsh/README.md b/research/rounded-half-shear-walsh/README.md new file mode 100644 index 0000000000..e9bb4d6912 --- /dev/null +++ b/research/rounded-half-shear-walsh/README.md @@ -0,0 +1,111 @@ +# Sharp 9h/8 error for a rounded half-shear between Walsh axes + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with an exact finite certificate. For each +of the twelve directed pairs of four coordinates, the literal program + +```text +x in h Z^4 +y = R_h(Ax) +z = R_h((I + E_ts/2)y) +F(x) = R_h(Bz) +T = B (I + E_ts/2) A +``` + +has sharp error `max_x ||F(x)-Tx||_infinity = 9h/8`. Here A and B are the +two distinct normalized real Walsh axes defined in [PROOF.md](PROOF.md), +and every R_h rounds to nearest with ties to even. This determines an exact +value for a program outside the integer-shear law of +[CubeJerry #6146](https://github.com/CrocSwap/integer-mult-bounds/pull/6146). +The half-shear is rounded internally, so it adds a rounding site. + +The direct triangle bound is 11h/8. The parity proof improves it to 9h/8, +and twelve explicit integer inputs attain that value. A nonzero rounding +error at the middle shear forces its stored target to be even and its source +to be odd. Those parities remove earlier error terms at a final half-tie. +The complete error vector has input period 16h in each coordinate. An exact +counterexample shows that the integer-shear period 8h is insufficient here. + +This answers a nonintegral part of the intervening-shear question in +[Josie Elliston #6140](https://github.com/CrocSwap/integer-mult-bounds/pull/6140). +The previous integer result and pure-stage results are cited context, not +replay targets. No new kappa or selected-frontier change is claimed. + +## Evidence and reproduction + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-half-shear-walsh/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/independent.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-half-shear-walsh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-half-shear-walsh --check-source-history +``` + +Another CPython 3.12 path may replace the absolute interpreter. The direct +commands print `PASS_ROUNDED_HALF_SHEAR_WALSH` or +`PASS_INDEPENDENT_HALF_SHEAR_WALSH` inside generated JSON stdout evidence. +The primary receipt is bound to all eight package files and the one context +input. No receipt is hand-written or consumed as an acceptance premise. + +Each interpreter enumerates all 786,432 directed-pair/input cases and hashes +the complete stream of 3,145,728 signed eighth-unit errors. The primary uses +literal butterfly arithmetic. The independent implementation uses dense +integer matrices and another rounding algorithm, with 3,072 complete-vector +Fraction comparisons. Seven named semantic controls cover the insufficient +period, sharp endpoint, tie rule, omitted middle rounding, omitted shear, +reversed word and signed ties. Eight invalid primary inputs are rejected. +The primary also checks 515 signed half-rounds and 576 signed/large period +translations. The mathematical theorem rests on the written parity proof +and explicit attaining inputs, not an extrapolation of finite experiments. + +## Scope and provenance + +Base `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. The +selected #7000 record gives conditional kappa `363005817/100000000000`. +The source-binding positive control passed; it was not a scientific replay. +[TASK.json](TASK.json) records the changed `uniform-transfer-audit` scope. +[SOURCES.json](SOURCES.json) pins the catalogue, selected record and the +unchanged integer-shear context. The package imports no predecessor code. + +The theorem assumes exact pre-round arithmetic and sufficient range. It +does not cover another coefficient, complex mixing, extra stages or a +production caller. There is no finite-width implementation, reversible +history, physical coefficient service, storage/tape bill, compiler admission, +native supplier or complete multiplication theorem. All five selected +framework assumptions remain. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected scientific cold replay +are unrun. Executable bounds and the allocation deviation are recorded in +[CODE-BOUNDS.md](CODE-BOUNDS.md). + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572871) +preceded the new calculation. Live open/account PRs, recent handoffs, local +reservations, complete cached open/closed source-reference checks, all-main +README searches and merged keyword searches were checked. Those searches +do not cover unpublished work or arbitrary historical diffs. + +## Open next questions + +- Which other rational coefficients have a sharp error law when the shear + is rounded internally? Fix one coefficient and first derive its valid + even-translation period. The general parity and attainment arguments are + absent. No further coefficient is claimed here. +- Does an actual selected `precision_tape` caller contain this exact tile? + Extract one complete trace and match its grids, rounding sites and + comparator. Range, coefficient service, reversal, storage and the full + caller bill remain blockers to any precision change. + +## Credit + +Josie Elliston / JosieElliston #6140 supplies the interleaved-gate question. +Jerry Chen / CubeJerry #6146 supplies the integer-shear model, parity context +and its explicitly excluded coefficient domain. Nick Petalas #6129 supplies +the pure-stage background; its theorem is not used as the new proof step. +The deferred-row context belongs to Vlado Vojdanovski #1673, and the distinct +shear-equivariance context to Sricharan Vagvala #1631, retaining the native, +BIT and analytic lineage credited by those sources. Douglas Colkitt's package +scaffold and the repository publication checks are reused without edits. +The new half-shear theorem, attaining inputs and checkers were produced by +Nick Petalas. Predecessor files and credit lines are unchanged. diff --git a/research/rounded-half-shear-walsh/SOURCES.json b/research/rounded-half-shear-walsh/SOURCES.json new file mode 100644 index 0000000000..500508c451 --- /dev/null +++ b/research/rounded-half-shear-walsh/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/walsh-interleaved-shear/PROOF.md", + "usage": "input", + "git_blob": "c2b60aceb03d8a59e8e3d7cd71e51f70cc2a38da", + "sha256": "e16cb441209c6a093c2f21eeec96819b88a7f8a74bd7df103267ddf88c9f644a" + } + ] +} diff --git a/research/rounded-half-shear-walsh/TASK.json b/research/rounded-half-shear-walsh/TASK.json new file mode 100644 index 0000000000..2709c384e4 --- /dev/null +++ b/research/rounded-half-shear-walsh/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Sharp all-grid error 9h/8 for a rounded positive half-shear between two normalized real Walsh axes, for all twelve directed coordinate pairs.", + "scope_change_reason": "A precision_tape side result prompted by PR6140; the internal half-shear rounding is outside PR6146. This does not bind or discharge an actual selected caller.", + "bottleneck_link": "Exact local rounding constants and a valid residue period are needed before budgeting a changed rounded compiler; this is an interface side result without a selected caller or paid bill.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp half-shear error theorem and leave other coefficients and physical binding open.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal bound and twelve attaining inputs; verify.py and independent.py exhaust all 786432 pair/input residues, with the same complete-coordinate stream digest.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which other rational shear coefficients have a sharp two-stage error law when the shear is rounded internally?", + "why_it_matters": "A rational coefficient can add a rounding site and change the valid input period.", + "first_step": "Fix one coefficient and derive its exact even-translation period before enumerating residues.", + "blocked_by": "No all-coefficient parity or attainment argument is supplied." + }, + { + "question": "Does an actual selected precision_tape caller contain the stated rounded half-shear tile?", + "why_it_matters": "A local sharp constant changes production precision only after the actual trace and range contract are matched.", + "first_step": "Extract one complete emitted local trace and compare the grids, intermediate rounding sites and exact comparator.", + "blocked_by": "Physical coefficient service, range, storage, reversal and complete caller costs remain unpriced." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572871", + "playbook": "Autonomous local run", + "selected_baseline": { + "source_pr": 7000, + "kappa": "363005817/100000000000", + "check": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + }, + "overlap": { + "checked_at": "2026-11-12T19:20:20Z", + "source_question": "PR #6140 by JosieElliston", + "main_predecessor": "PR #6146 by CubeJerry", + "source_spread": "Neither source is held by another active batch lock; no recent account PR body refers to either source in the complete cached open/closed corpus.", + "coverage": "768 open PRs and 6175 closed PRs paginated completely in the source-overlap cache; recent handoff comments, active discussion headers, all-main README terms and merged keyword searches checked. Unpublished work and arbitrary historical diffs are not covered." + }, + "claim_type": "scoped proof with exhaustive finite corroboration" +} diff --git a/research/rounded-half-shear-walsh/VERIFY.json b/research/rounded-half-shear-walsh/VERIFY.json new file mode 100644 index 0000000000..c940d64e7a --- /dev/null +++ b/research/rounded-half-shear-walsh/VERIFY.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/walsh-interleaved-shear/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Complete exact residue census, sharpness and signed rounding/semantic controls; generated stdout evidence only." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Complete exact residue census, sharpness and signed rounding/semantic controls; generated stdout evidence only." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 240, + "checks": "Complete exact residue census, sharpness and signed rounding/semantic controls; generated stdout evidence only." + } + ] +} diff --git a/research/rounded-half-shear-walsh/independent.py b/research/rounded-half-shear-walsh/independent.py new file mode 100644 index 0000000000..1e8adffa5f --- /dev/null +++ b/research/rounded-half-shear-walsh/independent.py @@ -0,0 +1,118 @@ +#!/usr/bin/env python3 +"""Independent dense integer/Fraction interpreter; no primary imports.""" + +import hashlib +import itertools +import json +from fractions import Fraction +import struct + + +def check(condition, message): + if not condition: + raise ArithmeticError(message) + + +def matvec(matrix, vector): + return tuple(sum(row[j] * vector[j] for j in range(4)) for row in matrix) + + +def rounded_ratio(n, denominator): + # Select the closer of two consecutive integers. + low = n // denominator + left = n - denominator * low + right = denominator - left + if left < right: + return low + if left > right: + return low + 1 + return low if low % 2 == 0 else low + 1 + + +def matrices(target, source): + a2 = ((1, 1, 0, 0), (1, -1, 0, 0), + (0, 0, 1, 1), (0, 0, 1, -1)) + b2 = ((1, 0, 1, 0), (0, 1, 0, 1), + (1, 0, -1, 0), (0, 1, 0, -1)) + s2 = tuple(tuple(2 * (i == j) + (i == target and j == source) + for j in range(4)) for i in range(4)) + return a2, s2, b2 + + +def dense(x, gates): + state = x + ideal = x + for gate in gates: + state = tuple(rounded_ratio(v, 2) for v in matvec(gate, state)) + ideal = matvec(gate, ideal) + return tuple(8 * state[j] - ideal[j] for j in range(4)) + + +def fractional(x, gates, omit_middle_round=False): + state = tuple(Fraction(v) for v in x) + ideal = state + for step, gate in enumerate(gates): + state = tuple(v / 2 for v in matvec(gate, state)) + if not (step == 1 and omit_middle_round): + state = tuple(Fraction(round(v)) for v in state) + ideal = tuple(v / 2 for v in matvec(gate, ideal)) + result = tuple(8 * (state[j] - ideal[j]) for j in range(4)) + check(all(v.denominator == 1 for v in result), "eighth-unit error") + return tuple(int(v) for v in result) + + +def run(): + digest = hashlib.sha256() + count = 0 + rows = [] + oracle_checks = 0 + for target in range(4): + for source in range(4): + if target == source: + continue + gates = matrices(target, source) + histogram = [0] * 10 + for x in itertools.product(range(16), repeat=4): + error = dense(x, gates) + maximum = max(map(abs, error)) + check(maximum <= 9, "dense upper bound") + histogram[maximum] += 1 + digest.update(struct.pack("4b", *error)) + count += 1 + check(histogram[9] > 0, "dense sharpness") + rows.append([target, source, histogram]) + for x in itertools.product((-3, -1, 0, 2), repeat=4): + check(dense(x, gates) == fractional(x, gates), + "complete-vector Fraction oracle") + oracle_checks += 1 + check(count == 12 * 16**4, "dense coverage") + return {"status": "PASS_INDEPENDENT_HALF_SHEAR_WALSH", "cases": count, + "rows": rows, "fraction_oracle_cases": oracle_checks, + "error_stream_sha256": digest.hexdigest()} + + +def semantic_controls(): + gates = matrices(0, 1) + x = (1, -1, 1, 1) + check(fractional(x, gates) != fractional(x, gates, True), + "omitting the internal rounding changes the program") + x = (1, 4, 0, 1) + correct = fractional(x, gates) + identity2 = tuple(tuple(2 * (i == j) for j in range(4)) for i in range(4)) + omitted = fractional(x, (gates[0], identity2, gates[2])) + check(correct != omitted, "omitting the shear changes the comparison") + check(correct != fractional(x, tuple(reversed(gates))), + "reversing the word changes the endpoint") + check(rounded_ratio(-1, 2) == 0 and rounded_ratio(-3, 2) == -2, + "signed tie control") + return 4 + + +def main(): + report = run() + report["semantic_controls"] = semantic_controls() + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/rounded-half-shear-walsh/verify.py b/research/rounded-half-shear-walsh/verify.py new file mode 100644 index 0000000000..5c1bb2faee --- /dev/null +++ b/research/rounded-half-shear-walsh/verify.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +"""Exact four-coordinate rounded half-shear certificate. Read-only, stdlib.""" + +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path +import struct + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def half_round(n): + """Nearest-even rounding of n/2, including negative n.""" + return n // 2 + (n % 4 == 3) + + +def evaluate(x, target, source): + require(type(target) is int and type(source) is int, "integer indices") + require(0 <= target < 4 and 0 <= source < 4 and target != source, + "distinct indices in 0..3") + require(len(x) == 4, "four coordinates") + require(all(type(v) is int and abs(v) < 2**128 for v in x), + "integer coordinates of fewer than 129 signed bits") + return evaluate_core(x, target, source) + + +def evaluate_core(x, target, source): + # Both butterfly inputs are read before either output is stored. + a, b, c, d = x + y = (half_round(a + b), half_round(a - b), + half_round(c + d), half_round(c - d)) + z = list(y) + z[target] = half_round(2 * y[target] + y[source]) + output = (half_round(z[0] + z[2]), half_round(z[1] + z[3]), + half_round(z[0] - z[2]), half_round(z[1] - z[3])) + # u is four times S A x. The source is unchanged by the shear. + u = [2 * (a + b), 2 * (a - b), 2 * (c + d), 2 * (c - d)] + u[target] += u[source] // 2 + ideal8 = (u[0] + u[2], u[1] + u[3], u[0] - u[2], u[1] - u[3]) + error8 = tuple(8 * output[j] - ideal8[j] for j in range(4)) + return y, tuple(z), output, ideal8, error8 + + +def census(): + digest = hashlib.sha256() + rows = [] + total = 0 + for target in range(4): + for source in range(4): + if target == source: + continue + counts = [0] * 10 + witness = None + for x in itertools.product(range(16), repeat=4): + error = evaluate_core(x, target, source)[4] + peak = max(abs(v) for v in error) + require(peak <= 9, "universal residue upper bound") + counts[peak] += 1 + digest.update(struct.pack("4b", *error)) + if peak == 9 and witness is None: + witness = list(x) + total += 1 + require(counts[9] > 0, "each orientation attains 9/8") + require(sum(counts) == 16**4, "complete residue domain") + rows.append({"target": target, "source": source, + "max_error8": 9, "peak_histogram": counts, + "first_witness": witness}) + require(total == 12 * 16**4, "complete directed-pair domain") + return {"cases": total, "coordinates": 4 * total, "rows": rows, + "error_stream_sha256": digest.hexdigest()} + + +def controls(): + for n in range(-257, 258): + require(half_round(n) == round(Fraction(n, 2)), "signed nearest-even") + period_checks = 0 + for target in range(4): + for source in range(4): + if target == source: + continue + for x in ((0, 0, 0, 0), (1, 4, 0, 1), (-3, 2, -1, 7)): + base = evaluate(x, target, source) + for axis in range(4): + for shift in (-2**80, -1, 1, 2**80): + moved = list(x) + moved[axis] += 16 * shift + require(evaluate(moved, target, source)[4] == base[4], + "signed and large period translation") + period_checks += 1 + require(evaluate((0, 0, 0, 2), 0, 1)[4] != + evaluate((8, 0, 0, 2), 0, 1)[4], "period eight is insufficient") + require(evaluate((1, 4, 0, 1), 0, 1)[4] == (-9, 0, -5, -4), + "sharp complete endpoint") + require(half_round(1) != 1 and half_round(-1) != -1, "ties away differ") + invalid = [((0, 0, 0), 0, 1), ((0, 0, 0, 0), 1, 1), + ((0, 0, 0, 0), -1, 1), ((0, 0, 0, 0), 0, 4), + ((0, 0, 0, 0), True, 1), ((0, 0, 0, 0.5), 0, 1), + ((True, 0, 0, 0), 0, 1), ((2**128, 0, 0, 0), 0, 1)] + for x, target, source in invalid: + try: + evaluate(x, target, source) + except ValueError: + continue + raise ValueError("invalid input accepted") + return {"rounding_checks": 515, "period_checks": period_checks, + "rejected_inputs": len(invalid), "semantic_controls": 3} + + +def package_hashes(): + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "CODE-BOUNDS.md", "TASK.json", + "SOURCES.json", "VERIFY.json", "verify.py", "independent.py") + result = {} + for name in names: + path = package / name + require(path.is_file() and not path.is_symlink(), "regular package input") + require(path.stat().st_size <= 1024**2, "bounded receipt input") + result[name] = hashlib.sha256(path.read_bytes()).hexdigest() + source_path = package.parent / "walsh-interleaved-shear" / "PROOF.md" + require(source_path.stat().st_size <= 1024**2, "bounded predecessor input") + source_hash = hashlib.sha256(source_path.read_bytes()).hexdigest() + require(source_hash == "e16cb441209c6a093c2f21eeec96819b88a7f8a74bd7df103267ddf88c9f644a", + "predecessor context pin") + result["../walsh-interleaved-shear/PROOF.md"] = source_hash + return result + + +def main(): + report = {"status": "PASS_ROUNDED_HALF_SHEAR_WALSH", + "claim_type": "scoped proof with exhaustive finite corroboration", + "sharp_error": "9/8", "package_sha256": package_hashes(), + "controls": controls(), "census": census()} + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()