From 3f8fc3482ebed70149996a502a839b13ec91bfcf Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 22:16:11 +0100 Subject: [PATCH] feat(research): prove the sharp parity-prefix tail threshold --- .../README.md | 177 ++++++++++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 80 ++++++++ .../VERIFY.json | 32 ++++ .../verify.py | 165 ++++++++++++++++ 5 files changed, 484 insertions(+) create mode 100644 research/triangular-parity-tail-threshold/README.md create mode 100644 research/triangular-parity-tail-threshold/SOURCES.json create mode 100644 research/triangular-parity-tail-threshold/TASK.json create mode 100644 research/triangular-parity-tail-threshold/VERIFY.json create mode 100644 research/triangular-parity-tail-threshold/verify.py diff --git a/research/triangular-parity-tail-threshold/README.md b/research/triangular-parity-tail-threshold/README.md new file mode 100644 index 0000000000..0930356395 --- /dev/null +++ b/research/triangular-parity-tail-threshold/README.md @@ -0,0 +1,177 @@ +# The sharp tail threshold for forward parity prefixes + +For every fixed real `eta > 1`, the exact triangular Toeplitz parity compiler +has a family whose completed map has infinity norm `1+eta`, but whose first +proper macro-prefix has norm + +```text +((eta+1)/2)^(N/2-1), N = 4,8,16,... . +``` + +This is a **scoped algebraic proof with finite controls**. It rules out even a +polynomial-in-`N` forward-prefix bound based only on a fixed coefficient-tail +budget greater than one. Together with Brian's +[#4737](https://github.com/CrocSwap/integer-mult-bounds/pull/4737) theorem for +`eta <= 1`, it identifies one as the exact threshold for a dimension-independent +forward macro-prefix bound over the complete tail-budget class. The new part is +the exponential family for every `eta > 1`; the complementary theorem is cited, +not re-proved or replayed. + +## Proposition and proof + +Use the exact parity recursion in +[`SHALLOW-TOEPLITZ.md`, section 3](../unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md). +A macro is a completed Toeplitz shear. At every node the right shear runs first, +the two children run next, and the left shear runs last. The proof only needs +the root right shear, so it applies to every legal child interleaving. + +Fix `eta > 1` and put + +```text +a = (eta+1)/2 > 1, b = (eta-1)/2 = a-1 > 0, +f(z) = 1 + b z + a z^2, N = 2m >= 4. +``` + +Let `T_N(f)` denote multiplication by `f` modulo `z^N` in coefficient order. +Its tail coefficient l1 norm is `a+b=eta`. Every row has absolute sum at most +`1+a+b`, and every row with index at least two attains it. Thus + +```text +||T_N(f)||_infinity = 1+eta = 2a, +``` + +independently of `N`. In even/odd order the root split has + +```text +e(z) = 1+a z, o(z) = b, +k(z) = o(z)/e(z) = b sum_(j=0)^(m-1) (-a)^j z^j mod z^m, +U = [ I T_m(z k) ; 0 I ]. +``` + +All inverses here are finite triangular inverses, since `e(0)=1`. No analytic +convergence is assumed. The first macro-prefix is exactly `U`. Its upper block +row with within-block index `i` has absolute row sum + +```text +1 + b sum_(j=0)^(i-1) a^j = a^i, 0 <= i < m. +``` + +For `i=0` the sum is empty. The largest row is `i=m-1`, so + +```text +||U||_infinity = a^(m-1) = ((eta+1)/2)^(N/2-1). +``` + +The shear is a proper prefix because it precedes the children and the nonzero +root left shear. Coordinate permutation preserves this norm. Also +`U^(-1)=[I -T_m(zk);0 I]`, so the same exact norm holds for its inverse. +The norm is attained on a unit infinity-norm input: choose each input coordinate +to have the sign of its coefficient in the largest row, and zero when that +coefficient vanishes. Thus the growth is an actual amplification of bounded +data, not merely a loose product estimate. + +For fixed `a>1`, the logarithm of the displayed norm is `(N/2-1) log(a)`. +It grows linearly in `N`, whereas the logarithm of any fixed polynomial grows +as `O(log N)`. Therefore no dimension-independent bound, or polynomial bound +with constants depending only on `eta`, can cover every symbol in this class. +This conclusion already holds with three nonzero coefficients and nonnegative +input-symbol coefficients. The proof is valid for every real `eta>1`; the +finite checker uses rational instances only. + +For example, `eta=3` gives `f=1+z+2z^2`. At `N=16` the first prefix has norm +`128`, while the completed map has norm `4`. These are exact values checked +by the verifier. + +## What this changes and what it does not establish + +The completed map's bounded forward norm alone cannot justify increasing the +parity compiler's permitted tail budget beyond one. Any such extension needs +an additional restriction or a changed factorization. Brian's #4737 gives a +single `eta=2` violation of the `1+eta` cap; this result strengthens that domain +observation to exponential growth for every fixed superunit budget. + +The retained triangular caller in `SHALLOW-TOEPLITZ.md` assumes `eta<1`. +Nothing here contradicts that theorem or changes the selected frontier. +This family is not asserted to have uniformly bounded inverse endpoint norm. +The obstruction is specific to the exact parity factorization and its macro +boundaries. It does not exclude other compilers, settle internal FFT or shear +gate accounting, provide a physical supplier, or prove a complete integer +multiplication theorem. No new kappa is claimed. Formal proof-kernel and +independent human review are unclaimed. + +The original `uniform-transfer-audit` card changes to this algebraic domain +side result. The original card, scope reason and remaining obligations are in +[TASK.json](TASK.json). The current selected source-binding orientation passed +with `scripts/research_selected_baseline.py`; the card's older balanced-schema +control is historical. No predecessor executable was replayed. + +## Reproduction and finite evidence + +Run from the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/triangular-parity-tail-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/triangular-parity-tail-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/triangular-parity-tail-threshold/verify.py +``` + +Expected marker: + +```text +PASS_PARITY_TAIL_THRESHOLD fixtures=25 controls=7 max_n=64 no_new_kappa +``` + +The 25 fixtures are the full Cartesian product of tail budgets +`17/16, 5/4, 3/2, 2, 3` and dimensions `4,8,16,32,64`. For every fixture the +checker independently divides the finite series, applies the root right, +diagonal and left factors to every input column, and compares the complete +product with the literal Toeplitz endpoint. It checks both inverse orders for +the first shear, its exact norm, an attaining signed input, the endpoint norm, +and the dyadic growth identity `p_(2N)=a p_N^2` on every adjacent size pair. +Seven controls cover the tail boundary, the finite upper tail limit, +non-dyadic size, size exhaustion, nonunit division, a missing shift and the +wrong Schur sign. These are controls of the new family, not rechecks of a +predecessor's claimed counts. + +Each run prints a generated JSON receipt containing these results and SHA256 +hashes of all five package files. No receipt is hand-authored or committed. +The all-size claim rests on the preceding proof, not these finite samples. +Lean, Docker, internal-gate compilation and the selected full operator replay +are outside scope and unrun. + +The checker has no imports from predecessor code, network calls, subprocesses +or writes. Source documents are pinned as historical provenance in +[SOURCES.json](SOURCES.json). Its loops have fixed finite bounds, with matrices +of at most `64 x 64` and 25 fixed rational fixtures. Functions are under 60 +lines, and explicit contracts remain active under optimization. Python's +managed allocation and arbitrary-precision arithmetic are a Power of Ten +deviation: live dimensions and coefficient inputs are bounded by this fixed +grid. The rejection helper's indirect calls have five explicit local targets. +Warning-strict normal and optimized execution are the available diagnostics. +No standalone linter or type checker is installed in this environment. + +## Open next questions + +- Can a changed factorization retain polynomial forward-prefix norms on a + class with tail budget above one and a separately bounded inverse endpoint? + This would distinguish a compiler limitation from unavoidable conditioning. + Start with a concrete zero-free symbol whose even part has an interior zero, + then price the replacement factorization. Such a class and its inverse bound + have not been constructed here. +- Can a caller normalize a superunit-tail triangular symbol into near-identity + factors without repaying the gain through coefficient generation, storage + or additional shears? Start with one caller's literal symbol and complete + invoice. Caller-specific spectra and implementation costs remain unknown. + +## Credit + +This contribution was produced by Nick Petalas. Apache-2.0. + +Brian's #4737 supplies the complementary forward theorem and the prior +`eta=2` example; #4731 supplies the common four-cut envelope. James Reed's +#4699 and subsequent finite parity-prefix packages supply the one-level +budget and individual examples. The parity compiler is retained from Vlado +Vojdanovski's #1673 and Cinna Davis's #4100 caller. Credit also Ryanson Jonathan +and unpaidmoon #4371 for the preceding conditioning question. The new +contribution is the sparse exponential family and the universal superunit-tail +obstruction. All predecessor files and credit lines are unchanged. diff --git a/research/triangular-parity-tail-threshold/SOURCES.json b/research/triangular-parity-tail-threshold/SOURCES.json new file mode 100644 index 0000000000..ceb95c63a8 --- /dev/null +++ b/research/triangular-parity-tail-threshold/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/triangular-parity-forward-bound/README.md", + "usage": "provenance", + "git_blob": "d008710585a897b9b568e74c7b867d8c784e4aa8", + "sha256": "745c2105fc614e6ba453327a37e483b808425a40ce3e2b44e2643b0ea1db3781" + }, + { + "path": "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md", + "usage": "provenance", + "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be", + "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310" + } + ] +} diff --git a/research/triangular-parity-tail-threshold/TASK.json b/research/triangular-parity-tail-threshold/TASK.json new file mode 100644 index 0000000000..f81cd2fa52 --- /dev/null +++ b/research/triangular-parity-tail-threshold/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "changed", + "actual_scope": "For every real eta>1, prove an exponential first forward macro-prefix in the exact triangular parity compiler, despite a completed forward norm of 1+eta.", + "scope_change_reason": "This is an original algebraic domain side result following Brian #4737, not an audit of the retained eta<1 caller. It isolates the universal forward-prefix threshold, separate from finite half-tail examples and internal gate bounds.", + "bottleneck_link": "Precision side result: bounded completed forward norm cannot alone extend this parity factorization to a superunit coefficient-tail class; a different restriction or factorization is needed.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved original obstruction, with bounded rational controls; do not expand to a replacement compiler.", + "outcome": "negative-result", + "evidence": "README.md contains the all-real-eta proof; verify.py checks 25 exact root factorizations, attaining inputs and seven controls through N=64.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed factorization retain polynomial forward-prefix norms above tail one when the inverse endpoint is separately bounded?", + "why_it_matters": "This separates avoidable compiler amplification from unavoidable inverse conditioning.", + "first_step": "Construct one explicit zero-free symbol whose even part has an interior zero, then specify the replacement factorization.", + "blocked_by": "No such symbol class with a uniform inverse bound or replacement invoice is supplied here." + }, + { + "question": "Can a concrete caller normalize a superunit-tail triangular symbol into near-identity factors within its paid budget?", + "why_it_matters": "A normalization might avoid the obstruction, but additional shears and coefficient preparation can repay its gain.", + "first_step": "Use one literal caller symbol and price coefficient generation, storage and every additional factor.", + "blocked_by": "Caller-specific spectra and complete implementation costs remain unknown." + } + ] +} diff --git a/research/triangular-parity-tail-threshold/VERIFY.json b/research/triangular-parity-tail-threshold/VERIFY.json new file mode 100644 index 0000000000..7bfb3ec3c4 --- /dev/null +++ b/research/triangular-parity-tail-threshold/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact 25-fixture root factorization, norm, attaining-input and growth-recurrence controls, plus seven domain/algebra controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same complete finite domain under optimization; every explicit contract must remain active." + } + ] +} diff --git a/research/triangular-parity-tail-threshold/verify.py b/research/triangular-parity-tail-threshold/verify.py new file mode 100644 index 0000000000..2b3fce64de --- /dev/null +++ b/research/triangular-parity-tail-threshold/verify.py @@ -0,0 +1,165 @@ +"""Exact finite controls for the separately proved superunit-tail obstruction.""" +from __future__ import annotations + +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path + +MAX_N = 64 +ETAS = (Q(17, 16), Q(5, 4), Q(3, 2), Q(2), Q(3)) +SIZES = (4, 8, 16, 32, 64) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def parameters(eta: Q, n: int) -> tuple[Q, Q]: + need(Q(1) < eta <= Q(3), "finite checker requires 1 < eta <= 3") + need(4 <= n <= MAX_N and n & (n - 1) == 0, "dyadic size in [4, 64]") + a = (eta + 1) / 2 + b = (eta - 1) / 2 + need(a > 1 and b == a - 1 and a + b == eta, "parameter identities") + return a, b + + +def identity(n: int) -> list[list[Q]]: + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def toeplitz(symbol: list[Q]) -> list[list[Q]]: + n = len(symbol) + return [[symbol[i - j] if i >= j else Q(0) + for j in range(n)] for i in range(n)] + + +def norm(matrix: list[list[Q]]) -> Q: + return max(sum(map(abs, row)) for row in matrix) + + +def quotient(numerator: list[Q], denominator: list[Q]) -> list[Q]: + need(len(numerator) == len(denominator) <= MAX_N, "division lengths") + need(denominator[0] == 1, "unit denominator") + out = [Q(0)] * len(numerator) + for i, value in enumerate(numerator): + out[i] = value - sum(denominator[j] * out[i - j] + for j in range(1, i + 1)) + return out + + +def shear(matrix: list[list[Q]], k: list[Q], upper: bool) -> list[list[Q]]: + n, m = len(matrix), len(k) + need(n == 2 * m <= MAX_N, "shear dimensions") + out = [row.copy() for row in matrix] + for i in range(m): + for j in range(i if upper else i + 1): + target = 2 * i if upper else 2 * i + 1 + source = 2 * j + 1 if upper else 2 * j + coefficient = k[i - j - 1] if upper else k[i - j] + for col in range(n): + out[target][col] += coefficient * matrix[source][col] + return out + + +def middle(matrix: list[list[Q]], e: list[Q], s: list[Q]) -> list[list[Q]]: + n, m = len(matrix), len(e) + out = [[Q(0)] * n for _ in range(n)] + for parity, symbol in enumerate((e, s)): + for i in range(m): + for j in range(i + 1): + for col in range(n): + out[2 * i + parity][col] += ( + symbol[i - j] * matrix[2 * j + parity][col]) + return out + + +def one_case(eta: Q, n: int) -> dict[str, str | int]: + a, b = parameters(eta, n) + m = n // 2 + f = [Q(1), b, a] + [Q(0)] * (n - 3) + e, o = f[::2], f[1::2] + k = quotient(o, e) + need(k == [b * (-a) ** j for j in range(m)], "geometric quotient") + s = e.copy() + for i in range(1, m): + s[i] -= sum(o[j] * k[i - 1 - j] for j in range(i)) + unit = identity(n) + u = shear(unit, k, upper=True) + ui = shear(unit, [-value for value in k], upper=True) + expected = a ** (m - 1) + need(norm(u) == norm(ui) == expected, "exact prefix norm") + need(shear(u, [-value for value in k], upper=True) == unit, + "two-sided square-zero shear inverse") + need(shear(ui, k, upper=True) == unit, "reverse inverse order") + completed = shear(middle(u, e, s), k, upper=False) + target = toeplitz(f) + need(completed == target, "literal factorization endpoint") + need(norm(target) == 1 + eta, "bounded completed output") + row = u[n - 2] + witness = [Q((value > 0) - (value < 0)) for value in row] + need(max(map(abs, witness)) == 1, "unit input witness") + need(sum(x * y for x, y in zip(row, witness)) == expected, + "attained infinity norm on an explicit input") + need(norm(u) == 1 + b * sum(a ** j for j in range(m - 1)), + "row geometric sum") + return {"eta": str(eta), "n": n, "a": str(a), + "prefix_norm": str(expected), "completed_norm": str(1 + eta)} + + +def rejected(call, message: str) -> None: + try: + call() + except ValueError as exc: + need(message in str(exc), "wrong rejection reason") + else: + raise ValueError("control failed to reject: " + message) + + +def controls() -> int: + rejected(lambda: parameters(Q(1), 8), "1 < eta") + rejected(lambda: parameters(Q(4), 8), "1 < eta") + rejected(lambda: parameters(Q(2), 6), "dyadic size") + rejected(lambda: parameters(Q(2), 128), "dyadic size") + rejected(lambda: quotient([Q(1)], [Q(2)]), "unit denominator") + # Omitting Z incorrectly includes the last quotient coefficient. + a, b = parameters(Q(3, 2), 8) + need(1 + b * sum(a ** j for j in range(4)) != a ** 3, + "unshifted-quotient control distinguishes the exponent") + f = [Q(1), b, a] + [Q(0)] * 5 + e, o = f[::2], f[1::2] + k = quotient(o, e) + wrong = e.copy() + for i in range(1, 4): + wrong[i] += sum(o[j] * k[i - 1 - j] for j in range(i)) + result = shear(middle(shear(identity(8), k, True), e, wrong), k, False) + need(result != toeplitz(f), "wrong Schur sign changes endpoint") + return 7 + + +def main() -> None: + results = [one_case(eta, n) for eta in ETAS for n in SIZES] + need(len(results) == 25, "finite fixture inventory") + for eta in ETAS: + a, _ = parameters(eta, 4) + for n in SIZES[:-1]: + small = Q(next(r["prefix_norm"] for r in results + if r["eta"] == str(eta) and r["n"] == n)) + large = Q(next(r["prefix_norm"] for r in results + if r["eta"] == str(eta) and r["n"] == 2 * n)) + need(large == a * small * small, "exact dyadic growth recurrence") + control_count = controls() + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("README.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py")} + print(json.dumps({"claim_type": "scoped proof with finite controls", + "package_sha256": hashes, "fixtures": results, + "controls": control_count}, sort_keys=True)) + print(f"PASS_PARITY_TAIL_THRESHOLD fixtures={len(results)} " + f"controls={control_count} max_n={MAX_N} no_new_kappa") + + +if __name__ == "__main__": + main()