diff --git a/research/downset-block-solve-bound/README.md b/research/downset-block-solve-bound/README.md new file mode 100644 index 0000000000..0b753c1b16 --- /dev/null +++ b/research/downset-block-solve-bound/README.md @@ -0,0 +1,241 @@ +# A block-solve envelope for completed elimination downsets + +This contribution is produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped all-size proof, with exact finite corroboration.** +At the ideal completed-shear/scalar boundary of recursive block elimination, +the common spectral-norm envelope improves from Brian's proposed +`32 N^(3/2) (ΛQ)^8` in [PR #4788](https://github.com/CrocSwap/integer-mult-bounds/pull/4788) +to **`2 sqrt(N) (ΛQ)^2`**. The new proof bounds whole block rows and inverse +block columns through original leading solves. It does not modify a compiler +or rounded allocation. There is no new κ or selected-frontier claim. + +## Theorem and boundary + +Let `T` be a complex `N×N` matrix, `N>=1`, such that + +``` +Λ,Q >= 1, ||T||₂ <= Λ, ||T_k^-1||₂ <= Q for 1<=k<=N, +T_k = T[0:k,0:k]. +``` + +Every leading section is invertible. Put `χ=ΛQ` and `S=Λ+Λ²Q`. +Choose any binary tree of contiguous coordinate intervals. At `[a,b)` split +at `s`, the reference matrix is the Schur descendant `T_b/T_a`, with the +empty-prefix convention. Execute the upper shear, both children in any +legal interleaving, then the lower shear. A leaf executes its scalar pivot. +Atoms are complete ideal shears and scalars, including identity atoms. + +For every downset of this atomic dependency order, let `P` be its endpoint +product. Form a partition by stopping at a fully finished subtree or a +subtree none of whose atoms has executed, and otherwise descending. Label +its intervals finished or untouched. If their counts are `c` and `u`, then + +``` +||P||₂² <= c S² + u(1+χ²), +||P^-1||₂² <= c Q² + u(1+χ²). +``` + +The partition has `1<=c+u<=N`. Since `S>=1+χ>=sqrt(1+χ²)` and +`Q<=χ`, this implies + +``` +||P||₂ <= sqrt(N) (Λ+Λ²Q), +||P^-1||₂ <= sqrt(N(1+χ²)), +``` + +and the common envelope `2 sqrt(N) χ²`. Neither Toeplitz structure, +positivity, equal splits nor a balanced tree is required. The theorem +concerns complete calls. Cuts inside a generator/FFT call, rounded arithmetic, +storage, native cost and the complete multiplication theorem are outside scope. + +## Proof + +### 1. Retain the global factorization and its order + +Write the unique scalar unit-LDU factorization as `T=L D U`. For an interval +`J=[a,b)`, write `M_J=T_b/T_a` and `U_J=U[J,J]`. The identities +`M_J=L[J,J] D[J,J] U_J` and the completed-downset/frontier factorization +are inherited from Jose Manuel's `rational-unitary-fft/FULL-PROOF.md`, +sections 2 and 4, and Brian's PR #4788, sections 2 and 3, head +`ddd98e28b1d6a674b1d6b93c5d7de8a9f9c86eec`. +The latter includes arbitrary contiguous interval trees. They are cited +inputs, not results audited here. + +Let `B` be the finished/untouched partition. Define + +``` +U_B = direct_sum over J in B of U_J, +E_B = direct_sum over J in B of (M_J if finished, I_J if untouched). +``` + +The inherited factorization gives, in this order, + +``` +P = E_B U_B^-1 U, (1) +P^-1 = U^-1 U_B E_B^-1. (2) +``` + +Indeed the usual upper frontier stops at untouched internal nodes and has +singleton leaves inside finished nodes. Replacing those singletons within a +finished `J` by `U_J` changes its left factor from `L_J D_J` to +`M_J=L_J D_J U_J`; the new right factor `U_J^-1` cancels that change. +Untouched blocks already have left factor identity and upper block `U_J`. +This gives (1) without commuting overlapping factors. Incomparable atoms +have disjoint intervals, so all legal linearizations give the same product. +Equivalently, contract each finished or untouched node to one block. At an +open internal node its lower atom is absent, so its product is +`diag(P_left,P_right) R`. Substituting the child formulas and +`U_node=diag(U_left,U_right) R` proves (1) inductively for every interval +tree. The two stopping cases are respectively `P=M_J` and `P=I_J`. + +### 2. Bound forward block rows + +For a finished `J=[a,b)`, equation (1) gives + +``` +P[J,:a] = 0, +P[J,a:N] = T[J,a:N] - T[J,:a] T_a^-1 T[:a,a:N]. (3) +``` + +Eliminate the leading `a` rows of `T=LDU` and restrict the resulting +rectangular Schur row to `J`. Each restriction of `T` has norm at most `Λ`. +Thus this whole block row has norm at most `S`. At `a=0` the second term +is absent and `Λ<=S` suffices. + +For an untouched `J`, its row is `U_J^-1 U[J,:]`. It is zero before `a`, +identity on `J`, and has tail + +``` +K_J = (T_b^-1 T[:b,b:N])[a:b,:]. (4) +``` + +To see this, cancel `L_b D_b` in `T_b^-1 T[:b,b:N]`. The last block rows +of the result are `U_J^-1 U[J,b:N]`. Hence `||K_J||<=QΛ=χ`. +The row `[I_J K_J]` has squared norm `1+||K_J||²<=1+χ²` by its Gram +product. For any `x`, sum the squared norms of the disjoint block-row +outputs of `Px`. This proves `||P||²<=cS²+u(1+χ²)`. + +### 3. Bound inverse block columns + +For every interval `J=[a,b)`, triangular block inversion gives + +``` +(U^-1[:,J] U_J)[0:b,:] = [-T_a^-1 T[:a,J]; I_J], (5) +(U^-1[:,J] U_J)[b:N,:] = 0. +``` + +At `a=0` the top block is empty. For the top identity, invert the upper +`2×2` blocks on `[:a,J]` and use +`T_a^-1 T[:a,J]=U[:a,:a]^-1 U[:a,J]`. + +An untouched block column in (2) equals (5). Its norm is at most +`sqrt(1+χ²)`, using the original leading solve at `a`, or is one if `a=0`. +For a finished block, multiply (5) on the right by `M_J^-1`. +The ordinary block inverse formula identifies the result as + +``` +P^-1[0:b,J] = T_b^-1[:,a:b], +P^-1[b:N,J] = 0. (6) +``` + +Its whole block-column norm is at most `Q`. This avoids multiplying +separate bounds for the two factors in (5). + +For disjoint input blocks, `P^-1 x=sum_J C_J x_J`. The triangle and +Cauchy-Schwarz inequalities give + +``` +||sum_J C_J x_J|| <= sum_J ||C_J|| ||x_J|| + <= sqrt(sum_J ||C_J||²) ||x||. +``` + +This proves the inverse inequality. Empty downsets, finished roots, +singletons and zero-width tails are included. Finally +`S=Λ(1+χ)<=2Λχ<=2χ²` proves the common envelope. + +## Exact evidence and reproduction + +`verify.py` is a self-contained standard-library checker. It constructs +literal upper/child/lower atomic programs and checks all binary contiguous +interval trees through five leaves and every downset of each tree, for one +real and one nonreal rational fixture per size. Complex matrices use faithful +interleaved rational realification. No predecessor verifier or unmerged Git +object is imported. + +For each downset it computes `P` by literal atomic multiplication and its +inverse by exact elimination, then checks (1), (3), (4), (5) and (6). +Exact rational positive-semidefinite tests certify block norms and both +assembled squared bounds. The printed receipt enumerates its checks and +binds them to hashes of the package files. Checks use explicit exceptions +and remain enabled under `-O`. Rejection controls cover wrong factor order, +omitted finished endpoints, wrong inverse signs, invalid partitions, invalid +spectral certificates and using only the whole-matrix inverse premise. +The complete finite replay passes 46 trees, 2,380 downsets, 9,520 matrix +identities, 9,372 partition blocks and 23,504 downset spectral certificates. +Eleven control groups pass, including 2,244 wrong-order, 2,160 omitted-endpoint +and 1,940 inverse-sign distinguishing states. These are finite coverage counts, +not claims about every complex matrix. + +From the worktree root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/downset-block-solve-bound/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/downset-block-solve-bound/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/downset-block-solve-bound +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/downset-block-solve-bound --check-source-history +``` + +The last command follows committing. The universal claim rests on the written +proof. A selected-baseline metadata control passed; the selected construction +was not replayed. Independent human and formal proof-kernel review are unclaimed. + +Checker resource limits: Python/Fraction arithmetic allocates managed objects. +The checker fixes at most five logical coordinates and ten real coordinates, +at most 16 tree shapes per size, and at most 256 downsets per tree. Loop +bounds follow these capacities or fixed package-file inventories. No recursion, +dynamic imports, code evaluation, subprocesses or external runtime dependencies are used. +The three negative-control callbacks have fixed local targets and no retained +state. AST syntax validation and warning-strict execution supplement the replay; +no unavailable standalone lint or type-check pass is claimed. A future +parameterized checker must add input/bit-size limits before lifting these +fixed-fixture resource bounds. + +## Open next questions + +1. Can this envelope replace the old one in the complete rounded Full factory? + First list every old-envelope dependency and prove the new allocation + inequalities. Unfinished generator fragments and scalar/data grids retain + their own obligations. No factory substitution is supplied here. +2. Is square-root growth in the number of frontier blocks necessary when + `Λ,Q` stay bounded? Seek an explicit growing family or a bound exploiting + shared block-solve geometry. No asymptotic sharpness claim is made. + +## Attribution and overlap + +Credit Brian (JoyboyBrian), PR #4788, for global-factor restrictions, +arbitrary interval trees and the previous `32 N^(3/2)χ^8` envelope; +Jose Manuel (jmbarrancoml), PR #4205, for the original scalar-LDU/frontier +proof and polynomial Full-recursion envelope; and Vlado Vojdanovski, +PR #1673, for the recursive compiler. Classical Schur and block inverse +identities are background. The new step is the mixed finished/untouched +partition and direct original-leading-solve block norm estimate. Predecessor +credit and disclosures remain unchanged in their own packages. + +The task changes `uniform-transfer-audit` into a new precision-interface +inequality. Brian's open package studies the same quantity and is the +nearest predecessor. Triangular parity-prefix/suffix and dirty FFT gate-cut +packages use different schedules and boundaries; this does not extend their +exact constants or audit their results. + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133325) +records the scope. Main README searches, merged PR searches, live open PR +bodies, recent handoffs and local reservations were checked. Those searches +do not cover unpublished investigations or every historical diff. +Provenance pins are in `SOURCES.json`; runtime needs only this package. +The overlap helper covered 367 open PRs and 3,821 Discussion records at its +21:46–21:47 UTC snapshot. Its sparse local inventory covered 115 of 6,319 +HEAD notes; separate `git grep` searched all main package READMEs for the +distinctive terms. No complete local-note inventory or novelty certificate +is claimed. A canonical refresh after the first replay retained the same base. diff --git a/research/downset-block-solve-bound/SOURCES.json b/research/downset-block-solve-bound/SOURCES.json new file mode 100644 index 0000000000..d7d2c04154 --- /dev/null +++ b/research/downset-block-solve-bound/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/rational-unitary-fft/FULL-PROOF.md", + "usage": "provenance", + "git_blob": "e650f46863115f810e27b403f916dd7f79b37786", + "sha256": "acf8c596d91b5efd35a286735d6867ff8afce64354a13f680c2fae3dab824410" + }, + { + "path": "research/full-toeplitz-cut-audit/README.md", + "usage": "provenance", + "git_blob": "f088efaaa828e415db6bb152a8cbeaea1dd68dd7", + "sha256": "5b514f93ab3b0a37a32978a599d74c545ed19122e235f9cccfff36faefb97a9b" + } + ] +} diff --git a/research/downset-block-solve-bound/TASK.json b/research/downset-block-solve-bound/TASK.json new file mode 100644 index 0000000000..3fe41a35e9 --- /dev/null +++ b/research/downset-block-solve-bound/TASK.json @@ -0,0 +1,108 @@ +{ + "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": "A sharper spectral-norm bound for every ideal completed-call downset of contiguous block elimination over C.", + "scope_change_reason": "Take a new block-solve inequality beyond the original LDU/frontier theorem and Brian PR4788; predecessor auditing is outside this contribution.", + "bottleneck_link": "The completed-call envelope enters Full-PROOF.md precision guards. A smaller envelope is useful before a separately justified physical-factory substitution.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and exactly corroborated sharper bound; no synthesis or downstream factory modification.", + "outcome": "completed", + "evidence": "README.md contains the all-size proof. verify.py constructs exact real and complex fixtures, all interval trees through five leaves, and all their atomic downsets.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the new envelope replace the old one in the complete rounded Full factory?", + "why_it_matters": "The factory spends powers of its completed-call envelope in precision and error allocations.", + "first_step": "List each dependency on the old envelope, then substitute the new value in a separate proof and matched literal-caller experiment.", + "blocked_by": "Unfinished generator fragments, rounding and scalar allocations remain outside this result." + }, + { + "question": "Is the square-root dependence on the number of frontier blocks necessary under bounded original leading conditioning?", + "why_it_matters": "The new estimate sums block bounds and may still overcount shared geometry.", + "first_step": "Seek a family with bounded Lambda and Q and growing downset norm, or exploit correlations among the block solves.", + "blocked_by": "No asymptotic sharpness construction is supplied." + } + ], + "predecessors": [ + { + "pr": 4788, + "author": "Brian (JoyboyBrian)", + "head": "ddd98e28b1d6a674b1d6b93c5d7de8a9f9c86eec", + "role": "Global scalar-LDU restrictions, arbitrary interval trees, frontier factorization and 32 N^(3/2) chi^8 envelope. Cited only; no runtime dependency." + }, + { + "pr": 4205, + "author": "Jose Manuel (jmbarrancoml)", + "role": "Original full-recursion completed-downset proof, retained on canonical main." + }, + { + "pr": 1673, + "author": "Vlado Vojdanovski", + "role": "Recursive compiler and block-elimination scheduler." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133325", + "overlap": { + "checked_at": "2026-10-22T21:47:27Z", + "open_prs": 367, + "discussion_records": 3821, + "local_head_notes": 6319, + "local_notes_searched": 115, + "local_inventory_complete": false, + "method": "Main README git-grep complements the sparse helper inventory; live PR bodies and merged-term searches were checked. PR4788 is cited, not audited. Unpublished work and arbitrary historical diffs are outside coverage." + } +} diff --git a/research/downset-block-solve-bound/VERIFY.json b/research/downset-block-solve-bound/VERIFY.json new file mode 100644 index 0000000000..2e0940757e --- /dev/null +++ b/research/downset-block-solve-bound/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": 240, + "checks": "Exact block-row and inverse-column identities, spectral PSD certificates, every downset of all interval trees through five leaves, and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact block-row and inverse-column identities, spectral PSD certificates, every downset of all interval trees through five leaves, and rejection controls." + } + ] +} diff --git a/research/downset-block-solve-bound/verify.py b/research/downset-block-solve-bound/verify.py new file mode 100644 index 0000000000..afe1d85d0c --- /dev/null +++ b/research/downset-block-solve-bound/verify.py @@ -0,0 +1,390 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the block-solve downset envelope.""" +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +MAX_N = 5 +MAX_REAL = 10 +MAX_TREES = 16 +MAX_STATES = 256 +FILES = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def zeros(rows, cols): + require(0 <= rows <= MAX_REAL and 0 <= cols <= MAX_REAL, 'matrix capacity') + return [[F(0) for _ in range(cols)] for _ in range(rows)] + + +def eye(n): + out = zeros(n, n) + for i in range(n): + out[i][i] = F(1) + return out + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def mul(a, b): + require(bool(a) and bool(b) and len(a[0]) == len(b), 'product shape') + out = zeros(len(a), len(b[0])) + for i, row in enumerate(a): + for k, value in enumerate(row): + if value: + for j, other in enumerate(b[k]): + if other: + out[i][j] += value * other + return out + + +def sub(a, b): + require(len(a) == len(b) and len(a[0]) == len(b[0]), 'difference shape') + return [[x - y for x, y in zip(r, s)] for r, s in zip(a, b)] + + +def block(a, r0, r1, c0, c1): + return [row[c0:c1] for row in a[r0:r1]] + + +def put(a, r0, c0, b): + for i, row in enumerate(b): + for j, value in enumerate(row): + a[r0 + i][c0 + j] = value + + +def inv(a): + n = len(a) + require(1 <= n <= MAX_REAL and all(len(r) == n for r in a), 'inverse shape') + out = eye(n) + work = [r[:] for r in a] + for k in range(n): + pivot = next((i for i in range(k, n) if work[i][k]), None) + require(pivot is not None, 'singular matrix') + work[k], work[pivot] = work[pivot], work[k] + out[k], out[pivot] = out[pivot], out[k] + scale = work[k][k] + work[k] = [x / scale for x in work[k]] + out[k] = [x / scale for x in out[k]] + for i in range(n): + if i != k: + scale = work[i][k] + work[i] = [x - scale * y for x, y in zip(work[i], work[k])] + out[i] = [x - scale * y for x, y in zip(out[i], out[k])] + require(mul(a, out) == eye(n) and mul(out, a) == eye(n), 'inverse residual') + return out + + +def psd(a): + n = len(a) + require(a == transpose(a), 'PSD symmetry') + work = [r[:] for r in a] + for k in range(n): + pivot = work[k][k] + if pivot < 0: + return False + if pivot == 0: + if any(work[i][k] for i in range(k + 1, n)): + return False + else: + for i in range(k + 1, n): + for j in range(k + 1, n): + work[i][j] -= work[i][k] * work[k][j] / pivot + return True + + +def norm_squared_at_most(a, bound): + require(bound >= 0 and bool(a) and bool(a[0]), 'norm contract') + # Use the smaller Gram matrix without changing its nonzero spectrum. + gram = mul(a, transpose(a)) if len(a) <= len(a[0]) else mul(transpose(a), a) + return psd(sub([[bound * x for x in r] for r in eye(len(gram))], gram)) + + +def envelope(a): + return max(F(1), max(sum(map(abs, r)) for r in a), + max(sum(map(abs, r)) for r in transpose(a))) + + +def fixture(n, width): + size = n * width + lower, upper, diagonal = eye(size), eye(size), zeros(size, size) + for i in range(n): + pivot = [[F(i + 2, i + 1)]] if width == 1 else [ + [F(i + 2, i + 1), F(-1, i + 2)], + [F(1, i + 2), F(i + 2, i + 1)]] + put(diagonal, width * i, width * i, pivot) + for j in range(i): + real, imag = F((-1) ** (i + j), 3 + i + j), F(1, 4 + i + j) + lo = [[real]] if width == 1 else [[real, -imag], [imag, real]] + up = [[-2 * real]] if width == 1 else [ + [-2 * real, imag], [-imag, -2 * real]] + put(lower, width * i, width * j, lo) + put(upper, width * j, width * i, up) + return mul(mul(lower, diagonal), upper) + + +def schur(t, a, b): + out = block(t, a, b, a, b) + if a: + out = sub(out, mul(mul(block(t, a, b, 0, a), + inv(block(t, 0, a, 0, a))), block(t, 0, a, a, b))) + return out + + +def unit_upper(t, width): + size = len(t) + out = eye(size) + for end in range(width, size, width): + solve = mul(inv(block(t, 0, end, 0, end)), block(t, 0, end, end, size)) + put(out, end - width, end, block(solve, end - width, end, 0, size - end)) + return out + + +def interval_trees(n): + # Each record is (start, end, split); split=0 denotes a leaf. + require(1 <= n <= MAX_N, 'logical dimension capacity') + levels = {1: [((0, 1, 0),)]} + for size in range(2, n + 1): + shapes = [] + for cut in range(1, size): + for left, right in product(levels[cut], levels[size - cut]): + shifted = tuple((a + cut, b + cut, s + cut if s else 0) + for a, b, s in right) + shapes.append(left + shifted + ((0, size, cut),)) + require(len(shapes) <= MAX_TREES, 'tree capacity') + levels[size] = shapes + return levels[n] + + +def program(t, tree, width): + size = len(t) + info, atoms = {}, [] + for a, b, split in tree: + x, y = width * a, width * b + matrix = schur(t, x, y) + if not split: + atom = eye(size) + put(atom, x, x, matrix) + number = len(atoms) + atoms.append(atom) + info[a, b] = {'mask': 1 << number, 'states': [0, 1 << number], + 'order': [number], 'split': 0} + continue + mid = width * split + pivot = inv(block(matrix, 0, mid - x, 0, mid - x)) + upper, lower = eye(size), eye(size) + put(upper, x, mid, mul(pivot, block(matrix, 0, mid - x, mid - x, y - x))) + put(lower, mid, x, mul(block(matrix, mid - x, y - x, 0, mid - x), pivot)) + up, low = len(atoms), len(atoms) + 1 + atoms.extend((upper, lower)) + left, right = info[a, split], info[split, b] + full = (1 << up) | (1 << low) | left['mask'] | right['mask'] + states = [0] + [(1 << up) | l | r for l, r in + product(left['states'], right['states'])] + [full] + require(len(states) <= MAX_STATES and len(set(states)) == len(states), + 'state capacity or uniqueness') + info[a, b] = {'mask': full, 'states': states, 'split': split, + 'order': [up] + left['order'] + right['order'] + [low]} + return info, atoms + + +def partition(info, n, state): + pending, out = [(0, n)], [] + for _ in range(2 * n - 1): + if not pending: + break + a, b = pending.pop() + node = info[a, b] + selected = state & node['mask'] + if selected in (0, node['mask']): + out.append((a, b, selected != 0)) + else: + split = node['split'] + require(a < split < b, 'partial leaf') + pending.extend(((split, b), (a, split))) + require(not pending, 'partition capacity') + validate_partition(out, n) + return out + + +def validate_partition(parts, n): + require(1 <= len(parts) <= n, 'partition count') + end = 0 + for a, b, finished in parts: + require(a == end and a < b <= n and type(finished) is bool, 'partition interval') + end = b + require(end == n, 'partition coverage') + + +def literal(atoms, order, state, size): + out = eye(size) + for number in order: + if state & (1 << number): + out = mul(atoms[number], out) + return out + + +def block_forward(t, parts, width): + size = len(t) + out = zeros(size, size) + for a0, b0, finished in parts: + a, b = width * a0, width * b0 + if finished: + row = block(t, a, b, a, size) + if a: + row = sub(row, mul(mul(block(t, a, b, 0, a), + inv(block(t, 0, a, 0, a))), block(t, 0, a, a, size))) + put(out, a, a, row) + else: + put(out, a, a, eye(b - a)) + if b < size: + solve = mul(inv(block(t, 0, b, 0, b)), block(t, 0, b, b, size)) + put(out, a, b, block(solve, a, b, 0, size - b)) + return out + + +def block_inverse(t, parts, width): + size = len(t) + out = zeros(size, size) + for a0, b0, finished in parts: + a, b = width * a0, width * b0 + if finished: + put(out, 0, a, block(inv(block(t, 0, b, 0, b)), 0, b, a, b)) + else: + put(out, a, a, eye(b - a)) + if a: + solve = mul(inv(block(t, 0, a, 0, a)), block(t, 0, a, a, b)) + put(out, 0, a, [[-v for v in row] for row in solve]) + return out + + +def factorized(t, upper, parts, width): + size = len(t) + ub, eb = zeros(size, size), zeros(size, size) + for a0, b0, finished in parts: + a, b = width * a0, width * b0 + put(ub, a, a, block(upper, a, b, a, b)) + put(eb, a, a, schur(t, a, b) if finished else eye(b - a)) + return mul(mul(eb, inv(ub)), upper), ub, eb + + +def check_state(t, upper, parts, width, p, pinv, lam, q, counts): + size, chi = len(t), lam * q + s = lam + lam * lam * q + predicted, ub, eb = factorized(t, upper, parts, width) + require(p == predicted, 'ordered frontier formula') + require(p == block_forward(t, parts, width), 'block row formula') + require(pinv == block_inverse(t, parts, width), 'inverse block column formula') + require(pinv == mul(mul(inv(upper), ub), inv(eb)), 'inverse factor order') + counts['matrix_identities'] += 4 + c = sum(finished for _, _, finished in parts) + u = len(parts) - c + require(norm_squared_at_most(p, c * s * s + u * (1 + chi * chi)), 'forward bound') + require(norm_squared_at_most(pinv, c * q * q + u * (1 + chi * chi)), 'inverse bound') + counts['spectral_certificates'] += 2 + for a0, b0, finished in parts: + a, b = width * a0, width * b0 + row, col = block(p, a, b, 0, size), block(pinv, 0, size, a, b) + rb = s * s if finished else 1 + chi * chi + cb = q * q if finished else 1 + chi * chi + require(norm_squared_at_most(row, rb), 'individual row bound') + require(norm_squared_at_most(col, cb), 'individual column bound') + counts['spectral_certificates'] += 2 + counts['partition_blocks'] += 1 + wrong_order = mul(mul(upper, inv(ub)), eb) != p + missing_endpoint = mul(inv(ub), upper) != p + wrong_sign = False + for a0, b0, finished in parts: + if a0 and not finished: + a, b = width * a0, width * b0 + mutant = [row[:] for row in pinv] + put(mutant, 0, a, [[-v for v in row] for row in block(pinv, 0, a, a, b)]) + wrong_sign |= mutant != pinv + return wrong_order, missing_endpoint, wrong_sign + + +def rejected(call): + try: + call() + except ValueError: + return + raise ValueError('control did not reject') + + +def controls(): + rejected(lambda: inv([[F(0)]])) + rejected(lambda: validate_partition([(0, 1, False), (2, 3, True)], 3)) + rejected(lambda: validate_partition([(0, 2, False), (1, 3, True)], 3)) + require(not psd([[F(0), F(1)], [F(1), F(0)]]), 'zero pivot PSD control') + require(not psd([[F(-1)]]), 'negative PSD control') + require(not norm_squared_at_most([[F(2)]], F(3)), 'spectral control') + # Well-conditioned endpoint, but a badly conditioned first leading section. + t = [[F(1, 128), F(1)], [F(1), F(0)]] + require(norm_squared_at_most(t, F(4)), 'whole endpoint norm control') + require(norm_squared_at_most(inv(t), F(4)), 'whole inverse norm control') + prefix = [[F(1), F(128)], [F(0), F(1)]] + require(not norm_squared_at_most(prefix, F(4 * 2 * 4 ** 4)), 'leading premise control') + require(inv(block(t, 0, 1, 0, 1))[0][0] == 128, 'leading inverse witness') + # A punctured triangular restriction is not a contiguous interval. + u = [[F(1), F(1), F(0)], [F(0), F(1), F(1)], [F(0), F(0), F(1)]] + require(inv(u)[0][2] != inv([[u[0][0], u[0][2]], [u[2][0], u[2][2]]])[0][1], + 'noncontiguous restriction control') + return 8 + + +def run(): + counts = {'fixtures': 0, 'trees': 0, 'states': 0, 'partition_blocks': 0, + 'matrix_identities': 0, 'spectral_certificates': 0, + 'wrong_order_witnesses': 0, 'missing_endpoint_witnesses': 0, + 'wrong_sign_witnesses': 0} + for n, width in product(range(1, MAX_N + 1), (1, 2)): + t = fixture(n, width) + size = len(t) + lam = envelope(t) + q = max(envelope(inv(block(t, 0, k, 0, k))) + for k in range(width, size + 1, width)) + require(norm_squared_at_most(t, lam * lam), 'root admission') + for k in range(width, size + 1, width): + require(norm_squared_at_most(inv(block(t, 0, k, 0, k)), q * q), 'leading admission') + upper = unit_upper(t, width) + counts['fixtures'] += 1 + for tree in interval_trees(n): + info, atoms = program(t, tree, width) + root = info[0, n] + require(literal(atoms, root['order'], root['mask'], size) == t, 'atomic endpoint') + for state in root['states']: + parts = partition(info, n, state) + p = literal(atoms, root['order'], state, size) + pinv = inv(p) + wrong, missing, sign = check_state(t, upper, parts, width, p, pinv, lam, q, counts) + counts['wrong_order_witnesses'] += int(wrong) + counts['missing_endpoint_witnesses'] += int(missing) + counts['wrong_sign_witnesses'] += int(sign) + counts['states'] += 1 + counts['trees'] += 1 + require(counts['wrong_order_witnesses'] > 0, 'wrong-order control exercised') + require(counts['missing_endpoint_witnesses'] > 0, 'finished-endpoint control exercised') + require(counts['wrong_sign_witnesses'] > 0, 'inverse-sign control exercised') + counts['controls'] = controls() + 3 + return counts + + +def main(): + counts = run() + root = Path(__file__).resolve().parent + hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in FILES} + print(json.dumps({'status': 'PASS_DOWNSET_BLOCK_SOLVE', 'claim_type': 'scoped proof', + 'finite_evidence': counts, 'source_sha256': hashes, + 'no_new_kappa': True}, sort_keys=True)) + + +if __name__ == '__main__': + main()