diff --git a/research/nearest-even-walsh-error/PROOF.md b/research/nearest-even-walsh-error/PROOF.md new file mode 100644 index 0000000000..6173c71bc7 --- /dev/null +++ b/research/nearest-even-walsh-error/PROOF.md @@ -0,0 +1,178 @@ +# Sharp deterministic error for normalized Walsh stages + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Fix a grid spacing h>0 and an integer J>=0. On an array with J selected +binary axes and any spectator axes, apply the J distinct factors + + H0 = (1/2) [[1,1],[1,-1]], + +one axis at a time, in any fixed order. After every factor, round each +coordinate to the nearest multiple of h, with ties to the even grid integer. +The input is any array in h Z, without a magnitude restriction in the +mathematical model. Every sum and difference before rounding is exact; +overflow and other arithmetic defects are excluded. + +Let T be the exact normalized Walsh operator and F its rounded version. +Then the sharp uniform coordinate bound is + + sup_(x in (h Z)^(2^J)) ||F(x)-T x||_infinity = h a_J, + a_J = J/3 + (1-(-1/2)^J)/9. (1) + +Spectator fibers are independent, so the same bound holds for any number +of spectators. Exact final recovery to the raw Walsh operator multiplies +the error by 2^J. In particular its sharp bound is h 2^J a_J. + +The more precise statement for one output coordinate is as follows. If +its stored output divided by h is even, the sharp absolute error is h a_J. +If it is odd and J>=1, the sharp absolute error is h a_(J-1). +At J=0 both errors are zero. + +The theorem concerns this deterministic quantizer. It is not a theorem for +arbitrary bounded faults, non-grid initial data, repeated axes, intervening +non-Walsh gates or the actual accelerated recursive supplier. + +## Reduction to a binary averaging tree + +Scale by h and work with integer grid values. Write R(s) for nearest-even +rounding of a real number to an integer. It is odd, and + + R(s+2k) = R(s)+2k (2) + +for every integer k. Translation by an odd integer need not commute with R. + +Fix an output of the J-stage butterfly network. Its dependencies form a +complete binary tree of depth J, with disjoint original inputs at its +leaves. Each internal node is R((u+v)/2) or R((u-v)/2). +Oddness lets us absorb every minus sign into the leaves and intermediate +subtrees. Thus it suffices to analyze a complete tree of rounded averages. +Its exact value is the average of its 2^J signed leaves. This reduction +uses distinct axes; repeated use of an axis need not give disjoint leaves. + +## Parity-sensitive bounds + +Let a_j and b_j be the maximal absolute error at depth j conditioned on +an even or odd integer output. Start with a_0=b_0=0. We prove inductively +that the finite maxima exist and satisfy + + b_j = a_(j-1), + a_j = 1/2 + (a_(j-1)+b_(j-1))/2. (3) + +Consider child outputs u,v. If u+v is even, the root division is exact. +The child parities agree, and averaging their errors costs at most +max(a_(j-1),b_(j-1))=a_(j-1). + +If u+v is odd, its half lies exactly between consecutive integers. The +stored root is even, its local error has magnitude 1/2, and the child +parities differ. The total error is therefore at most the second line +of (3). An odd root can occur only in the exact-division case, proving +the first line's upper bound. + +For completeness the second line dominates the exact-division bound. +Put d_j=a_j-a_(j-1). The recurrences give d_1=1/2 and + + d_j = (1-d_(j-1))/2, j>=2. + +Induction gives 1/4<=d_j<=1/2 for every j>=1. Hence a_j is increasing and +b_j<=a_j. This proves the comparisons used in the induction, without +assuming a closed form in advance. + +## Attaining inputs + +Construct integer leaf lists E_j,O_j with rounded outputs 0 and 1. +Their signed errors, stored output minus exact average, will be a_j,b_j. +Use concatenation, and let adding an integer to a list mean entrywise +addition. Define + + E_0=[0], O_0=[1], + E_j = E_(j-1) concatenated with (O_(j-1)-2), + O_j = E_(j-1) concatenated with (E_(j-1)+2). (4) + +By (2), the children of E_j have stored outputs 0,-1 and errors +a_(j-1),b_(j-1). Their root rounds -1/2 to 0, so its error is the second +line of (3). The children of O_j have outputs 0,2 and both have error +a_(j-1). Their root is exactly 1, proving the first line of (3). +Negating a leaf list attains the negative extremum. Even translations +give every other prescribed output of the same parity. + +The E_j entries lie in [-j,0]. In the ordinary low-bit-first Walsh +schedule, concatenate the lists along the last processed axis. Then its +zero-frequency output is exactly the averaging tree above. This proves +attainment in the actual butterfly network, rather than in a relaxed +independent-error model. Other fixed axis orders use the matching input +axis permutation. Therefore the coordinate upper bound and the sup norm +maximum in (1) are both sharp. + +Substituting b_j=a_(j-1) in (3), with a_0=0 and a_1=1/2, gives + + a_j = 1/2 + (a_(j-1)+a_(j-2))/2, j>=2. + +The expression (1) satisfies these initial conditions and recurrence, +which proves the formula. The usual stagewise bound is J h/2. Equation +(1) is strictly smaller for every J>=2, and its ratio to J h/2 tends to 2/3. +These are exact algebraic comparisons, not measured speedups. + +## Complete residue domains + +For depth J the error is periodic in each integer input coordinate with +period 2^(J+1). Indeed, add 2^(J+1) times an arbitrary integer array to +the input. After k stages its exact displacement has coordinates +divisible by 2^(J+1-k), which are even integers for all k<=J. Equation +(2) therefore propagates precisely that displacement through every +rounded stage. The final displacement equals the exact Walsh displacement, +so their error arrays coincide. This also holds in the presence of signs. + +Consequently the verifier's 4^2 one-stage inputs and 8^4 two-stage inputs +are complete residue-domain checks for those depths. Larger depths are +corroborated by witnesses and a parity-state enumeration; the all-J +conclusion rests on the proof above. + +## Application to PR #6119's numerical surrogate + +CubeJerry's PR #6119, head bdfe5a10d488b5f774e906d8d4588dc8da25e7ba, +defines an eight-input surrogate with exposure, four temporary coordinates, +the echo m=1/2,a=4, two distinct H0 axes and projection of the temporaries. +It rounds after its six nominated noisy maps to the same h grid. +Its arbitrary-defect theorem and its finite ternary-cube observation are +credited prior results and context; neither is re-audited here. + +For every grid retained coordinate x=h k, its initially zero echo temporary +becomes h R(k/2). The upper addition and its inverse are integer-grid +operations and cancel exactly. The lower inverse leaves, before rounding, + + h [R(k/2)-k/2], + +which is 0 or +/-h/2, and hence rounds to zero. Thus for every grid input +the entire rounded echo is the identity on retained data and returns the +temporary row to zero. The remaining retained computation is precisely +two rounded Walsh axes. Exposure and its inverse are exact permutations. +Its sharp normalized error is therefore 3h/4, for all eight grid inputs. + +At the predecessor's h=1/4 this is 3/16; exact raw recovery multiplies it +by four, giving 3/4. One attaining original-coordinate input is + + (0,0,-1/4,0,-1/2,0,0,0). + +The four entries of the first spectator fiber are E_2/4. This supplies an +all-grid theorem and explicit witness beyond the predecessor's finite +6,561-point cube. It is still a numerical surrogate, not a materialized +PR6030 child or a physical disposal implementation. + +## Limits and credit + +CubeJerry supplies the explicit open distinction between independent +defect boxes and deterministic quantizer errors, and the two-phase surrogate. +Vlado Vojdanovski's PR1673 supplies the normalized H0/deferred-row context; +the selected construction retains its original authors and five assumptions. +JoyboyBrian's `native-rounded-butterfly-contract` supplies related pair-first +nearest-even arithmetic and parity constraints for different complex Gaussian +letters. The present averaging-tree parity recurrence and attaining all-J +Walsh bound are the new result. + +No full selected replay, native admission, proof-kernel check or independent +human review is claimed. The theorem assumes exact pre-rounding arithmetic, +unbounded integer range and the specified grid ABI. Bit costs, intermediate +range guards, tape movement, reversible history and an accelerated supplier +remain separate obligations. Source files and the selected frontier are unchanged. diff --git a/research/nearest-even-walsh-error/README.md b/research/nearest-even-walsh-error/README.md new file mode 100644 index 0000000000..749def2f85 --- /dev/null +++ b/research/nearest-even-walsh-error/README.md @@ -0,0 +1,139 @@ +# Sharp nearest-even Walsh-stage error + +This contribution was produced by Nick Petalas. Apache-2.0. + +For J distinct normalized Walsh stages, with exact sums and differences +and nearest-even rounding to a common grid h after each stage, the sharp +uniform error over every grid input is + + h [J/3 + (1-(-1/2)^J)/9]. + +The usual stagewise bound is J h/2. The new bound is strictly smaller +for J>=2 and approaches two thirds of that coefficient. This is a scoped +mathematical proof with exact finite corroboration, not a new kappa. + +[PROOF.md](PROOF.md) proves the even/odd output recurrence and constructs +attaining integer inputs for every J. At even stored outputs the maximum +is h a_J; at odd outputs it is h a_(J-1). The attaining even-output inputs +use only integers between -J and zero in grid units. + +## New source application + +CubeJerry's [PR #6119](https://github.com/CrocSwap/integer-mult-bounds/pull/6119) +reports normalized error at most 3/16 on a finite cube for its particular +two-phase nearest-even surrogate at h=1/4. Its separate arbitrary-defect +box has a sharp bound of 1. The present result proves **3/16 is the exact +global error for every grid input** of that surrogate. Exact raw recovery +gives the sharp value 3/4. Its rounded echo returns the temporary row to +zero on every such input. This does not establish a physical erasure cost. + +The source is pinned as a literature reference at +`bdfe5a10d488b5f774e906d8d4588dc8da25e7ba`. Its explicit m=1/2,a=4 echo +becomes identity on grid inputs; the remaining computation is two rounded +Walsh axes. One new attaining original-coordinate input is +`(0,0,-1/4,0,-1/2,0,0,0)`. No predecessor verifier or census is imported, +executed or offered as this contribution. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nearest-even-walsh-error/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nearest-even-walsh-error/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nearest-even-walsh-error +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nearest-even-walsh-error --check-source-history +``` + +Another CPython 3.12 interpreter may replace that absolute path. The last +command checks publication bytes after committing. Direct verification +prints a generated SHA256-bound JSON receipt with status +`PASS_NEAREST_EVEN_WALSH_ERROR` and writes no files. + +The exact finite coverage is: + +- 2,049 signed half-integers checked against a separate exact Fraction + nearest-even implementation, including the tie-output parity. +- All 16 one-stage and 4,096 two-stage residue inputs, with every output + compared to the literal Walsh coefficient formula. Error periodicity + makes these complete integer-input domains at those two depths. +- Reachable error sets classified by output parity through depth seven, + independently of the proposed closed formula. +- Even- and odd-output attaining witnesses through depth twelve, in both + low-bit-first and reversed schedules, with every output checked and + negative witnesses checked by actual execution. +- 256 signed periodicity fixtures through eight stages, 513 echo values + and 65 full eight-coordinate source-application fixtures. +- Four scope controls and five rejected invalid inputs. Off-grid data + give error 7/8 at J=2; different tie rules can give error 1. These + explicitly reject unwarranted extensions of the 3/4 grid-unit theorem. + +The finite checks corroborate the all-J written proof. They do not replace +its quantifiers or supply independent human or proof-kernel review. + +## Scope, provenance and overlap + +The original `uniform-transfer-audit` card is explicitly changed to this +numerical side theorem for the `precision_tape` boundary. It does not +discharge any selected framework assumption. The authenticated selected +metadata baseline passed at main +`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. Its selected +conditional kappa is 0.003125804. No selected cold replay was needed or run. + +This is a new quantizer-specific step beyond PR6119's finite cube, not an +audit of its arbitrary-defect theorem. Source questions and exact reference +heads are in [TASK.json](TASK.json). The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241916) +records the expected scope. Live PRs, recent account work, Discussion +claims, local reservations, main text and merged-PR searches were checked. +The overlap cache covered 379 open PRs and 5,777 Discussion records with +complete remote pagination, but only 70 of 8,348 local note paths. Direct +Git searches supplemented that sparse coverage. These are bounded overlap +checks, not proof of global novelty. + +The theorem requires grid input, distinct Walsh axes, the specified tie +rule, exact pre-rounding arithmetic and sufficient range. Arbitrary faults, +non-grid inputs, other gates, repeated axes and complex Gaussian butterflies +need separate bounds. A real emitted recursive caller, bit costs, overflow +guards, tape routing, reversible history and supplier admission remain open. +The selected frontier and all five assumptions are unchanged. No Lean, +Docker, full native replay or complete multiplication theorem is claimed. + +## Engineering bounds + +The verifier has no recursion, subprocesses or external mathematical imports. +Its transform accepts at most 4,096 entries and signed inputs of magnitude +at most 2^64. The formula interface permits depths through 64; executed +full witnesses stop at twelve. Every function is below 60 physical lines. +The largest explicit exhaustive input domain has 4,096 tuples; the parity +enumeration stops at seven and stores at most 627 errors in one parity set. +All checks use explicit exceptions and remain active under optimization. + +Python's required dynamic allocation is the bounded managed-runtime +deviation from Power of Ten static allocation. Lists, integer sizes and +set domains are bounded by the fixed limits above. Receipt reads are +limited to twelve package files of at most one MiB each. Warning-strict +normal and optimized checks provide runtime diagnostics; no shared build +configuration is changed. This offline verifier is not a machine-cost model. + +## Open next questions + +1. Bind the sharp bound to an actual emitted recursive H0 boundary with + its grid, axis ordering, pre-rounding arithmetic and range guards. + First export that complete event list; it is missing here. The smaller + logical error coefficient alone supplies no accelerated physical bill. +2. Can an analogous parity-state analysis sharpen deterministic rounding + for the actual complex Gaussian butterflies? Start with their joint + real/imaginary parity states. Their mixing and error amplification + differ from this real averaging tree, so this formula does not transfer. + +## Credit + +Credit CubeJerry for PR6119's explicit surrogate and separation between +defect boxes and quantizer correlations; Vlado Vojdanovski for PR1673's +normalized H0/deferred-row interface; and JoyboyBrian for related pair-first +nearest-even Gaussian butterfly arithmetic and parity constraints. Their +native, analytic, compiler and selected-construction predecessors retain +their attribution. The new result is the all-J parity recurrence, its +sharp attaining family and the all-grid two-phase consequence. Independent +human and formal proof-kernel review are unclaimed. diff --git a/research/nearest-even-walsh-error/SOURCES.json b/research/nearest-even-walsh-error/SOURCES.json new file mode 100644 index 0000000000..40f96c767a --- /dev/null +++ b/research/nearest-even-walsh-error/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/nearest-even-walsh-error/TASK.json b/research/nearest-even-walsh-error/TASK.json new file mode 100644 index 0000000000..22b6bcac17 --- /dev/null +++ b/research/nearest-even-walsh-error/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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 nearest-even normalized Walsh-stage error and the all-grid two-phase numerical consequence of PR6119.", + "scope_change_reason": "The generic assumption audit is replaced by an original quantizer-specific numerical theorem; no selected assumption is discharged.", + "bottleneck_link": "A sharp deterministic rounding coefficient can fund a smaller logical precision allowance at a compatible emitted H0 boundary; physical implementation remains separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp bound and attaining construction; do not extend to other butterflies or a physical supplier.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; exact parity recurrence, complete one/two-stage residue domains and constructive all-depth witnesses.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this sharp real Walsh bound be bound to an actual emitted recursive H0 boundary?", + "why_it_matters": "A compatible source contract could lower its logical rounding allowance.", + "first_step": "Export the entire event list, grid, distinct axis order and arithmetic/range contract.", + "blocked_by": "No actual emitted accelerated child or physical cost contract is supplied." + }, + { + "question": "Can parity-state analysis sharpen the deterministic error of actual complex Gaussian butterflies?", + "why_it_matters": "Their current sufficient bounds permit independently aligned faults that may be unrealizable.", + "first_step": "Derive joint real/imaginary reachable parity states for one exact source butterfly.", + "blocked_by": "Complex mixing and amplification are outside the averaging-tree recurrence." + } + ], + "question_source": { + "pr": 6119, + "author": "CubeJerry", + "head": "bdfe5a10d488b5f774e906d8d4588dc8da25e7ba", + "path": "research/deferred-row-rounding-audit/PROOF.md", + "role": "Sections 3 and 6 distinguish independent defect boxes from the actual deterministic quantizer; the new result resolves its all-grid Walsh consequence." + }, + "predecessors": [ + { + "pr": 6119, + "author": "CubeJerry", + "head": "bdfe5a10d488b5f774e906d8d4588dc8da25e7ba", + "role": "Two-phase numerical surrogate and finite quantizer observation, cited rather than audited." + }, + { + "pr": 1673, + "author": "Vlado-V", + "role": "Normalized H0 and deferred-row source context." + }, + { + "path": "research/native-rounded-butterfly-contract/README.md", + "author": "JoyboyBrian", + "role": "Related nearest-even complex butterfly arithmetic and parity constraints; no transferred error formula." + } + ] +} diff --git a/research/nearest-even-walsh-error/VERIFY.json b/research/nearest-even-walsh-error/VERIFY.json new file mode 100644 index 0000000000..682668f914 --- /dev/null +++ b/research/nearest-even-walsh-error/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": "Complete small residue domains, parity error sets, attaining witnesses, periodicity, source application and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact scientific checks with assertions disabled." + } + ] +} diff --git a/research/nearest-even-walsh-error/verify.py b/research/nearest-even-walsh-error/verify.py new file mode 100644 index 0000000000..dd0debe462 --- /dev/null +++ b/research/nearest-even-walsh-error/verify.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Exact sharp nearest-even normalized Walsh bound. Nick Petalas. Apache-2.0.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def half_even(numerator): + quotient, remainder = divmod(numerator, 2) + return quotient + (remainder & (quotient & 1)) + + +def quantizer_checks(): + count = 0 + for numerator in range(-1024, 1025): + value = half_even(numerator) + require(value == round(Fraction(numerator, 2)), "independent signed nearest-even oracle") + require(numerator % 2 == 0 or value % 2 == 0, "half-tie output is even") + count += 1 + return count + + +def transform(values, rounded=True, reverse=False): + """Input and output are integers in units of one common grid step.""" + n = len(values) + require(1 <= n <= 4096 and n & (n - 1) == 0, "power-of-two size <=4096") + require(all(type(v) is int and abs(v) <= 2**64 for v in values), "integer input bound") + out = list(values) + stages = list(range(n.bit_length() - 1)) + if reverse: + stages.reverse() + for bit in stages: + width = 1 << bit + for start in range(0, n, 2 * width): + for i in range(start, start + width): + left, right = out[i], out[i + width] + if rounded: + out[i], out[i + width] = half_even(left + right), half_even(left - right) + else: + out[i], out[i + width] = left + right, left - right + return out + + +def bound(depth): + require(type(depth) is int and 0 <= depth <= 64, "depth 0..64") + return Fraction(depth, 3) + (1 - Fraction(-1, 2)**depth) / 9 + + +def error_numerators(values, reverse=False): + exact = transform(values, rounded=False) + computed = transform(values, reverse=reverse) + return [len(values) * y - z for y, z in zip(computed, exact)] + + +def literal_walsh(values): + n = len(values) + require(n <= 16, "literal Walsh oracle capacity") + return [sum((-1 if (i & j).bit_count() % 2 else 1) * x + for j, x in enumerate(values)) for i in range(n)] + + +def exhaustive_residue_checks(): + counts = [] + for depth in (1, 2): + n = 1 << depth + maximum, maximizing = -1, None + for values in product(range(2 * n), repeat=n): + exact = literal_walsh(values) + require(transform(values, rounded=False) == exact, "closed Walsh formula") + computed = transform(values) + error = max(abs(n * y - z) for y, z in zip(computed, exact)) + require(error <= n * bound(depth), "complete residue-domain bound") + if error > maximum: + maximum, maximizing = error, values + require(Fraction(maximum, n) == bound(depth), "complete residue-domain sharpness") + counts.append({"depth": depth, "inputs": (2 * n)**n, + "maximum": str(Fraction(maximum, n)), "witness": maximizing}) + return counts + + +def tree_error_sets(): + """Enumerate attainable scaled errors by output parity, without the formula.""" + even, odd = {0}, {0} + result = [] + for depth in range(1, 8): + scale = 1 << (depth - 1) + same = {x + y for group in (even, odd) for x in group for y in group} + mixed = {x + y + sign * scale for x in even for y in odd for sign in (-1, 1)} + even, odd = same | mixed, same + expected = (1 << depth) * bound(depth) + require(max(even) == -min(even) == expected, "even-output reachable extrema") + require(max(odd) == -min(odd) == (1 << depth) * bound(depth - 1), + "odd-output reachable extrema") + result.append({"depth": depth, "even_errors": len(even), "odd_errors": len(odd), + "maximum_scaled_error": max(even)}) + return result + + +def witness_checks(): + even, odd = [0], [1] + result = [] + for depth in range(13): + n = 1 << depth + for parity, values in enumerate((even, odd)): + for reverse in (False, True): + if reverse: + indices = [int(f"{i:0{depth}b}"[::-1], 2) if depth else 0 for i in range(n)] + current = [values[i] for i in indices] + else: + current = values + computed = transform(current, reverse=reverse) + errors = error_numerators(current, reverse=reverse) + target = bound(depth) if parity == 0 else bound(max(0, depth - 1)) + require(computed[0] == parity, "attaining output parity") + require(Fraction(errors[0], n) == target, "constructive sharpness") + require(max(map(abs, errors)) <= n * bound(depth), "all witness outputs") + require(transform([-x for x in current], reverse=reverse) == [-y for y in computed], + "negative sharpness by oddness") + require(min(even) >= -depth and max(even) == 0, "small attaining input range") + result.append({"depth": depth, "sharp_error": str(bound(depth)), + "input_minimum": min(even), "input_maximum": max(even)}) + if depth < 12: + even, odd = even + [x - 2 for x in odd], even + [x + 2 for x in even] + return result + + +def periodicity_checks(): + count = 0 + for depth in range(1, 9): + n = 1 << depth + for sample in range(16): + values = [((i * 8191 + sample * 127) % 20001) - 10000 for i in range(n)] + shifts = [((i * 11 + sample * 5) % 17) - 8 for i in range(n)] + shifted = [x + 2 * n * z for x, z in zip(values, shifts)] + for reverse in (False, True): + require(error_numerators(values, reverse) == error_numerators(shifted, reverse), + "period 2^(J+1) in each input") + count += 1 + return count + + +def deferred_echo_checks(): + """New all-grid application; no predecessor code is imported or executed.""" + count = 0 + for x in range(-256, 257): + temporary = half_even(x) + retained = x + 4 * temporary + retained -= 4 * temporary + temporary = half_even(2 * temporary - retained) + require(retained == x and temporary == 0, "rounded echo endpoint") + count += 1 + require(bound(2) / 4 == Fraction(3, 16), "normalized two-stage application") + require(bound(2) == Fraction(3, 4), "raw two-stage application") + return count + + +def deferred_model(values): + """Integer-grid implementation of the stated eight-coordinate application.""" + require(len(values) == 8, "eight-coordinate application") + permutation = [(i & 4) | ((i & 1) << 1) | ((i & 2) >> 1) for i in range(8)] + work = [values[i] for i in permutation] + [0] * 4 + for i in range(4): + work[i + 8] = half_even(work[i]) + work[i] += 4 * work[i + 8] + work[i] -= 4 * work[i + 8] + work[i + 8] = half_even(2 * work[i + 8] - work[i]) + require(work[8:] == [0] * 4, "application clean temporary row") + for i in range(0, 12, 2): + left, right = work[i], work[i + 1] + work[i], work[i + 1] = half_even(left + right), half_even(left - right) + out = [work[i] for i in permutation] + for i in range(4): + left, right = out[i], out[i + 4] + out[i], out[i + 4] = half_even(left + right), half_even(left - right) + return out + + +def application_checks(): + inputs = [[0, 0, -1, 0, -2, 0, 0, 0]] + inputs += [[((i * 31 + sample * 17) % 257) - 128 for i in range(8)] for sample in range(64)] + maximum = 0 + for values in inputs: + exact = [sum((-1 if (i & j & 6).bit_count() % 2 else 1) * x + for j, x in enumerate(values) if (i ^ j) & 1 == 0) for i in range(8)] + computed = deferred_model(values) + error = max(abs(4 * y - z) for y, z in zip(computed, exact)) + require(error <= 3, "full application all-output bound") + maximum = max(maximum, error) + require(maximum == 3, "full application attaining witness") + return {"fixtures": len(inputs), "sharp_normalized_error_at_h_quarter": str(Fraction(maximum, 16)), + "sharp_raw_error_at_h_quarter": str(Fraction(maximum, 4))} + + +def semantic_controls(): + values = [Fraction(3, 4), Fraction(3, 4), Fraction(3, 2), Fraction(3, 2)] + first = [round((values[0] + values[1]) / 2), round((values[2] + values[3]) / 2)] + off_grid_error = abs(round(Fraction(sum(first), 2)) - sum(values) / 4) + require(off_grid_error == Fraction(7, 8) > bound(2), "off-grid exclusion") + for mode in ("away", "floor"): + values = [0, 1, 1, 2] + first = [] + for i in (0, 2): + numerator = values[i] + values[i + 1] + first.append((numerator + 1) // 2 if mode == "away" else numerator // 2) + numerator = sum(first) + result = (numerator + 1) // 2 if mode == "away" else numerator // 2 + require(abs(Fraction(result) - Fraction(sum(values), 4)) == 1 > bound(2), + "different tie rule exclusion") + require(bound(3) > bound(2), "two-stage value cannot be used at every depth") + rejected = 0 + for values in ([], [0, 0, 0], [Fraction(1, 2), 0], [True, 0], [2**65, 0]): + try: + transform(values) + except ValueError: + rejected += 1 + require(rejected == 5, "invalid domains rejected") + return {"semantic_exclusions": 4, "invalid_inputs": rejected, "off_grid_error": str(off_grid_error)} + + +def main(): + result = {"status": "PASS_NEAREST_EVEN_WALSH_ERROR", "signed_half_checks": quantizer_checks(), + "residue_censuses": exhaustive_residue_checks(), + "reachable_tree_errors": tree_error_sets(), "sharp_witnesses": witness_checks(), + "periodicity_fixtures": periodicity_checks(), "echo_grid_values": deferred_echo_checks(), + "application": application_checks(), "controls": semantic_controls(), "new_kappa_claimed": False} + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + require(len(files) <= 12 and all(p.stat().st_size <= 1024**2 for p in files), "package receipt capacity") + receipt = {"python": platform.python_version(), + "package_sha256": {p.name: sha256(p.read_bytes()).hexdigest() for p in files}, + "result": result} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()