From 99df7cf237f7fdc801501afea3347f5ef9f74704 Mon Sep 17 00:00:00 2001 From: James Reed Date: Wed, 21 Oct 2026 17:42:51 -0700 Subject: [PATCH] Record the Schur row margin at the 10 p^2 ceiling Co-authored-by: Cursor --- research/gaussian-schur-gap/README.md | 139 ++++++++++++++++++ research/gaussian-schur-gap/SOURCES.json | 42 ++++++ research/gaussian-schur-gap/TASK.json | 74 ++++++++++ research/gaussian-schur-gap/VERIFY.json | 24 ++++ research/gaussian-schur-gap/verify.py | 174 +++++++++++++++++++++++ 5 files changed, 453 insertions(+) create mode 100644 research/gaussian-schur-gap/README.md create mode 100644 research/gaussian-schur-gap/SOURCES.json create mode 100644 research/gaussian-schur-gap/TASK.json create mode 100644 research/gaussian-schur-gap/VERIFY.json create mode 100644 research/gaussian-schur-gap/verify.py diff --git a/research/gaussian-schur-gap/README.md b/research/gaussian-schur-gap/README.md new file mode 100644 index 0000000000..4ff3e12b7f --- /dev/null +++ b/research/gaussian-schur-gap/README.md @@ -0,0 +1,139 @@ +# Schur complements keep a row margin of 1/(10 p^2) + +**Claim type:** one elimination lemma, plus the exponent arithmetic it feeds. +**No new κ.** The ideal gaps stay hypotheses. The selected record remains +`23/10000`. + +## Question + +#4462 transferred the exponents 11, 24, 26, 26 and 6 to the whole banded +reference, with inverse bound `10 p^2` in its robust reading. Its open +question asks whether those exponents survive the Schur complement. The +first step named there is to restate the interior-elimination row gap with +`10 p^2` in place of `16 p^2 - 1`. + +## Lemma + +Let `p ≥ 2` be an integer and let `δ = 1/(10 p^2)`. Suppose `H` has diagonal +entries equal to 1, and every row and every column has absolute off-sum at +most `1 - δ`. Let `S` be the Schur complement of any principal set whose +pivots stay nonzero. + +Then every row and every column of `S` has margin at least `δ`, and absolute +sum at most `2 - δ`. In particular + +```text +||S^{-1}||_1 ≤ 10 p^2, ||S^{-1}||_∞ ≤ 10 p^2, ||S||_2 < 2, +``` + +and the same holds for `||S^{-1}||_2`. The polynomial used in #4452, with +spectral endpoint 11, therefore satisfies +`||P - S^{-1}||_2 < p^6 exp(-p^2)` on this complement. Its bandwidth is at +most `(2 p^{24} - 1) W < p^{26}` for every integer `W ≤ p - 1`, and a row at +distance `p^{26}` from a section edge agrees with the block row. + +So 11, 24, 26, 26 and 6 apply to every such Schur complement. Replacing +`10 p^2` by `16 p^2 - 1` does not: at `p = 2` that ceiling squares to +`3969 > 2048 = 2^{11}`. + +## Proof + +Write `δ` for the margin. The hypothesis gives, on the original matrix, +margin `1 - off-sum ≥ δ` and absolute row sum `1 + off-sum ≤ 2 - δ`. The +same holds for columns. Proceed by eliminating one index at a time. The +active diagonal `d` and off-sum `o` of a remaining row satisfy `d - o ≥ δ`, +and the active absolute row sum `d + o` is at most `2 - δ`. The pivot +diagonal `a` satisfies `a ≥ δ`, so it is not zero. A coupling entry has +absolute value `c`, and the pivot row has off-sum `o1 ≤ a - δ`. + +The new row is the old row minus `c/a` times the pivot row. The triangle +inequality produces a lower bound `L` for the new margin and an upper bound +`U` for the new absolute row sum: + +```text +a L = a d - a (o - c) - c o1 = a (d - o) + c (a - o1), +a U = a (d + o) + c (o1 - a). +``` + +The first right-hand side is at least `a δ`, so `L ≥ δ`. The second says +`U = (d + o) - c (a - o1) / a ≤ d + o`. Thus the new margin is at least `δ` +and the new absolute row sum is at most the old one, hence at most `2 - δ`. +Columns are the rows of the transpose, so the same two identities apply to +them. After the whole set has been eliminated, the active matrix is the +block Schur complement `D - C A^{-1} B`. + +The bound `||S^{-1}||_∞ ≤ 1/δ` is the one-row estimate: if `S y = x` and +`|y_k|` is maximal, the margin at `k` multiplies `|y_k|` by at most `||x||_∞`. +The same estimate on `S^*` bounds the 1-norm. Therefore both inverse norms +are at most `10 p^2`, and the 2-norm is at most `10 p^2`. Absolute row and +column sums at most `2 - δ` give `||S||_2 < 2`. + +The eigenvalues of `S^* S` are then strictly larger than `p^{-11}` and +strictly smaller than 4. Indeed `(10 p^2)^2 = 100 p^4`, and `100 < p^7` for +every integer `p ≥ 2` because the minimum is `128` at `p = 2`. Also +`4 < p^{11}`. The matrix `Q = I - p^{-11} S^* S` has spectrum in +`[0, 1 - p^{-22})`. The length `p^{24}` contributes `p^2`. The length +`p^{23}` contributes only `p`. The scalar step is strict because `1/2! < 1`. +The normalizer 6 is legal because `10 p^2 < p^6`, while `10 p^2 > p^5` at +`p = 2`, so 5 fails. The bandwidth identity is the same one used for the +within-cell block: + +```text +p^{26} - (2 p^{24} - 1)(p - 1) = p^{24} ((p - 1)^2 + 1) + p - 1 > 0. +``` + +At `p = 2` the loose radius equals `p^{25} + 1`. For every integer `p ≥ 3` +the sharp radius at `W = p - 1` exceeds `p^{25}`. + +#4462's robust margin `(4p - 1)/(32 p^3)` is at least `7/(64 p^2)`, and +`7/64 > 1/10`, so that margin is at least `δ`. Those matrices meet the +hypothesis of this lemma. This package does not reprove the robust margin. + +| Role | With margin `1/(16 p^2 - 1)` | With margin `1/(10 p^2)` | +| --- | --- | --- | +| Inverse ceiling | `16 p^2 - 1` | `10 p^2` | +| Spectral endpoint on the Schur complement | 12, because `63^2 > 2^{11}` | 11 | +| Series, bandwidth, agreement, normalizer | 26, 28, 28, 6 | 24, 26, 26, 6 | + +## Not covered + +- A proof that the ideal gaps exceed `1/(8 p^2)` for every prime. +- The core side `L = 2^{ceil(400 log2 p)}`. Agreement distance 26 does not + by itself replace that choice. +- The broad matrix. HALO still applies `S` and does not invert it. +- Any new κ. The #4100 notes keep their written gap, `p^{10}`, and `A = p^{48}`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-schur-gap --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-schur-gap +``` + +Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection +refresh κ = `23/10000`. + +Overlap on 2026-10-22, from the snapshot fetched at 00:40 UTC, matched this +draft, PR #4462, and the unrelated width-2 note +`research/gaussian-origin-displayed`. #4462 asks for this elimination step +and does not take it. No other open pull request assigns the margin +`1/(10 p^2)` to a Schur complement. A search miss is not a novelty +certificate. #4452 is the within-cell δ ceiling. + +## Open next questions + +1. **Can the core side exponent 400 fall?** Every Schur complement now has + the same inverse ceiling `10 p^2`, and the agreement distance on the + halo polynomial is `p^{26}`. HALO still chooses `L ≥ p^{400}` against + `A = p^{48}`. The first step is to substitute `A = p^{26}` into the two + sparse powers and name the smallest uniform integer that keeps both + negative whenever the group exponents are strictly less than 1. + +## Credit + +- The elimination sentence and the written core side are #4100's. +- The inverse-ceiling `10 p^2`, and this question, are Ryanson Jonathan's #4462. +- The exponent route is #4452. The across-cell contract it used is Mihir S's #4449. +- The sharp bandwidth radius is Nick Petalas's halo audit, PR #4217. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-schur-gap/SOURCES.json b/research/gaussian-schur-gap/SOURCES.json new file mode 100644 index 0000000000..d9b8b8233c --- /dev/null +++ b/research/gaussian-schur-gap/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + }, + { + "path": "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "usage": "input", + "git_blob": "3853ffac91dfed5421b05533eb274a8646741071", + "sha256": "be3e4b729481b15a5ccc286b297908e4f9cef94c0c9144a28ee1cf58950d142a" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + } + ] +} diff --git a/research/gaussian-schur-gap/TASK.json b/research/gaussian-schur-gap/TASK.json new file mode 100644 index 0000000000..73bf966c7e --- /dev/null +++ b/research/gaussian-schur-gap/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "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": "Decide whether a unit-diagonal matrix with row and column margins at least 1/(10 p^2) passes that margin, and the exponents 11, 24, 26, 26 and 6, to every principal Schur complement.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only restates the interior-elimination gap at the 10 p^2 ceiling. It does not lower the core side 400 and does not claim a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. The Schur margin is the elimination input to the halo polynomial, still under the eventual ideal-gap hypothesis.", + "budget_minutes": 60, + "stop_rule": "Stop once the Schur margin is compared with 10 p^2 and with 16 p^2-1. Do not retune the core side 400, do not edit the #4100 notes, and do not claim a new kappa.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-schur-gap", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the elimination identities and the package text.", + "open_questions": [ + { + "question": "Can HALO's core side exponent 400 fall once every Schur complement has inverse bound 10 p^2 and the agreement distance is p^{26}?", + "why_it_matters": "The written core side is still p^{400} against agreement distance p^{48}. The elimination gap no longer forces the larger inverse ceiling.", + "first_step": "Substitute A = p^{26} into HALO's two sparse powers and name the smallest uniform integer that keeps both negative for group exponents strictly less than 1.", + "blocked_by": "The ideal gaps 1/(8 p^2) remain eventual statements, so the margin hypothesis is still conditional." + } + ] +} diff --git a/research/gaussian-schur-gap/VERIFY.json b/research/gaussian-schur-gap/VERIFY.json new file mode 100644 index 0000000000..70fb619f6b --- /dev/null +++ b/research/gaussian-schur-gap/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "One Schur step preserves a margin of 1/(10 p^2), so 11, 24, 26, 26 and 6 apply to the complement; 10, 23, 25 and 5 fail, and 16 p^2-1 does not give endpoint 11 at p=2." + } + ] +} diff --git a/research/gaussian-schur-gap/verify.py b/research/gaussian-schur-gap/verify.py new file mode 100644 index 0000000000..27b578a1a8 --- /dev/null +++ b/research/gaussian-schur-gap/verify.py @@ -0,0 +1,174 @@ +#!/usr/bin/env python3 +"""Row-dominance margins survive a Schur step, and 10 p^2 keeps the exponents. + +Every comparison is an integer or polynomial identity. The ideal gaps are hypotheses. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-schur-gap" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def add(left, right): + out = dict(left) + for key, coeff in right.items(): + out[key] = out.get(key, 0) + coeff + if out[key] == 0: + del out[key] + return out + + +def scale(poly, factor): + return {key: factor * coeff for key, coeff in poly.items() if factor * coeff} + + +def mul_uni(left, right): + out = {} + for degree, coeff in left.items(): + for other, factor in right.items(): + key = degree + other + out[key] = out.get(key, 0) + coeff * factor + return {key: coeff for key, coeff in out.items() if coeff} + + +def mul(left, right): + out = {} + for left_key, left_coeff in left.items(): + for right_key, right_coeff in right.items(): + key = tuple(left_key[i] + right_key[i] for i in range(len(left_key))) + out[key] = out.get(key, 0) + left_coeff * right_coeff + return {key: coeff for key, coeff in out.items() if coeff} + + +def mono(exponent, coeff=1): + return {exponent: coeff} + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + assert digest(ROOT / row["path"]) == row["sha256"], row["path"] + halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8") + gaussian = (ROOT / "research/unconditional-batched-crt/GAUSSIAN.md").read_text( + encoding="utf-8" + ) + conditioning = ( + ROOT / "research/unconditional-batched-crt/INVERSE-CONDITIONING.md" + ).read_text(encoding="utf-8") + fine = (ROOT / "research/unconditional-batched-crt/vendor/FINE-PRIME.md").read_text( + encoding="utf-8" + ) + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "L=2^ceil(400 log2 p)" in halo + assert "For A=p^48, L>=p^400" in halo + assert "S=D-C A^-1 B; do not solve with S^-1" in halo + assert "strict row diagonal dominance survives every\nelimination with at least the original row gap" in gaussian + assert "complementary Schur inverse is the corresponding\nprincipal block of T^-1" in conditioning + assert "The Schur complement itself is bounded by D-C A^-1 B" in conditioning + assert "its Schur complements retain that gap." in fine + assert selected["kappa"] == "23/10000" + + +def elimination_identities() -> None: + # Variables a, d, o, c, o1. The cleared one-step identities are identically zero. + a = mono((1, 0, 0, 0, 0)) + d = mono((0, 1, 0, 0, 0)) + o = mono((0, 0, 1, 0, 0)) + c = mono((0, 0, 0, 1, 0)) + o1 = mono((0, 0, 0, 0, 1)) + # a(L-delta) = a(d-o-delta) + c(a-o1), so the delta terms were already cleared + # into the two margin factors. The polynomial below is a*L_cleared minus that sum, + # with L_cleared = a*d - a*(o-c) - c*o1 and delta removed from both sides. + cleared_margin = add( + add(mul(a, d), scale(mul(a, add(scale(o, -1), c)), 1)), + scale(mul(c, o1), -1), + ) + claimed_margin = add(mul(a, add(d, scale(o, -1))), mul(c, add(a, scale(o1, -1)))) + assert add(cleared_margin, scale(claimed_margin, -1)) == {} + # a(U - (d+o)) = c(o1-a). + cleared_sum = add( + add(add(mul(a, d), mul(a, o)), scale(mul(a, c), -1)), + mul(c, o1), + ) + claimed_sum = add(mul(a, add(d, o)), mul(c, add(o1, scale(a, -1)))) + assert add(cleared_sum, scale(claimed_sum, -1)) == {} + # Integer witness. Pivot 40, diagonal 40, off-sums 36 and 30, coupling 6. + # The current margin equals 4, so the cleared slack is the coupling term only. + pivot, diagonal, off, coupling, pivot_off = 40, 40, 36, 6, 30 + margin_product = pivot * (diagonal - off) + coupling * (pivot - pivot_off) + raw = pivot * diagonal - pivot * (off - coupling) - coupling * pivot_off + assert raw == margin_product == 220 + assert raw - pivot * (diagonal - off) == coupling * (pivot - pivot_off) == 60 + row_raw = pivot * (diagonal + off - coupling) + coupling * pivot_off + previous = pivot * (diagonal + off) + assert previous - row_raw == coupling * (pivot - pivot_off) == 60 + + +def ceilings() -> None: + # 10 p^2 against p^5 and p^6 at p=2, and its square against p^{10} and p^{11}. + assert 10 * 4 == 40 + assert 2 ** 5 == 32 + assert 40 > 32 + assert 2 ** 6 == 64 + assert 40 < 64 + assert 100 * (2 ** 4) == 1600 + assert 2 ** 10 == 1024 + assert 1600 > 1024 + assert 2 ** 7 == 128 + assert 100 < 128 + assert 2 ** 11 == 2048 + assert 1600 < 2048 + assert 2 ** 4 == 16 + assert 10 < 16 + assert 4 < 2048 + assert 1 < 2 + # The older ceiling 16p^2-1 has square 3969 > 2048 at p=2, so endpoint 11 fails. + assert 16 * 4 - 1 == 63 + assert 63 * 63 == 3969 + assert 3969 > 2048 + # #4462's margin (4p-1)/(32 p^3) is at least 7/(64 p^2), hence at least 1/(10 p^2). + assert 7 * 10 > 64 + cubic = add(scale({3: 1}, 32), {2: -64}) + factored = mul_uni({2: 32}, {1: 1, 0: -2}) + assert cubic == factored == {3: 32, 2: -64} + assert 32 * 4 * (2 - 2) == 0 + assert 32 * 9 * (3 - 2) == 32 * 9 + + +def exponents() -> None: + quadratic = add(mul_uni({1: 1, 0: -1}, {1: 1, 0: -1}), {0: 1}) + assert quadratic == {2: 1, 1: -2, 0: 2} + factored = add(mul_uni({24: 1}, quadratic), {1: 1, 0: -1}) + sharp = mul_uni({24: 2, 0: -1}, {1: 1, 0: -1}) + margin = add({26: 1}, scale(sharp, -1)) + assert factored == margin + assert margin == {26: 1, 25: -2, 24: 2, 1: 1, 0: -1} + assert 24 - 22 == 2 + assert 23 - 22 == 1 + assert 2 * (2 ** 24) + 1 == 2 ** 25 + 1 + assert 2 ** 25 + 1 > 2 ** 25 + assert (2 * (3 ** 24) - 1) * (3 - 1) > 3 ** 25 + + +def main() -> None: + pins_and_phrases() + elimination_identities() + ceilings() + exponents() + print("PASS_GAUSSIAN_SCHUR_GAP") + + +if __name__ == "__main__": + main()