diff --git a/research/critical-tail-parity-cuts/PROOF.md b/research/critical-tail-parity-cuts/PROOF.md new file mode 100644 index 0000000000..854b595c96 --- /dev/null +++ b/research/critical-tail-parity-cuts/PROOF.md @@ -0,0 +1,140 @@ +# The sharp critical-tail macro-cut envelope + +Produced by Nick Petalas. Apache-2.0. + +## Statement + +Let N be a positive power of two and let + +```text +f(z) = 1 + sum_(j=1)^(N-1) f_j z^j, sum_(j>=1) |f_j| <= 1, +``` + +with real or complex coefficients. Let T_N(f) be multiplication by f modulo +z^N in coefficient order. Use the exact parity compiler defined below. +A macro is one complete Toeplitz shear. The right shear precedes both +children; the left shear follows both children. The two children may use +any interleaving preserving their own macro orders. + +At any complete-macro cut, including the two endpoints, write T_N(f)=QP, +where P has executed and Q remains. Then + +```text +max(||P||_infinity, ||P^-1||_infinity, + ||Q||_infinity, ||Q^-1||_infinity) <= N. (1) +``` + +For each dyadic N this common bound is optimal. The quantifier includes +arbitrary coefficients in the stated tail ball and every legal schedule. +It excludes cuts inside a shear's implementation. + +## Definition and attribution of the compiler + +The retained construction is section 3 of Cinna Davis / PR4100's +`vendor/SHALLOW-TOEPLITZ.md`, following Vlado Vojdanovski / PR1673. +James Reed / PR4699 supplies the earlier one-level shared-budget estimate. +The following factorization is retained construction, not a new identity. +We write it out to specify every cut and prove the new boundary estimate. + +For N=2m, in the even/odd coordinate order, put + +```text +f(z) = e(z^2) + z o(z^2), k = o/e mod z^m, +s = e - z o^2/e mod z^m, E = T_m(e), S = T_m(s), K = T_m(k), +U = [ I ZK ; 0 I ], L = [ I 0 ; K I ], +T_N(f) = L diag(E,S) U, +``` + +where O=T_m(o) and Z=T_m(z). Multiplication verifies this identity because E,O,K,Z +commute and EK=O. All inverses exist as finite formal power series since +each symbol has constant term one. A one-coordinate leaf is the identity. +Coordinate permutations have infinity norm one and preserve the argument. + +## The unit tail ball is closed under both children + +Let a=||e-1||_1 and b=||o||_1 for coefficient l1 norm. Then a+b<=1. + +If a<1, the finite inverse of e has norm at most + +```text +sum_(j=0)^(m-1) a^j <= 1/(1-a). +``` + +Indeed e-1 has zero constant term, so its m-th power vanishes modulo z^m. +Coefficient norm is submultiplicative and truncation cannot increase it. +Consequently + +```text +||k||_1 <= b/(1-a) <= 1, +||s-1||_1 <= a + b^2/(1-a) <= a+b <= 1. (2) +``` + +If a=1, the budget forces b=0. Then o=k=0 and s=e. Both conclusions of +(2) still hold. This branch uses no division by 1-a. The even child also +has tail at most one. Thus every descendant is again in the same unit +tail ball, including its critical boundary. + +It follows that each of U,L,U^-1,L^-1 has infinity norm at most two. +The inverse shear changes only the sign of its off-diagonal block; +||K||_infinity<=||k||_1 and ||ZK||_infinity<=||k||_1. + +## Induction at every cut + +For N=1, all four operators are the identity. Assume (1) at dimension m. +During the child phase, let P_e,P_s be the child prefixes and Q_e,Q_s +their remaining suffixes. The exact four operators are + +```text +P = diag(P_e,P_s) U, +P^-1 = U^-1 diag(P_e^-1,P_s^-1), +Q = L diag(Q_e,Q_s), +Q^-1 = diag(Q_e^-1,Q_s^-1) L^-1. +``` + +The infinity norm of a coordinate direct sum is the maximum of its +summands' norms. Each displayed diagonal factor has norm at most m by +induction and (2). The neighboring shear or inverse shear has norm at +most two. Submultiplicativity gives 2m=N for every displayed operator. + +Every pair of legal child cuts can occur in a legal parent interleaving: +execute each child's chosen prefix, then each remaining suffix, preserving +the order inside each child. Conversely every parent cut in the child +phase specifies such a pair. This covers arbitrary legal interleavings, +including either child empty or complete. Parallel disjoint macros may be +serialized, so parallel-layer boundaries are included as well. + +The only other cuts are the initial and final endpoints. At N>=2, +||T_N(f)||_infinity<=2<=N. Writing A=T_N(f)-I gives A^N=0 and ||A||<=1, +so the exact finite identity + +```text +T_N(f)^-1 = sum_(j=0)^(N-1) (-A)^j +``` + +gives ||T_N(f)^-1||_infinity<=N. The endpoint identity factors have norm +one. This completes the induction without a strict-tail assumption. + +## Sharpness and scope + +For N>=2 take f=1-z. Its inverse is I+Z+...+Z^(N-1). The last row has +N entries equal to one, so its infinity norm is exactly N. This inverse +is P^-1 at the final cut and Q^-1 at the initial cut. At N=1 the identity +already attains one. Therefore no smaller bound can control all four +operators for each N. This elementary endpoint witness is credited prior +context; the new step is the universal upper bound at every macro cut. + +Brian / PR4731 already supplies the four-cut bound 1/(1-eta) at eta<1, +and PR4737 supplies the sharper forward-prefix bound 1+eta at eta<=1. +Nick Petalas / PR4831 gives the exact binomial forward-suffix law. None +of those narrower bounds is claimed as new here. The proof above starts +from the compiler definition and the finite inverse, and executes no +predecessor verifier. It concerns the full critical tail ball, rather +than just a binomial family or the forward-prefix operator. + +This bound permits a log2(N) macro amplification allowance at the critical +boundary. It does not admit that boundary to the original Gaussian caller, +whose other hypotheses remain strict. No claim prices internal shear +gates, rounding events, fixed tapes, preparation, storage, dirty restoration, +native realization, recursive invoices or the outer algorithm. This is a +scoped written proof, not a proof-kernel certificate or a complete +multiplication theorem. No new kappa is claimed. diff --git a/research/critical-tail-parity-cuts/README.md b/research/critical-tail-parity-cuts/README.md new file mode 100644 index 0000000000..7af5165988 --- /dev/null +++ b/research/critical-tail-parity-cuts/README.md @@ -0,0 +1,133 @@ +# Sharp linear growth at the triangular parity compiler's critical tail + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof with exact finite +corroboration. For every dyadic dimension N and every real or complex unit +symbol whose coefficient tail has l1 norm at most one, the exact triangular +Toeplitz parity compiler satisfies + +```text +T_N(f) = Q P +max(||P||_infinity, ||P^-1||_infinity, + ||Q||_infinity, ||Q^-1||_infinity) <= N. +``` + +This holds at every complete-shear cut, including both endpoints, and for +every order-preserving interleaving of the disjoint children. For each N the +common constant is optimal. The inverse endpoint for f=1-z attains N. +[PROOF.md](PROOF.md) gives the complete induction and its critical a=1,b=0 +branch. Infinite Neumann convergence is unnecessary. + +The new result is the universal four-operator upper bound at the critical +tail. Brian's [PR4731](https://github.com/CrocSwap/integer-mult-bounds/pull/4731) +already gives 1/(1-eta) for eta<1, and his +[PR4737](https://github.com/CrocSwap/integer-mult-bounds/pull/4737) gives the +sharper forward-prefix bound 1+eta through eta=1. Nick Petalas's +[PR4831](https://github.com/CrocSwap/integer-mult-bounds/pull/4831) gives the +exact binomial suffix law. Those results and the elementary attaining +inverse endpoint retain their credit. No predecessor scientific verifier +is imported or replayed here. + +## Reproduction and evidence + +Use CPython 3.12 and its standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/critical-tail-parity-cuts/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/critical-tail-parity-cuts/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/critical-tail-parity-cuts +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/critical-tail-parity-cuts --check-source-history +``` + +Any CPython 3.12 path can replace the local interpreter. Both registered +checks have 60-second limits. The standalone verifier writes nothing and +runs in a Git-free export. It emits `PASS_CRITICAL_TAIL_PARITY_CUTS` in a +generated JSON receipt binding all six package files by SHA256. No receipt +is handwritten or committed. + +The exact checker covers 162 rational symbols, including 91 with tail norm +exactly one, and 557 nonleaf tree nodes. It enumerates every distinct legal +cut prefix for each fixture by taking all child-cut pairs. There are 951 +cut quadruples. Each has a dense independently eliminated prefix inverse, +literal suffix and inverse suffix, endpoint identities and four norm checks. +Identical operators from different schedules are deduplicated; these are +counts of operators per fixture, not schedules. + +The complete quarter-grid tail balls at dimensions two and four are included. +Dimension-eight fixtures cover signed single shifts, mixed odd/even tails and +the even-tail-one case. Six dimensions through 32 check every entry of the +attaining binomial inverse. Seven controls distinguish a wrong Schur sign, +wrong chronology, missing left shear, two invalid symbol domains, the +zero-denominator branch and the necessary dimension loss. These finite +domains corroborate the written real/complex theorem; they do not prove its +unbounded quantifiers or enumerate arbitrary complex symbols. + +## Scope and implementation limits + +This supplies a log2(N) macro amplification allowance at the critical +boundary. It does not install a precision change or admit eta=1 to the +Gaussian caller. Internal shear gates, additional rounding events, +coefficient preparation, native operations, owned storage and restoration, +movement, tapes, stock, compiler and outer recovery remain separate. +All five selected framework assumptions retain their status. No new kappa, +selected-frontier change, supplier admission, complete multiplication +theorem, independent human review or formal proof-kernel review is claimed. +The selected cold replay, Lean and Docker were unrun. + +Power of Ten review is limited to this verifier. The compiler tree uses +bottom-up bounded loops and no recursion. Its census dimension is at most +eight, with at most 123 prefix matrices per node by the recurrence +c(1)=1, c(2m)<=2+c(m)^2. Dense sharpness matrices have dimension at most 32. +Every function has fewer than 60 physical lines. Mathematical checks use +explicit exceptions and remain active under optimization. The six source +reads are the fixed package inventory; there are no subprocesses, imports +of predecessor executables, network calls, dynamic code or mutable global +state. Python/Fraction allocation is a managed-runtime deviation from fixed +allocation. These fixed replay domains bound live data; allocation-free +execution is unclaimed. Warning-strict normal and optimized execution and +AST/function-size inspection provide the available diagnostics. + +## Provenance and credit + +Scientific base: canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected +PR6030. The selected-baseline orientation passed at kappa 0.003125804; +that check authenticates metadata, not a scientific supplier replay. +[TASK.json](TASK.json) explicitly changes the formal-interface card to a +written component theorem, without a proof-kernel or selected-caller claim. +[SOURCES.json](SOURCES.json) pins the compiler and credited predecessor +notes as historical provenance. Runtime depends only on package files. + +The parity factorization retains Vlado Vojdanovski / PR1673 and Cinna Davis / +[PR4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) credit. +James Reed / [PR4699](https://github.com/CrocSwap/integer-mult-bounds/pull/4699) +supplies the earlier one-level shared-budget estimate. Brian's complete-cut +and forward-prefix results, Nick Petalas's binomial suffix law, Ryanson +Jonathan's numerical-ledger motivation and the retained Gaussian/compiler +lineage keep their attribution. Finite triangular inversion and elementary +matrix norm inequalities are classical. The new proof starts from the +retained factorization and finite inverse, without assuming a predecessor's +universal cut theorem. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362993) +records this original question. Live open/account PRs, recent handoffs, +active Discussions, local reservations, all-main README searches and merged +general-form searches were checked. The cached card search covered 412 open +PRs and 6,369 Discussion records with complete remote pagination, but only +108 of 8,917 main note paths were materialized. Targeted Git searches covered +the relevant main README text. Arbitrary diffs, unpublished work and later +posts remain outside coverage. These checks are not a novelty certificate. + +## Open next questions + +What is the best universal forward-suffix bound at tail norm at most one? +The common N bound is forced by inverse endpoints; the credited binomial +family only needs 1+log2(N) for forward suffixes. Start with a suffix-only +induction on independent even/odd budgets. No universal sharp suffix-only +bound is supplied here. + +Can an actual critical-tail caller pay for every gate inside a complete +shear? Start with its literal microprogram, entry/exit contract, rounding +events and complete suffix/tape bill. Internal amplification, preparation +and physical accounting block that extension. No further work is reserved. diff --git a/research/critical-tail-parity-cuts/SOURCES.json b/research/critical-tail-parity-cuts/SOURCES.json new file mode 100644 index 0000000000..eabf8daa72 --- /dev/null +++ b/research/critical-tail-parity-cuts/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + }, + { + "path": "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md", + "usage": "provenance", + "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be", + "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310" + }, + { + "path": "research/triangular-parity-prefix/README.md", + "usage": "provenance", + "git_blob": "1d5e9c4c07246169a4efd2b9a0482bab9ad2a3a8", + "sha256": "c5a9db1f99274e5928c56f328ff67286e778675c2dc21e12d372b6a072b03548" + }, + { + "path": "research/triangular-parity-uniform-prefix/README.md", + "usage": "provenance", + "git_blob": "6e64fb48fbd33b9742f0ba81de77bfb661b80403", + "sha256": "dd0259414df08b5b462cec450df5a0618c30ba112ddf87b2acbb2e39a1c69414" + }, + { + "path": "research/triangular-parity-forward-bound/README.md", + "usage": "provenance", + "git_blob": "d008710585a897b9b568e74c7b867d8c784e4aa8", + "sha256": "745c2105fc614e6ba453327a37e483b808425a40ce3e2b44e2643b0ea1db3781" + }, + { + "path": "research/triangular-parity-binomial-suffix/README.md", + "usage": "provenance", + "git_blob": "40be9dc4c7cf7a8e0b1e4f29267adeecdb4bddd8", + "sha256": "9c92249119c31c97b970975ef28ea8a23263acd8e5d5b95f083b71af93b2d5f1" + } + ] +} diff --git a/research/critical-tail-parity-cuts/TASK.json b/research/critical-tail-parity-cuts/TASK.json new file mode 100644 index 0000000000..0ad140f502 --- /dev/null +++ b/research/critical-tail-parity-cuts/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp universal N bound for all four complete-macro cut operators of the exact triangular parity compiler at coefficient-tail l1 <= 1.", + "scope_change_reason": "Replace a proof-kernel interface task by a written critical-boundary precision theorem with exact finite corroboration; no selected-caller assumption is discharged.", + "bottleneck_link": "Provides a finite, sharp amplification envelope where the strict-tail 1/(1-eta) envelope diverges. This is a component lemma for the retained parity compiler, not admission of a critical-tail Gaussian caller.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sharp common envelope and bounded exact matrix evidence; do not extend to internal shear gates or a complete supplier.", + "outcome": "completed", + "evidence": "PROOF.md and the standalone exact verifier: 162 rational symbols, 91 critical symbols, 951 cut quadruples, 557 tree nodes, six attaining dimensions and seven controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the best universal forward-suffix bound at tail l1 <= 1?", + "why_it_matters": "The common N bound is forced by inverse endpoints and may overcharge forward suffix propagation.", + "first_step": "Separate the forward-suffix induction from inverse endpoints and compare with the credited binomial law 1+log2(N).", + "blocked_by": "No universal forward-suffix-only sharp bound is proved here." + }, + { + "question": "Can one actual critical-tail caller pay for every gate inside a complete shear?", + "why_it_matters": "Macro-cut stability alone does not permit a larger tail in the physical Gaussian routine.", + "first_step": "Name the actual shear microprogram, its rounding events and entry/exit contract, then derive a complete suffix and tape bill.", + "blocked_by": "Internal amplification, rounding, preparation and physical accounting remain outside this package." + } + ] +} diff --git a/research/critical-tail-parity-cuts/VERIFY.json b/research/critical-tail-parity-cuts/VERIFY.json new file mode 100644 index 0000000000..95606c0daf --- /dev/null +++ b/research/critical-tail-parity-cuts/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": 60, + "checks": "Exact finite parity identities, all child-cut pairs for declared rational symbols, four norm envelopes, sharpness and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete evidence with optimized Python; mathematical checks remain enabled." + } + ] +} diff --git a/research/critical-tail-parity-cuts/verify.py b/research/critical-tail-parity-cuts/verify.py new file mode 100644 index 0000000000..3b87df8ad6 --- /dev/null +++ b/research/critical-tail-parity-cuts/verify.py @@ -0,0 +1,223 @@ +"""Exact critical-tail parity-cut evidence. Produced by Nick Petalas. + +Apache-2.0. Only the Python standard library is used; execution writes nothing. +""" + +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def eye(n): + return tuple(tuple(Q(i == j) for j in range(n)) for i in range(n)) + + +def mul(a, b): + n = len(a) + return tuple(tuple(sum((a[i][k] * b[k][j] for k in range(n)), Q(0)) + for j in range(n)) for i in range(n)) + + +def norm(a): + return max(sum(abs(x) for x in row) for row in a) + + +def inverse(a): + """Independent dense row elimination, with bounded pivot search.""" + n = len(a) + rows = [list(row) + list(unit) for row, unit in zip(a, eye(n))] + for k in range(n): + pivot = next((i for i in range(k, n) if rows[i][k]), None) + need(pivot is not None, 'invertible literal matrix') + rows[k], rows[pivot] = rows[pivot], rows[k] + q = rows[k][k] + rows[k] = [x / q for x in rows[k]] + for i in range(n): + if i != k: + q = rows[i][k] + rows[i] = [x - q * y for x, y in zip(rows[i], rows[k])] + return tuple(tuple(row[n:]) for row in rows) + + +def convolution(a, b, n): + return tuple(sum((a[j] * b[i - j] for j in range(i + 1) + if j < len(a) and i - j < len(b)), Q(0)) + for i in range(n)) + + +def reciprocal(a): + need(a[0] == 1, 'unit constant coefficient') + out = [Q(1)] + for k in range(1, len(a)): + out.append(-sum((a[j] * out[k - j] for j in range(1, k + 1)), Q(0))) + return tuple(out) + + +def toeplitz(f): + n = len(f) + return tuple(tuple(f[i - j] if i >= j else Q(0) for j in range(n)) + for i in range(n)) + + +def split(f, wrong_sign=False): + n = len(f) + need(n >= 2 and n & (n - 1) == 0, 'dyadic nonleaf dimension') + e, o = f[::2], f[1::2] + k = convolution(o, reciprocal(e), n // 2) + correction = convolution(o, k, n // 2) + sign = 1 if wrong_sign else -1 + s = tuple(e[i] + sign * (correction[i - 1] if i else 0) + for i in range(n // 2)) + return e, s, k + + +def shears(k): + """Embed both complete shears in original coefficient order.""" + n = 2 * len(k) + u, l = [list(row) for row in eye(n)], [list(row) for row in eye(n)] + for i in range(n // 2): + for j in range(i + 1): + l[2 * i + 1][2 * j] = k[i - j] + if j < i: + u[2 * i][2 * j + 1] = k[i - j - 1] + return tuple(map(tuple, u)), tuple(map(tuple, l)) + + +def interlace(a, b): + n = len(a) + return tuple(tuple(a[i // 2][j // 2] if i % 2 == j % 2 == 0 + else b[i // 2][j // 2] if i % 2 == j % 2 == 1 + else Q(0) for j in range(2 * n)) for i in range(2 * n)) + + +def cut_states(f): + """Enumerate every child-cut pair, using a bottom-up nonrecursive tree.""" + need(1 <= len(f) <= 8 and len(f) & (len(f) - 1) == 0, 'cut census size') + levels = [[f]] + for _ in range(len(f).bit_length() - 1): + children = [] + for symbol in levels[-1]: + e, s, _ = split(symbol) + children.extend((e, s)) + levels.append(children) + states = [(eye(1),) for _ in levels[-1]] + nodes = 0 + for symbols in reversed(levels[:-1]): + parents = [] + for index, symbol in enumerate(symbols): + e, s, k = split(symbol) + a = sum(abs(x) for x in e[1:]) + b = sum(abs(x) for x in symbol[1::2]) + need(a + b <= 1, 'inherited unit tail budget') + need(sum(abs(x) for x in k) <= 1, 'bounded complete shear') + need(sum(abs(x) for x in s[1:]) <= 1, 'Schur unit tail budget') + u, l = shears(k) + endpoint = mul(l, mul(interlace(toeplitz(e), toeplitz(s)), u)) + need(endpoint == toeplitz(symbol), 'literal parity endpoint') + prefixes = {eye(len(symbol)), endpoint} + for left, right in product(states[2 * index], states[2 * index + 1]): + prefixes.add(mul(interlace(left, right), u)) + parents.append(tuple(sorted(prefixes))) + nodes += 1 + states = parents + return states[0], nodes + + +def check_symbol(f): + need(f[0] == 1 and sum(abs(x) for x in f[1:]) <= 1, 'admitted symbol') + prefixes, nodes = cut_states(f) + target = toeplitz(f) + target_inverse = inverse(target) + need(mul(target, target_inverse) == eye(len(f)), 'independent endpoint inverse') + digest = sha256() + for prefix in prefixes: + pinv = inverse(prefix) + suffix = mul(target, pinv) + sinv = mul(prefix, target_inverse) + need(mul(suffix, prefix) == target, 'complete chronological cut') + need(mul(suffix, sinv) == eye(len(f)), 'literal suffix inverse') + need(all(norm(x) <= len(f) for x in (prefix, pinv, suffix, sinv)), + 'four critical-cut envelopes') + digest.update(str((prefix, pinv, suffix, sinv)).encode()) + return len(prefixes), nodes, digest.hexdigest() + + +def fixtures(): + yield (Q(1),) + for n in (2, 4): + for tail in product(range(-4, 5), repeat=n - 1): + if sum(abs(x) for x in tail) <= 4: + yield (Q(1),) + tuple(Q(x, 4) for x in tail) + for shift in range(1, 8): + for sign in (-1, 1): + yield (Q(1),) + tuple(Q(sign if i == shift else 0) for i in range(1, 8)) + for signs in product((-1, 1), repeat=3): + yield (Q(1), Q(signs[0], 2), Q(signs[1], 4), Q(signs[2], 4)) + (Q(0),) * 4 + yield (Q(1), Q(0), Q(1, 2), Q(1, 2), Q(0), Q(0), Q(0), Q(0)) + + +def controls(): + checks = [] + f = (Q(1), Q(1, 2), Q(1, 2), Q(0)) + e, s, k = split(f, wrong_sign=True) + u, l = shears(k) + need(mul(l, mul(interlace(toeplitz(e), toeplitz(s)), u)) != toeplitz(f), + 'wrong Schur sign must fail') + checks.append('wrong Schur sign') + e, s, k = split(f) + middle = interlace(toeplitz(e), toeplitz(s)) + need(mul(u, mul(middle, l)) != toeplitz(f), 'wrong chronology must fail') + need(mul(middle, u) != toeplitz(f), 'missing left shear must fail') + checks.extend(('wrong chronology', 'missing left shear')) + for bad in ((Q(0),), (Q(1), Q(2))): + try: + check_symbol(bad) + except ValueError: + checks.append('invalid symbol ' + str(bad)) + else: + raise ValueError('invalid symbol accepted') + f = (Q(1), Q(0), Q(1), Q(0)) + need(split(f)[2] == (0, 0), 'even-tail-one singular-denominator branch') + checks.append('even-tail-one branch') + need(norm(inverse(toeplitz((Q(1), Q(-1))))) == 2, + 'constant common envelope cannot replace dimension') + checks.append('missing dimension loss') + return checks + + +def main(): + cases, total_cuts, nodes, critical = [], 0, 0, 0 + for f in fixtures(): + count, visited, digest = check_symbol(f) + cases.append([list(map(str, f)), count, digest]) + total_cuts += count + nodes += visited + critical += sum(abs(x) for x in f[1:]) == 1 + sharp = [] + for n in (1, 2, 4, 8, 16, 32): + f = (Q(1),) + ((Q(-1),) if n > 1 else ()) + (Q(0),) * max(0, n - 2) + inv = inverse(toeplitz(f)) + need(norm(inv) == n, 'attained sharp dimension envelope') + need(inv == tuple(tuple(Q(i >= j) for j in range(n)) for i in range(n)), + 'literal geometric inverse entries') + sharp.append([n, str(norm(inv))]) + result = {'status': 'PASS_CRITICAL_TAIL_PARITY_CUTS', 'symbols': len(cases), + 'critical_symbols': critical, 'cut_quadruples': total_cuts, + 'tree_nodes': nodes, 'cases_sha256': sha256(json.dumps(cases).encode()).hexdigest(), + 'sharpness': sharp, 'controls': controls()} + here = Path(__file__).resolve().parent + names = ('PROOF.md', 'README.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'verify.py') + result['files_sha256'] = {name: sha256((here / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()