diff --git a/research/clean-residual-dilation/CERTIFICATE.json b/research/clean-residual-dilation/CERTIFICATE.json new file mode 100644 index 0000000000..673f9be0d0 --- /dev/null +++ b/research/clean-residual-dilation/CERTIFICATE.json @@ -0,0 +1,83 @@ +{ + "assignment_seed": 51, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "collapsed_host_moment_ratio": "2", + "collapsed_host_sandwich_profile": { + "9": 2 + }, + "coverage": { + "Walsh_child_reduction_columns_both_directions": 1024, + "binomial_dp_widths": [ + 0, + 288 + ], + "clean_basis_columns": 512, + "collapsed_program_basis_columns": 1024, + "dilation_counts_sha256": "eb2a043145ad2440ac4248b31833b6ed865c438d91fc6aa62271441c531fd45a", + "dilation_f": [ + 1, + 32 + ], + "dirty_basis_columns": 512, + "dirty_repaired_basis_columns": 512, + "independent_tensor_columns": 512 + }, + "dirty_complement_multiplicities": [ + 24, + 88, + 232, + 168 + ], + "free_host_moment_ratio_lower_bound": "4", + "free_host_width_profile": { + "4": 2, + "5": 2, + "9": 2 + }, + "host_multiplicities": [ + 160, + 224, + 352, + 288 + ], + "moment_ratio_lower_bound_for_0_lt_sigma_le_1": "5", + "negative_controls": { + "omit_host_calls": "REJECTED on source basis column 0", + "omit_host_entry": "REJECTED on source basis column 0", + "omit_normalization": "REJECTED on source basis column 0", + "omit_source_boundaries": "REJECTED on source basis column 0", + "rank_two_into_two_rank_one_owners": "REJECTED: missing -1 eigenspace", + "unrestored_dirty_workspace": { + "scratch_basis_column": 63, + "status": "REJECTED", + "unrepaired_phase_exponent": 3 + }, + "wrong_dirty_repair_sign": { + "scratch_basis_column": 63, + "status": "REJECTED", + "unrepaired_phase_exponent": 3 + }, + "wrong_eigenvalue_route": "REJECTED" + }, + "object": { + "a": 4, + "b": 5, + "coefficients_per_stream": 512, + "r": 9 + }, + "recursive_width_profile": { + "4": 3, + "5": 3, + "9": 2 + }, + "route_sha256": "a73a93797b26756588687ca65516c17d45ee59079f8c901d3911d6b2a879454b", + "scope": "Exact finite operator replay and written all-f algebraic argument; this literal encoder loses even with free routing and owner calls. No all-size tape compiler, global lower bound, or new kappa.", + "source_multiplicities": [ + 136, + 136, + 120, + 120 + ], + "status": "PASS_EXACT_DILATION_AND_UNFAVORABLE_BOUNDARY_BUDGET", + "uniform_capacity_slack_lower_bound": "3/64" +} diff --git a/research/clean-residual-dilation/CLAIM.json b/research/clean-residual-dilation/CLAIM.json new file mode 100644 index 0000000000..e70776db74 --- /dev/null +++ b/research/clean-residual-dilation/CLAIM.json @@ -0,0 +1,55 @@ +{ + "track": "Recursive interfaces", + "assignment_seed": 51, + "randomness": "python3 secrets.randbelow(100), operating-system randomness; drawn once", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T02:56:12Z", + "selection_deadline_utc": "2026-10-13T03:04:12Z", + "verification_starts_by_utc": "2026-10-13T03:26:12Z", + "expected_finish_utc": "2026-10-13T03:36:12Z", + "coordination": "No pinned issues; only open issue #650 concerns Discussions. Claim recorded locally as requested.", + "candidates": [ + { + "task": "Defer dirty-helper cleanup across successive calls", + "decision": "Not selected: extensive cold-end, gauge and deferred-readout work in existing suppliers and open PRs." + }, + { + "task": "Clean-workspace spectral embedding of a width-9 complex residual into two separate owners", + "decision": "Selected: changes the arbitrary-dirty similarity hypothesis in #451; explicit encoder and full boundary cost, not another split-routing replay." + }, + { + "task": "Fuse consecutive native bit queries", + "decision": "Not selected: #521 already supplies an exact dirty-input primitive; avoid duplicating it." + } + ], + "object": "C_(9f) into C_(4f) direct-sum C_(5f), one equally sized zero workspace, f>=1. Seed selects a=1+(51 mod 8)=4, b=9-a=5.", + "method": "Exact fourth-root eigenspace multiplicities and an explicit Walsh/permutation encoder; exact finite all-basis replay and negative controls; bill both encoder boundaries, owners, workspace and restoration.", + "deliverable": "Scoped research note, exact reproducible standard-library certificate/checker and full conditional cost recurrence; no kappa claim.", + "overlap_checked": { + "open_pr_count": 480, + "relevant_prs": [ + 448, + 451, + 480, + 481, + 494, + 521, + 627, + 633 + ] + }, + "scope_exclusions": [ + "No selected-certificate edits", + "No supplier or upstream modifications", + "No claim that a finite replay proves an all-size tape compiler" + ], + "result": { + "status": "Completed research note and scoped negative cost result; no new kappa", + "finding": "For every f>=1, C_(9f) embeds in C_(4f) direct-sum C_(5f) with a complementary workspace phase. One phase pass restores arbitrary dirty workspace. The literal recursive moment costs at least five times a single residual (four with free hosts); host collapse leaves two width-9f transforms, and full collapse recovers the original call.", + "evidence": "512 clean columns, 512 dirty columns, 512 repaired columns; independent tensor entries; 1024 Walsh reduction checks; 1024 collapsed-circuit columns; 8 mathematical negative controls.", + "refinement": "The clean embedding also supplies a dirty interface after an explicit complementary phase repair; this is the same encoded residual, not a second investigation.", + "link": "https://github.com/CrocSwap/integer-mult-bounds/tree/research/seed51-clean-residual-dilation/research/clean-residual-dilation", + "verification_started_utc": "2026-10-13T03:12:40Z", + "reproduce": "python3 -B research/clean-residual-dilation/verify.py" + } +} diff --git a/research/clean-residual-dilation/README.md b/research/clean-residual-dilation/README.md new file mode 100644 index 0000000000..48408f9431 --- /dev/null +++ b/research/clean-residual-dilation/README.md @@ -0,0 +1,324 @@ +# Spectral split residuals: an exact interface with an unfavorable boundary cost + +Research note and scoped negative result. Douglas R. Colkitt, with substantial +OpenAI Codex assistance. Apache-2.0. No new multiplication exponent. + +An explicit encoder can put the complex residual `C_(9f)` into two separate +streams acted on by `C_(4f)` and `C_(5f)`, for every integer `f >= 1`. +Zero workspace returns to zero. Arbitrary dirty workspace can also be restored +by one explicitly described phase pass. This changes the interface behind the +earlier split-residual obstruction: it uses payload transforms and a phase +correction, not just a routing conjugation. + +The proposed implementation nevertheless fails its favorable cost screen. +Its literal recursive profile is `2 C_(9f) + 3 C_(4f) + 3 C_(5f)`, on the +original per-stream volume. Even granting the two owner kernels for free +leaves `2 C_(9f) + 2 C_(4f) + 2 C_(5f)`. An obvious algebraic simplification +removes the owner sandwiches and leaves two width-9f transforms. Recognizing +the entire remaining operator simply recovers the original `C_(9f)` call. +This supplies no saving, even before movement, precision and workspace costs. + +The result is an algebraically feasible alternative interface and an exact +accounting diagnostic for this encoder. It is **not** an impossibility theorem +for encoded hosting, a repair of #448's priced word, or a new supplier. + +## Reproduce + +From the repository root, with Python 3.10 or later and no external packages: + +```sh +python3 -B research/clean-residual-dilation/verify.py +``` + +Expected output starts with +`PASS_EXACT_DILATION_AND_UNFAVORABLE_BOUNDARY_BUDGET`. The command checks source +pins, recomputes the certificate and compares every field with +[CERTIFICATE.json](CERTIFICATE.json). `--write /tmp/dilation.json` writes the +same deterministic result separately. It also works with `python3 -I -O`; +admission checks do not use Python `assert`. + +## Starting point and scope selection + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. At this base the selected +conditional result is #626/#623/#622 with #543, +`kappa = 51110230636731/31250000000000000`. The +[selected review](../../docs/research/community-k492-review.md) and its actual +construction were read. The complex supplier binds. This note does not adopt +larger numbers from pending PRs. + +The OS-generated assignment seed was **51**, assigning the recursive-interface +track. Among deferred helper cleanup, encoded residual hosting, and native bit +query fusion, hosting was selected. Cold-end/cleanup work is already extensive; +#521 has an exact native bit fusion primitive. The seed picks the split +`a = 1 + (51 mod 8) = 4`, `b = 9-a = 5`. Width 9 is motivated by the complex +helper geometry, not by treating a pending record as accepted. In particular, +the selected global profile already hosts whole helpers and has no width-9 +child to which this note claims to apply a saving. + +There was no pinned coordination issue. The local [claim](CLAIM.json) records +the three candidates, overlap checks, scope and time allocation. Exact source +and PR heads are in [SOURCE-PINS.json](SOURCE-PINS.json). + +## What changes relative to the prior obstruction + +Chafik Boukhalfa's [#451 trace obstruction](https://github.com/CrocSwap/integer-mult-bounds/blob/f3a38153678b55063fc005901cc968266166507d/research/cross-family-residual-obstruction/README.md) +shows that `C_(a+b) direct-sum I` and `C_a direct-sum C_b` have different traces. +They cannot be conjugate by an invertible linear map on the two complete +streams. The later [#448 discussion](https://github.com/CrocSwap/integer-mult-bounds/pull/448#issuecomment-6113842081) +also acknowledges the missing single-register, multi-stream realization. +Those findings remain valid. + +Here a clean-input embedding leaves a complementary operator `B`, not `I`, on +the workspace. An additional `B^-1` phase pass then restores dirty workspace. +Thus the full program is not merely a similarity between the two operators +in #451. The proof below constructs the encoder and exposes its expense. +It does not rerun the already closed coordinate-routing search. + +The [earlier Fourier boundary diagnostic](../fourier-boundary-fusion/REPORT.md) +already charged entrance and exit transforms in a copied-center scatter and +proved a scoped coordinate-cut inequality. This note credits that warning; +its new object is a direct sum of two separately acted-on streams, its changed +assumption is a spectral embedding with a complementary workspace action, and +its evidence includes exact dirty restoration. It does not claim a new +coordinate-only lower bound. + +## Exact operator and all-f embedding + +Work over the Gaussian rationals. Let + +```text +C = (1/2) [[1+i, 1-i], [1-i, 1+i]], +H = [[1, 1 ], [1, -1 ]]. +``` + +On an `N = 2^e` coefficient stream, `C_k` and `H_k` act on the low `k` +address coordinates and leave the others as spectators. Here `e = 9f`. +`H_k^-1 = 2^-k H_k`, and + +```text +H_k C_k H_k^-1 = Delta_k, +Delta_k[x,x] = i^(popcount(x mod 2^k)). +``` + +The multiplicity of `i^j` in `C_k` is + +```text +d_j(k;e) = 2^(e-k) sum_{t = j mod 4} binom(k,t), j=0,1,2,3. +``` + +An injective intertwiner from `C_e` into `D = C_(4f) direct-sum C_(5f)` +exists exactly when each source eigenspace fits into its corresponding host +eigenspace. Necessity follows because an injective intertwiner maps each +eigenspace injectively to the same eigenvalue; sufficiency follows by choosing +such injections. All operators are diagonalizable since their fourth power +is the identity over a characteristic-zero field containing `i`. + +At `f=1`, the exact dimensions are: + +| Operator on one or two 512-coefficient streams | 1 | i | -1 | -i | +|---|---:|---:|---:|---:| +| source `C_9` | 136 | 136 | 120 | 120 | +| first host `C_4` | 64 | 128 | 192 | 128 | +| second host `C_5` | 96 | 96 | 160 | 160 | +| total host | 160 | 224 | 352 | 288 | +| workspace complement | 24 | 88 | 232 | 168 | + +For completeness, this is not just a favorable finite example. Put +`p_j(k) = 2^-k sum_{t=j mod 4} binom(k,t)`. Pascal's identity gives + +```text +p_j(k+1) = (p_j(k) + p_(j-1 mod 4)(k))/2. +``` + +Consequently `min_j p_j(k)` is nondecreasing and `max_j p_j(k)` is +nonincreasing. The exact rows at 4, 5 and 9 give + +```text +min p(4) = 1/8, min p(5) = 3/16, max p(9) = 17/64. +``` + +For every `f>=1` and every `j`, the host capacity minus source demand, +divided by `N`, is therefore at least + +```text +1/8 + 3/16 - 17/64 = 3/64 > 0. +``` + +This is a written proof for all `f`; the checker additionally compares +binomial and independent dynamic-programming counts through width 288 and +checks the proposed dilations for `f=1,...,32`. Those finite counts are not +presented as the proof of the universal statement. + +## A literal encoder and its dirty restoration + +Enumerate source addresses in increasing order. Send each source address to +the first unused host coordinate with the same phase eigenvalue, first +through host A and then host B. Complete this injection to a permutation `P` +by mapping the workspace addresses, in increasing order, to the unused host +slots, also in increasing order. This specifies a full permutation of `2N` +coordinates, not a copy or a many-to-one map. + +Define + +```text +E = (H_(4f)^-1 direct-sum H_(5f)^-1) P (H_e direct-sum I). +``` + +All factors are invertible. Let `B` be the diagonal phase on the workspace +whose `j`th entry is the host phase at `P[N+j]`. Direct conjugation gives + +```text +E^-1 D E = C_e direct-sum B, +(I direct-sum B^-1) E^-1 D E = C_e direct-sum I. +``` + +The first identity implements `(h,0) -> (C_e h,0)`. The second implements +`(h,z) -> (C_e h,z)` for arbitrary dirty `h,z`. `B^-1` is an address-dependent +unit phase, not another recursive transform. It must still be computed and +applied. At `f=1`, scratch basis column 63 acquires phase `-i` if this repair +is omitted. The trace has not disappeared: it is carried by `B` and changed +by the explicitly added correction. + +This is a standalone residual primitive. During `E` both streams contain +linear combinations of their inputs. No unchanged local scalar word is +allowed to read a supposedly single helper at an intermediate point. A port +to actual owner windows would have to provide exclusive use of both full +streams and compatible intervening operations. No such port is supplied. + +## Complete recurrence and favorable cost screen + +Let `T(k,N,p)` be the cost of the inherited `C_k` primitive on **N original +coefficient positions**, with coefficient bit budget `p`. In a parent at +width `mf`, all children below have the same `N=V/W` logical coefficient +volume. The workspace is another physical stream, not a second independent +copy of the requested input and not permission to replace `N` by `N/2`. + +The inherited exact identity, also tested here, is + +```text +H_k = (1-i)^k S_k C_k S_k, +H_k^-1 = 2^-k (1-i)^k S_k C_k S_k, +S_k[x,x] = i^(popcount(x mod 2^k)). +``` + +Each Walsh boundary therefore costs one width-k child plus two coefficient +passes, with its exact scalar combined into the second pass. There are six +Walsh boundaries and two owner calls. With `e=9f`, the full local bill is + +```text +R(e,N,p) <= 2 T(e,N,p') + 3 T(4f,N,p') + 3 T(5f,N,p') + + 12 Scan(N,p') + Scan(N,p') + + 2 Route(2N,e,p') + Prep(e,p'). +``` + +`Scan` pays a full coefficient pass, including its specified unit phase and +Gaussian-dyadic scalar multiplication. The thirteenth pass is dirty +restoration. `Route` includes reading, moving and writing both streams; it +includes creating and clearing private keys and sorting buffers. `Prep` includes the multiplicity +table, route descriptors and scalar preparation. For the clean variant, +replace the final repair pass by a paid initialization pass unless zero +workspace is explicitly supplied. No additional source copy is used. The +borrowed dirty variant restores its entire extra stream at return. + +These terms can be bounded without a unit-cost wide-address assumption. +Binomial prefix counts rank and unrank the four phase classes. Binary search +in the count of unused slots handles the completed workspace permutation. +With `L=ceil(log2(2N))` and `Q=p+e+L+1`, quadratic integer arithmetic and +sequential merge routing give the conservative combined nonrecursive bound +`O(N Q^4 + Q^5)`, and `O(N Q + Q^4)` temporary bits, including route records. +For example there are `O(e^2)` prefix-count table entries of `O(e)` bits; +ranking uses `O(e)` such operations, and workspace unranking at most another +`O(e)` bisections. Routing sorts `2N` keyed records in `O(L)` merge passes. +This generous bound is only a complete upper invoice, not a transfer into +the repository's tight fixed-tape overhead allowance. + +The coefficients are exact Gaussian dyadics. Every layer introduces only +`O(e)` numerator or denominator bits: the program has a fixed number of +transforms, their scalars have `O(e)` bits, and a butterfly sums at most four +integer components. Thus `p'=p+O(e)` suffices for this exact arithmetic +description. This does not establish the inherited numerical rounding or +precision guard for a new all-size supplier. Granting `p'=p` only makes the +following rejection more favorable. + +In a conditional parent recurrence, replacing a single width-9f child by the +literal interface changes its term from + +```text +(9/m)^sigma / W +``` + +to + +```text +[2 (9/m)^sigma + 3 (4/m)^sigma + 3 (5/m)^sigma] / W. +``` + +For `0= 5 (>= 4 with free hosts; 2 after host collapse)." + }, + { + "name": "reject omitted source boundary in committed certificate", + "exit_code": 1, + "seconds": 3.928, + "expected_pass": false, + "last_output": "ValueError: committed certificate differs from the replay" + }, + { + "name": "reject corrupt inherited operator source", + "exit_code": 1, + "seconds": 0.046, + "expected_pass": false, + "last_output": "ValueError: source pin mismatch: notes/general-clifford-frames.tex" + } + ], + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "regular_replay": { + "command": "python3 -B research/clean-residual-dilation/verify.py --write research/clean-residual-dilation/CERTIFICATE.json", + "exit_code": 0, + "wall_seconds": 3.98 + }, + "optimized_replay": { + "command": "python3 -I -O research/clean-residual-dilation/verify.py", + "exit_code": 0 + }, + "selected_record_check": { + "command": "make selected-record-check", + "exit_code": 0, + "kappa": "51110230636731/31250000000000000" + }, + "upstream_preservation": { + "command": "git diff --exit-code -- upstream/", + "exit_code": 0 + }, + "final_overlap_refresh": { + "open_pr_count": 482, + "arrivals": [ + { + "number": 662, + "title": "Tooling: accelerate exact Clifford helper checks with identical receipts", + "head": "458744109003e0958798f27c1f04be78f03663ce" + }, + { + "number": 661, + "title": "Scoped negative result: R420 phase-B frames are moment-optimal at fixed gate order", + "head": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89" + } + ], + "pinned_coordination_issues": [], + "main_head": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "conclusion": "New arrivals concern fixed-order bit frames and Clifford verifier speed; no matching spectral split-residual scope found." + }, + "not_run": [ + "full make verify", + "frontier626 cold supplier replay", + "Linux CI", + "Lean build" + ], + "check_scope": "New standalone package only; selected suppliers and upstream source files are unchanged. Finite exact checks supplement the written all-f algebraic proof, not a full theorem or compiler verification.", + "artifact_sha256": { + "verify.py": "81248ba140b100c2660f25bd79a1869191c8b1bb875bf547ea0248cd30cba88e", + "README.md": "e6cfe4bbbc0879a4b5711a34098b624b82ef549ff09fbe8ac908b479c4e2b146", + "CERTIFICATE.json": "22bff5e3bdf72416574c10298d65fdcb0350b7cf8e83a1d3c52e54bf7204cbf7", + "SOURCE-PINS.json": "c6316ecd1e7d82b86784db46da96259b224205571b6dd10bd68e9cf3eb1f0113", + "CLAIM.json": "89bee032c4daf0f814fb14d576503c7fa4f57c0243dbdef1c03c3556a987649f" + } +} diff --git a/research/clean-residual-dilation/verify.py b/research/clean-residual-dilation/verify.py new file mode 100644 index 0000000000..36d0561978 --- /dev/null +++ b/research/clean-residual-dilation/verify.py @@ -0,0 +1,354 @@ +#!/usr/bin/env python3 +"""Exact spectral split-residual diagnostic; Python standard library only. + +Douglas R. Colkitt with substantial OpenAI Codex assistance. Apache-2.0. +No supplier imports, floating arithmetic, or assertions disabled by -O. +""" + +import argparse +from dataclasses import dataclass +from fractions import Fraction +import hashlib +import json +from math import comb +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + return hashlib.sha256(json.dumps(value, separators=(",", ":")).encode()).hexdigest() + + +def multiplicities(width, ambient): + """Binomial eigenvalue counts of C_width on 2**ambient coefficients.""" + require(0 <= width <= ambient, "invalid width") + return [sum(comb(width, k) for k in range(j, width + 1, 4)) + << (ambient - width) for j in range(4)] + + +def multiplicities_dp(width): + counts = [1, 0, 0, 0] + for _ in range(width): + counts = [counts[j] + counts[(j - 1) % 4] for j in range(4)] + return counts + + +def make_route(a, b): + """Full permutation: source eigenvectors first, scratch in unused slots.""" + r = a + b + n = 1 << r + phases = [(i & ((1 << a) - 1)).bit_count() % 4 for i in range(n)] + phases += [(i & ((1 << b) - 1)).bit_count() % 4 for i in range(n)] + bins = [[i for i, p in enumerate(phases) if p == j] for j in range(4)] + need = multiplicities(r, r) + require(all(len(bins[j]) >= need[j] for j in range(4)), + "insufficient eigenspace capacity") + used = [0] * 4 + route = [] + for x in range(n): + j = x.bit_count() % 4 + route.append(bins[j][used[j]]) + used[j] += 1 + occupied = set(route) + route += [i for i in range(2 * n) if i not in occupied] + check_route(route, phases, r) + return route, phases + + +def check_route(route, phases, r): + n = 1 << r + require(len(route) == 2 * n and sorted(route) == list(range(2 * n)), + "route is not a permutation") + require(all(phases[route[x]] == x.bit_count() % 4 for x in range(n)), + "route mismatches a source eigenvalue") + + +@dataclass +class Vector: + """(real + i*imag) / 2**shift, with unbounded exact integer numerators.""" + + real: list + imag: list + shift: int = 0 + + +def zero(n): + return Vector([0] * n, [0] * n) + + +def basis(n, column): + v = zero(n) + v.real[column] = 1 + return v + + +def equal(x, y): + shift = max(x.shift, y.shift) + return (len(x.real) == len(y.real) + and all((a << (shift - x.shift)) == (b << (shift - y.shift)) + for a, b in zip(x.real + x.imag, y.real + y.imag))) + + +def walsh(v, width, inverse=False): + re, im = v.real.copy(), v.imag.copy() + for axis in range(width): + bit = 1 << axis + for block in range(0, len(re), 2 * bit): + for i in range(block, block + bit): + j = i + bit + re[i], re[j] = re[i] + re[j], re[i] - re[j] + im[i], im[j] = im[i] + im[j], im[i] - im[j] + return Vector(re, im, v.shift + (width if inverse else 0)) + + +def kernel(v, width): + """Butterfly evaluation with C = ((1+i,1-i),(1-i,1+i))/2.""" + re, im = v.real.copy(), v.imag.copy() + for axis in range(width): + bit = 1 << axis + for block in range(0, len(re), 2 * bit): + for i in range(block, block + bit): + j = i + bit + sr, si = re[i] + re[j], im[i] + im[j] + dr, di = re[i] - re[j], im[i] - im[j] + re[i], im[i], re[j], im[j] = sr - di, si + dr, sr + di, si - dr + return Vector(re, im, v.shift + width) + + +def mul(z, w): + return z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0] + + +def power(z, exponent): + out = (1, 0) + for _ in range(exponent): + out = mul(out, z) + return out + + +def reference_column(width, column): + """Independent Kronecker entry formula; no butterfly or encoder calls.""" + n = 1 << width + entries = [mul(power((1, 1), width - d), power((1, -1), d)) + for d in range(width + 1)] + vals = [entries[(x ^ column).bit_count()] for x in range(n)] + return Vector([z[0] for z in vals], [z[1] for z in vals], width) + + +def join(x, y): + shift = max(x.shift, y.shift) + re = [a << (shift - x.shift) for a in x.real] + im = [a << (shift - x.shift) for a in x.imag] + re += [a << (shift - y.shift) for a in y.real] + im += [a << (shift - y.shift) for a in y.imag] + return Vector(re, im, shift) + + +def split(v): + n = len(v.real) // 2 + return (Vector(v.real[:n], v.imag[:n], v.shift), + Vector(v.real[n:], v.imag[n:], v.shift)) + + +def permute(v, route, inverse=False): + if inverse: + return Vector([v.real[i] for i in route], [v.imag[i] for i in route], v.shift) + re, im = [0] * len(route), [0] * len(route) + for source, target in enumerate(route): + re[target], im[target] = v.real[source], v.imag[source] + return Vector(re, im, v.shift) + + +def phase(v, exponents): + units = [(1, 0), (0, 1), (-1, 0), (0, -1)] + out = [mul((x, y), units[k % 4]) for x, y, k in zip(v.real, v.imag, exponents)] + return Vector([z[0] for z in out], [z[1] for z in out], v.shift) + + +def walsh_by_child(v, width, inverse=False): + """Check the paid reduction H_k=(1-i)^k S_k C_k S_k independently.""" + exponents = [(i & ((1 << width) - 1)).bit_count() for i in range(len(v.real))] + out = phase(kernel(phase(v, exponents), width), exponents) + factor = power((1, -1), width) + values = [mul((x, y), factor) for x, y in zip(out.real, out.imag)] + return Vector([z[0] for z in values], [z[1] for z in values], + out.shift + (width if inverse else 0)) + + +def collapsed_program(h, z, route, phases, width): + """Cancel both host sandwiches into phases; keep the source boundaries.""" + v = permute(join(walsh(h, width), z), route) + v = phase(v, phases) + u, v = split(permute(v, route, True)) + return walsh(u, width, True), phase(v, [-phases[i] for i in route[len(h.real):]]) + + +def program(h, z, a, b, route, phases, repair=True, omit=None): + """E^-1 (C_a direct-sum C_b) E, followed by the dirty phase repair.""" + r = a + b + source = h if omit == "source_boundaries" else walsh(h, r) + x, y = split(permute(join(source, z), route)) + if omit != "host_entry": + x, y = walsh(x, a, True), walsh(y, b, True) + if omit != "host_calls": + x, y = kernel(x, a), kernel(y, b) + x, y = walsh(x, a), walsh(y, b) + u, v = split(permute(join(x, y), route, True)) + if omit != "source_boundaries": + u = walsh(u, r, inverse=(omit != "normalization")) + if repair: + direction = 1 if omit == "repair_sign" else -1 + v = phase(v, [direction * phases[i] for i in route[len(h.real):]]) + return u, v + + +def verify_pins(): + pins = json.loads((HERE / "SOURCE-PINS.json").read_text()) + for path, expected in pins["local_sha256"].items(): + require(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "source pin mismatch: " + path) + return pins["base_commit"] + + +def audit(): + base = verify_pins() + a, b = 4, 5 + r, n = a + b, 1 << (a + b) + route, phases = make_route(a, b) + source_counts = multiplicities(r, r) + host_counts = [multiplicities(a, r)[j] + multiplicities(b, r)[j] + for j in range(4)] + complement = [host_counts[j] - source_counts[j] for j in range(4)] + require([sum(phases[i] == j for i in route[n:]) for j in range(4)] == complement, + "complement multiplicity mismatch") + + # Independent arithmetic checks and finite support for the all-f proof. + for width in range(289): + require(multiplicities(width, width) == multiplicities_dp(width), + "binomial/DP eigenvalue disagreement") + dilations = [] + for f in range(1, 33): + source = multiplicities(9 * f, 9 * f) + hosts = [multiplicities(4 * f, 9 * f)[j] + multiplicities(5 * f, 9 * f)[j] + for j in range(4)] + require(all(hosts[j] >= source[j] for j in range(4)), "dilation capacity") + require(min(Fraction(hosts[j] - source[j], 1 << (9 * f)) + for j in range(4)) >= Fraction(3, 64), "uniform slack") + dilations.append({"f": f, "source": source, "hosts": hosts}) + + z = zero(n) + # All complex-linear basis columns, with independent dense tensor entries. + for column in range(n): + h = basis(n, column) + expected = reference_column(r, column) + require(equal(kernel(h, r), expected), "kernel/reference mismatch") + for inverse in (False, True): + require(equal(walsh(h, r, inverse), walsh_by_child(h, r, inverse)), + "Walsh one-child invoice identity") + u, v = program(h, z, a, b, route, phases, repair=False) + require(equal(u, expected) and equal(v, z), "clean dilation identity") + u, v = collapsed_program(h, z, route, phases, r) + require(equal(u, expected) and equal(v, z), "collapsed clean identity") + for column in range(n): + scratch = basis(n, column) + u, v = program(z, scratch, a, b, route, phases, repair=False) + wanted = phase(scratch, [phases[i] for i in route[n:]]) + require(equal(u, z) and equal(v, wanted), "dirty complement identity") + u, v = program(z, scratch, a, b, route, phases) + require(equal(u, z) and equal(v, scratch), "dirty restoration identity") + u, v = collapsed_program(z, scratch, route, phases, r) + require(equal(u, z) and equal(v, scratch), "collapsed dirty identity") + + controls = {} + try: + make_route(1, 1) + except ValueError as exc: + require(str(exc) == "insufficient eigenspace capacity", "wrong capacity failure") + controls["rank_two_into_two_rank_one_owners"] = "REJECTED: missing -1 eigenspace" + require(len(controls) == 1, "infeasible embedding accepted") + bad = route.copy() + bad[0], bad[1] = bad[1], bad[0] + try: + check_route(bad, phases, r) + except ValueError as exc: + require(str(exc) == "route mismatches a source eigenvalue", "wrong route failure") + controls["wrong_eigenvalue_route"] = "REJECTED" + require(len(controls) == 2, "bad route accepted") + h = basis(n, 0) + expected = reference_column(r, 0) + for omission in ["source_boundaries", "host_entry", "host_calls", "normalization"]: + u, v = program(h, z, a, b, route, phases, omit=omission) + require(not (equal(u, expected) and equal(v, z)), "mutation survived: " + omission) + controls["omit_" + omission] = "REJECTED on source basis column 0" + j = next(j for j, slot in enumerate(route[n:]) if phases[slot] % 2 == 1) + dirty = basis(n, j) + for name, repair, omission in [("unrestored_dirty_workspace", False, None), + ("wrong_dirty_repair_sign", True, "repair_sign")]: + u, v = program(z, dirty, a, b, route, phases, repair=repair, omit=omission) + require(not equal(v, dirty), "dirty mutation survived") + controls[name] = {"status": "REJECTED", "scratch_basis_column": j, + "unrepaired_phase_exponent": phases[route[n + j]]} + + # At sigma=1 rank mass is already larger. For 0= 5 (>= 4 with free hosts; 2 after host collapse).") + + +if __name__ == "__main__": + main()