diff --git a/research/triangular-parity-forward-bound/README.md b/research/triangular-parity-forward-bound/README.md new file mode 100644 index 0000000000..d008710585 --- /dev/null +++ b/research/triangular-parity-forward-bound/README.md @@ -0,0 +1,187 @@ +# Sharp forward macro-prefix bound for triangular parity recursion + +For every dyadic size, the exact lower unit triangular Toeplitz parity compiler +has **every forward macro-prefix bounded by `1+η` in infinity norm**, provided +the symbol tail has coefficient l1 norm at most `0 ≤ η ≤ 1`. The bound covers +all legal interleavings of the two disjoint children and is sharp even at a +proper prefix. In particular, the half-tail forward-only bound is **3/2**. + +This resolves the remaining forward-only question in +[Discussion #4715](https://github.com/CrocSwap/integer-mult-bounds/discussions/4715#discussioncomment-19130279). +[PR #4731](https://github.com/CrocSwap/integer-mult-bounds/pull/4731), exact head +`3fcaa4d4c0568ce474c593d0882296ff43d3705a`, already proves the common four-cut +bound `1/(1−η)` for `η<1`; its half-tail bound 2 remains sharp for inverse +operators. The present proof uses the correlation between a forward prefix and +its inverse suffix instead of bounding both separately. It does not require +or copy code from that pending package. + +## Quantified proposition and schedule + +Let `N=2^d`, `d≥0`, and `f=(1,f_1,...,f_(N−1))` have real or complex entries +with `Σ_(j≥1)|f_j| ≤ η ≤ 1`. Write `T=T_N(f)`. A **macro** is one completed +right or left Toeplitz shear in the exact parity recursion of +[`SHALLOW-TOEPLITZ.md` §3](../unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md). +Within every node the right shear runs first, both child recursions run next +on disjoint coordinates in any interleaving preserving each child's order, +and the left shear runs after both finish. Include the empty and completed +prefixes. No cut inside a shear is included. + +For a cut let `P` be its forward prefix, and `Q` its remaining suffix, so +`T=QP`. Define **`R=P T^(-1)=Q^(-1)`**, with this multiplication direction. +Then + +``` +||P||_infinity ≤ 1+η. +``` + +The theorem is about the restored logical-coordinate basis. A physical wire +permutation at a cut only left-multiplies the prefix by a norm-one permutation, +so the same norm bound holds during those reorderings. Literal support and +unit-diagonal assertions below are used only after restoring logical indices. +Simultaneous completed macros on disjoint subtrees may be serialized in either +order; thus their layer boundaries are included as well. + +## Proof: disjoint supports retain the lost correlation + +First prove an algebraic invariant **without any small-tail hypothesis**: +`P` and `R` have unit diagonal, and `H=P−I` and `G=R−I` have disjoint supports +entrywise. For the one-wire leaf both matrices are the identity. At any node +write `f(z)=e(z²)+z o(z²)`, and, modulo `z^(N/2)`, put + +``` +k=o/e, s=e−z o²/e, +E=T(e), S=T(s), K=T(k), +U=[ I ZK ; 0 I ], L=[ I 0 ; K I ], +T=L diag(E,S) U. +``` + +Every child symbol has constant term 1; all finite triangular inverses exist, +including when the original tail is 1. Work temporarily in even/odd block +order. Between the completed `U` and the final `L`, let `P_e,P_s` be arbitrary +legal prefixes of the children, with `R_e=P_e E^(-1)` and +`R_s=P_s S^(-1)`. Exact multiplication gives + +``` +P = diag(P_e,P_s) U = [ P_e P_e ZK ; 0 P_s ], +R = P T^(-1) = diag(R_e,R_s) L^(-1) + = [ R_e 0 ; −R_s K R_s ]. +``` + +The two off-diagonal blocks occupy opposite positions. In the diagonal blocks, +the child induction gives disjointness of `P_child−I` and `R_child−I`, and +unit diagonals. Thus the invariant holds for every pair of child cuts, +including either child empty or completed. Before `U`, `P=I`; after the +completed `L`, `P=T` and `R=I`. These endpoints also satisfy the invariant. +This covers all cuts and arbitrary legal interleavings. Simultaneous conjugation +by the parity permutation preserves supports and the diagonal, so induction +returns to the original logical basis. + +Now set `F=T−I`, so `||F||_infinity ≤ η`, and use `P=RT`: + +``` +H−G = P−R = R(T−I) = (I+G)F. +``` + +For row `i` put `h_i=Σ_j|H_ij|` and `g_i=Σ_j|G_ij|`. Disjoint supports and +zero diagonal give the exact equalities `||H_i−G_i||_1=h_i+g_i` and +`||R_i||_1=1+g_i`. Therefore + +``` +h_i+g_i ≤ η(1+g_i), +h_i+(1−η)g_i ≤ η. +``` + +Since `0≤η≤1`, this implies `h_i≤η`. The unit diagonal of `P` now yields +`||P||_infinity=max_i(1+h_i)≤1+η`. Absolute values suffice throughout, so +complex coefficients cause no change. No Neumann inverse bound is used. + +## Sharpness, the edge η=1, and a domain control + +At `N=4`, `f=(1,η,0,0)` has a proper root-`U` prefix with infinity norm +exactly `1+η`. The bound is therefore optimal even without the final endpoint. +At `η=1`, the same proof gives 2. This does **not** bound inverse suffixes +uniformly at that edge: for `f=1−z`, the empty prefix has `R=T^(-1)` with +infinity norm `N`. + +The restriction on η matters. At `N=8`, `f=(1,1,1,0,0,0,0,0)` has tail 2, +`e=1+z`, `o=1`, and `k=1−z+z²−z³`; the proper root-`U` prefix has norm 4, +which exceeds `1+η=3`. This is a domain control, not a classification for every +η above 1. + +## Scope, family status, and overlap + +This is a local quantified precision audit. It closes a sharp **forward macro** +lemma, not a missing general polynomial stability theorem: the retained source +already states polynomial bounds for internal gates and composed circuits. +The proof does not establish sharper bounds inside FFT/circulant/negacyclic +shears, rounding, generator preparation, Gaussian normalization, fixed-tape +bit costs or a full multiplication theorem. The selected conditional frontier +and supplier admission are unchanged. No new mechanism expansion is proposed. + +The original `uniform-transfer-audit` card and refinement to `η≤1` are recorded +in [TASK.json](TASK.json). Family coverage before this contribution was: + +| Obligation | Status and distinct contribution | +| --- | --- | +| One-level parity tail budget | James Reed's [#4699](https://github.com/CrocSwap/integer-mult-bounds/pull/4699), head `67c70cc7d190fc4f728292d8f384c13f26f90385`; already covered. | +| Individual four/eight-wire prefix symbols | [#4701–#4706](https://github.com/CrocSwap/integer-mult-bounds/pull/4706); finite examples, not repeated as the result. | +| All-depth common four-cut bound | #4731 at the exact head above; already covered, including child interleavings. | +| All-depth forward-only sharp bound | This proof: disjoint support, row tradeoff, and `1+η` through η=1. | +| Internal gates, complete Gaussian/physical accounting | Separate obligations, not discharged here. | + +Before the claim, offline `find_overlap.py` inspected the full shared snapshot +of 498 open PRs (2026-10-22 18:24:36 UTC), 3641 Discussion records +(18:25:24 UTC), and all 5860 tracked local package notes, with no local omissions. +The card search and terms `forward-prefix-only`, `triangular-parity`, `1+eta` +found the predecessor thread and finite lineage; no competing general proof +was found. Cache coverage is not proof of novelty and does not include arbitrary +unpublished work or every PR diff. + +## Reproduce and evidence limits + +From the repository root, using Python 3.12 (standard library only): + +```sh +python3 scripts/research_package.py --package research/triangular-parity-forward-bound --check-only +python3.12 scripts/research_package.py --package research/triangular-parity-forward-bound +``` + +The registered normal and optimized runs use explicit checks that survive `-O`. +The checker enumerates order ideals of the macro dependency DAG, compares +matrices reached by different interleavings, and checks endpoints, both inverse +identities, unit diagonals, disjoint support, the exact row identity and its +tradeoff. Seven rational fixtures of sizes 1, 2, 4, 8 include signed tails, +η=1, proper-prefix sharpness, and all 123 eight-wire DAG cuts. Five negative +controls reject a non-macro midpoint, non-dyadic size, non-unit symbol, +wrong final-shear sign, and applying the theorem beyond η=1. The last control +also checks the exact norm-4 witness above. + +These finite controls support implementation review; the preceding induction +is the all-size proof. They are not exhaustive coefficient search, a formal +proof, independent human acceptance, or full historical/native/Lean/Docker +replay. [SOURCES.json](SOURCES.json) pins retained inputs and provenance at +canonical base `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. + +## Open next questions + +The structured question in [TASK.json](TASK.json) is whether one concrete +retained internal shear implementation has the gate-cut precision accounting +required by the Gaussian caller. Start with a specified section-2 gate cut and +its caller norms, after a separate overlap/claim check. The support invariant +need not hold inside a shear, so this theorem cannot be substituted for that +work. No further minor macro-bound construction round is requested. + +## Credit + +Prepared for Brian with substantial OpenAI Codex assistance in proof discovery, +implementation and independent AI proof review; no human review acceptance is +claimed. Apache-2.0. The parity compiler is retained from Vlado Vojdanovski's +[#1673](https://github.com/CrocSwap/integer-mult-bounds/pull/1673), used by Cinna +Davis's [#4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) Gaussian +caller. The forward-only question follows Ryanson Jonathan (`one-factor-of-t`), +unpaidmoon/#4371, James Reed's one-level and finite lineage, and #4731. +The checker reuses only the pure `identity`, `multiply`, and `toeplitz` helpers +from [q-toeplitz-factorization](../q-toeplitz-factorization/README.md), whose +retained factorization credits Chafik Boukhalfa/#489, Alexey Kuznetsov, and Jose +Manuel (`jmbarrancoml`)/#3851. Its historical selected-result check and main +program are not invoked. diff --git a/research/triangular-parity-forward-bound/SOURCES.json b/research/triangular-parity-forward-bound/SOURCES.json new file mode 100644 index 0000000000..a258c55cf6 --- /dev/null +++ b/research/triangular-parity-forward-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/q-toeplitz-factorization/verify.py", + "usage": "input", + "git_blob": "fefc8f9d86556269fd7a60494f7f3626563b9192", + "sha256": "9fd54cfb1dbb4d6d2f73b699a7108ca265c35a7e222a419c7586b4a057a1f575" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md", + "usage": "input", + "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be", + "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310" + } + ] +} diff --git a/research/triangular-parity-forward-bound/TASK.json b/research/triangular-parity-forward-bound/TASK.json new file mode 100644 index 0000000000..19b1ffcb4c --- /dev/null +++ b/research/triangular-parity-forward-bound/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "refined", + "actual_scope": "Prove the sharp forward-only macro-prefix bound ||P||_infinity <= 1+eta for every dyadic lower unit triangular Toeplitz parity compiler, every legal interleaving, and 0 <= eta <= 1.", + "scope_change_reason": "Handoff #4715 and PR #4731 leave forward-only 3/2 open after establishing a common four-cut bound of 2. The disjoint-support invariant closes that question and also permits eta=1, beyond the initial claim eta<1. This is one quantified precision lemma, not a new construction round.", + "bottleneck_link": "This removes a forward macro-prefix norm gap in the retained #4100 Gaussian triangular caller. It does not bound cuts inside shear implementations, rounding or total physical costs, and makes no selected-frontier change.", + "budget_minutes": 60, + "stop_rule": "Stop after a complete proof or exact counterexample for this single forward-only obligation, then bounded exact replay and review. No extension into internal gate costs or full Gaussian admission.", + "outcome": "completed", + "evidence": "README.md gives the quantified proof and family boundary; verify.py checks all DAG ideals for seven rational fixtures of sizes 1,2,4,8, eta=1 edges, sharp proper prefixes and five negative controls.", + "author": "Brian, with substantial OpenAI Codex assistance", + "ai_assistance": "Prepared for Brian with substantial OpenAI Codex assistance in proof discovery, implementation, source/overlap audit and an independent AI proof review; no independent human acceptance or formal proof claimed.", + "open_questions": [ + { + "question": "Can the retained implementation bound actual cuts inside the right and left Toeplitz shear macros with the precision accounting required by the Gaussian caller?", + "why_it_matters": "The theorem covers atomic completed shears only; the source already states polynomial internal-gate bounds, but this sharper macro lemma does not provide or independently audit their constants and composition.", + "first_step": "Select one retained section-2 circulant/negacyclic shear implementation and specify an exact internal gate cut and its caller norms before attempting a new bound.", + "blocked_by": "A source-specific gate-level accounting obligation and separate overlap/claim check; the present macro support invariant need not hold inside a shear." + } + ] +} diff --git a/research/triangular-parity-forward-bound/VERIFY.json b/research/triangular-parity-forward-bound/VERIFY.json new file mode 100644 index 0000000000..0735284039 --- /dev/null +++ b/research/triangular-parity-forward-bound/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/q-toeplitz-factorization/verify.py", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact DAG ideals, correlated row-support identity, row tradeoff and endpoint; sharp proper prefixes, eta=1, five rejection/counterexample controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same explicit checks with Python assertions disabled." + } + ] +} diff --git a/research/triangular-parity-forward-bound/verify.py b/research/triangular-parity-forward-bound/verify.py new file mode 100644 index 0000000000..98c9f8e565 --- /dev/null +++ b/research/triangular-parity-forward-bound/verify.py @@ -0,0 +1,187 @@ +"""Exact DAG-cut controls for the forward macro-prefix proof; no all-size enumeration.""" +from __future__ import annotations + +import importlib.util +import json +from fractions import Fraction as F +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +SPEC = importlib.util.spec_from_file_location( + "retained_matrix_helpers", ROOT / "research/q-toeplitz-factorization/verify.py" +) +if SPEC is None or SPEC.loader is None: + raise RuntimeError("cannot load retained matrix helpers") +HELPERS = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(HELPERS) +eye, mul, toeplitz = HELPERS.identity, HELPERS.multiply, HELPERS.toeplitz + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def norm(a): + return max(sum(map(abs, row)) for row in a) + + +def divide(a, b): + need(b[0] == 1, "unit denominator required") + q = [] + for i, value in enumerate(a): + q.append(value - sum(b[j] * q[i-j] for j in range(1, i+1))) + return q + + +def inverse(a): + n = len(a) + need(all(a[i][i] == 1 and all(a[i][j] == 0 for j in range(i+1, n)) + for i in range(n)), "unit lower triangular matrix required") + b = eye(n) + for i in range(n): + for j in range(i): + b[i][j] = -sum(a[i][k] * b[k][j] for k in range(j, i)) + need(mul(a, b) == mul(b, a) == eye(n), "two-sided inverse") + return b + + +def events(f, indices, after=(), path=""): + """Parent U precedes both children; parent L follows both completions.""" + n = len(f) + need(n > 0 and n & (n-1) == 0 and f[0] == 1, "unit dyadic symbol required") + if n == 1: + return [], after + m = n // 2 + e, o = f[::2], f[1::2] + k = divide(o, e) + s = e.copy() + for i in range(1, m): + s[i] -= sum(o[j] * k[i-1-j] for j in range(i)) + ev, od = indices[::2], indices[1::2] + u, l = path + "U", path + "L" + upper = (u, after, [(ev[i], od[j], k[i-j-1]) + for i in range(m) for j in range(i)]) + a, da = events(e, ev, (u,), path+"E") + b, db = events(s, od, (u,), path+"S") + lower = (l, tuple(sorted(set(da+db))), [(od[i], ev[j], k[i-j]) + for i in range(m) for j in range(i+1)]) + return [upper] + a + b + [lower], (l,) + + +def apply(p, event): + # Every source row is read before this atomic shear macro is applied. + out = [row.copy() for row in p] + for i, j, coefficient in event[2]: + for col in range(len(p)): + out[i][col] += coefficient * p[j][col] + return out + + +def cut_check(p, t, ti, eta): + n = len(t) + r = mul(p, ti) # Inverse suffix; the multiplication direction matters. + need(mul(r, t) == p, "R T = P") + for i in range(n): + need(p[i][i] == r[i][i] == 1, "unit diagonal") + h = [p[i][j] - int(i == j) for j in range(n)] + g = [r[i][j] - int(i == j) for j in range(n)] + need(all(x == 0 or y == 0 for x, y in zip(h, g)), "disjoint supports") + hs, gs = sum(map(abs, h)), sum(map(abs, g)) + difference = [h[j]-g[j] for j in range(n)] + product = [sum(r[i][k] * (t[k][j]-int(k == j)) + for k in range(n)) for j in range(n)] + need(difference == product, "H-G = R(T-I)") + need(sum(map(abs, difference)) == hs+gs, "disjoint row equality") + need(hs + (1-eta)*gs <= eta, "row tradeoff") + need(norm(p) <= 1+eta, "forward bound") + return norm(r) + + +def replay(f): + eta = sum(map(abs, f[1:])) + need(eta <= 1, "the forward theorem requires eta <= 1") + t, ti = toeplitz(f), inverse(toeplitz(f)) + es, _ = events(f, list(range(len(f)))) + start = frozenset() + states = {start: eye(len(f))} + todo = [start] + max_p, max_r = F(0), F(0) + while todo: + done = todo.pop() + p = states[done] + max_r = max(max_r, cut_check(p, t, ti, eta)) + max_p = max(max_p, norm(p)) + for event in es: + name, deps, _ = event + if name in done or not set(deps) <= done: + continue + nxt, matrix = done | {name}, apply(p, event) + if nxt in states: + need(states[nxt] == matrix, "interleaving commutation") + else: + states[nxt] = matrix + todo.append(nxt) + complete = frozenset(event[0] for event in es) + need(states[complete] == t, "compiler endpoint") + return {"n": len(f), "eta": str(eta), "dag_cuts": len(states), + "max_P": str(max_p), "max_inverse_suffix": str(max_r)} + + +def rejected(call, message): + try: + call() + except ValueError as exc: + need(message in str(exc), "wrong rejection: " + str(exc)) + else: + raise ValueError("missing rejection: " + message) + + +def main(): + fixtures = [ + ("identity", [1]), + ("two_wires", [1, F(-1, 2)]), + ("proper_sharp_half", [1, F(1, 2), 0, 0]), + ("mixed_half", [1, F(1, 4), F(1, 8), F(1, 8), 0, 0, 0, 0]), + ("signed_three_quarters", [1, F(1, 8), F(-1, 8), F(1, 8), + F(-1, 8), F(1, 8), F(-1, 8), 0]), + ("eta_one_geometric", [1, -1, 0, 0, 0, 0, 0, 0]), + ("eta_one_mixed", [1, F(1, 2), F(-1, 4), F(1, 4), 0, 0, 0, 0]), + ] + results = {name: replay(list(map(F, f))) for name, f in fixtures} + need(results["mixed_half"]["dag_cuts"] == 123, "eight-wire DAG inventory") + need(results["eta_one_geometric"]["max_P"] == "2", "eta-one forward edge") + need(results["eta_one_geometric"]["max_inverse_suffix"] == "8", "eta-one inverse grows") + for eta in (F(1, 2), F(1)): + es, _ = events([F(1), eta, F(0), F(0)], list(range(4))) + need(norm(apply(eye(4), es[0])) == 1+eta, "proper prefix sharpness") + + # Non-macro midpoint fails the stronger support invariant even at eta=1/2. + t = toeplitz([F(1), F(1, 2)]) + midpoint = eye(2) + midpoint[1][0] = F(1, 4) + rejected(lambda: cut_check(midpoint, t, inverse(t), F(1, 2)), "disjoint supports") + rejected(lambda: events([F(1)]*3, list(range(3))), "unit dyadic") + rejected(lambda: events([F(2), F(0)], list(range(2))), "unit dyadic") + + # Changing a nonzero final left-shear sign must break the exact endpoint. + f = list(map(F, [1, F(1, 4), F(1, 8), F(1, 8), 0, 0, 0, 0])) + es, _ = events(f, list(range(8))) + name, deps, adds = es[-1] + es[-1] = (name, deps, [(i, j, -c) for i, j, c in adds]) + p = eye(8) + for event in es: + p = apply(p, event) + rejected(lambda: need(p == toeplitz(f), "compiler endpoint"), "compiler endpoint") + + # The eta <= 1 guard is real: a proper root-U prefix at eta=2 has norm 4 > 3. + outside = list(map(F, [1, 1, 1, 0, 0, 0, 0, 0])) + es, _ = events(outside, list(range(8))) + need(norm(apply(eye(8), es[0])) == 4, "outside-domain counterexample") + rejected(lambda: replay(outside), "eta <= 1") + print(json.dumps(results, sort_keys=True)) + print("PASS_PARITY_FORWARD_BOUND exact_DAG_controls=7 negative_controls=5 no_new_kappa") + + +if __name__ == "__main__": + main()