diff --git a/research/gaussian-twonorm-guard/README.md b/research/gaussian-twonorm-guard/README.md new file mode 100644 index 0000000000..f457c44533 --- /dev/null +++ b/research/gaussian-twonorm-guard/README.md @@ -0,0 +1,103 @@ +# The written p^10 guards do not move + +**Scoped ledger comparison for #4100's narrow inverse 2-norm. No new κ.** +This decides open question 2 of #4402. It does not prove a column gap for +`GAUSSIAN.md`'s rounded reference `H`. + +## Question + +`INVERSE-CONDITIONING.md` bounds the inverse 2-norm by + +```text +sqrt((1/delta)(1/delta + 2 b rho/delta^2)). +``` + +#4402 replaces that, inside one phase run, by `1/sqrt(delta delta_col)`. +Do any written precision guards in the #4100 notes change? + +## Callers and the exponents they write + +The search is the note directory `research/unconditional-batched-crt` on +canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`. Older vendored +copies of the fine-prime note are the same inherited statement, not a second +ledger. + +| Note | Role | Exponents | +| --- | --- | --- | +| `INVERSE-CONDITIONING.md` | States the bandwidth formula. For this route it records `b < p` and `delta >= 1/(16p^2)`. | No separate power of `p`. | +| `GAUSSIAN.md`, narrow paragraph | Applies the formula to `Haug` and its principal sections. | Both 2-norms `< p^10` eventually. | +| `GAUSSIAN.md`, broad paragraph | Shifted-symbol bound. It does not use the bandwidth formula. | `< p^6`, with the `p^10` allowance called ample. | +| `GAUSSIAN.md`, locality and normalizer | Repeats HALO's consequences and divides completed maps by a dyadic bound. | `p^-20`, `p^42`, `p^45`, error `p^10 exp(-p^2)`, `p^48`, `p^100`. | +| `HALO.md` | Assumes both 2-norms are at most `p^10` and bandwidth `< p`. | Spectral interval `[p^-20, p^20]`, gap `p^-40`, `J = ceil(p^42)`, bandwidth `< p^45`, error `p^10 exp(-p^2)`, `A = ceil(p^48)`, core `L >= p^400`. | +| `vendor/FINE-PRIME.md` §§4–5 | Inherited hypothesis `\|\|H\|\|_2, \|\|H^-1\|\|_2 <= p^10`. | `2^ceil(100 log2 p)`, the same halo exponents through `p^48`, and core exponent 128. | +| `PROOF.md` | Uses the halo/core pair already chosen above. | Core exponent 400 and halo 48. It does not restate `p^10`. | +| `AUDIT.md` | Names the conditioning notes. | No `p^10`. | + +## Comparison + +Take an integer `p >= 2`, bandwidth `b <= p - 1`, `delta >= 1/(16p^2)` and +`rho = 1 - delta`. These are the floors the notes give the lemma. At that +corner the squared bandwidth ceiling equals + +```text +256 p^4 (1 + 2(p-1)(16p^2 - 1)). +``` + +The parenthesis expands as `32p^3 - 32p^2 - 2p + 3`, which is strictly below +`32p^3`. The resulting square is strictly below `p^20`, so the 2-norm ceiling +is strictly below `p^10`. The same corner is already at least `p^18` when +`p = 2`, so no smaller single exponent stays under the ceiling for every +integer `p >= 2`. The forward 2-norm square is strictly below `4p`, which is +also below `p^20`. + +If `delta_col` meets the same floor, the column-gap ceiling is at most +`16p^2`, and `(16p^2)^2 = 256 p^4` is strictly below `p^20` as well. + +Every later exponent in the table is a consequence of the hypothesis that +both 2-norms are at most `p^10`. Both ceilings satisfy that hypothesis, so +none of those exponents has to increase. This package does not decrease them. + +For every integer `p >= 19` the slack is larger than the notes use. At the +`p = 19` corner the squared bandwidth ceiling is `6936029752576`, below +`19^12`, so the 2-norm ceiling is below `p^6`. The column-gap ceiling is +`5776`, below `19^3`. Their squared ratio is `207901`, below `19^6`. The +room from that bandwidth ceiling up to `p^20` is more than a factor `p^8`. + +The broad `p^6` / `p^10` sentence is a different argument and does not read +the bandwidth term. + +## What this does not say + +- It does not prove `delta_col >= 1/(16p^2)` for the rounded matrix `H`. + Cross-cut entries, truncation and rounding stay where #4402 left them. +- It does not say the section error, the halo, or a multiplication exponent + moves. The selected κ is unchanged: + `836330098538459/500000000000000000`. +- Upstream pin: main `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority + revision 7, checked 2026-10-21T16:32:11Z. Overlap refresh + 2026-10-21T16:33:25Z covered 507 open PR bodies and 3240 discussions. + The live neighbor is #4402. Claim: + https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19102318 + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-twonorm-guard +``` + +## Open next questions + +If both 2-norms are assumed only up to `16p^2`, which of HALO's exponents +20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease while keeping +the same error and coverage conclusions? A decrease would be a ledger edit. +It is not required for correctness, and it still would not apply to `H` +until the column gap survives phase cuts, truncation and rounding. + +## Credit + +The conditioning lemma, the `p^10` guards and the halo exponents are #4100's. +The column-gap question is pinterbanget's, in #4402, from #4336. The narrow +kernel comes from PR1673 (Vlado Vojdanovski). + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. No +independent human review. Apache-2.0. diff --git a/research/gaussian-twonorm-guard/SOURCES.json b/research/gaussian-twonorm-guard/SOURCES.json new file mode 100644 index 0000000000..63b9e037a9 --- /dev/null +++ b/research/gaussian-twonorm-guard/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/AUDIT.md", + "usage": "input", + "git_blob": "cd59c5e786a3d37de027b8d0f7376fbb00d52efd", + "sha256": "2a6c84ba32c6febee0cbc205210a8935c481d40ec1d52d621442e03221cacc3d" + }, + { + "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/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + } + ] +} diff --git a/research/gaussian-twonorm-guard/TASK.json b/research/gaussian-twonorm-guard/TASK.json new file mode 100644 index 0000000000..254edf150c --- /dev/null +++ b/research/gaussian-twonorm-guard/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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 #4100's written precision guards change when the inverse 2-norm input drops from INVERSE-CONDITIONING.md's bandwidth form to 1/sqrt(delta delta_col), listing each caller and exponent in research/unconditional-batched-crt.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This comparison stays inside the written p^10 guards and GAUSSIAN.md's floors. It does not prove the column gap for the rounded matrix H.", + "bottleneck_link": "The selected frontier is unchanged. The comparison only classifies a precision guard inside the unselected #4100 construction.", + "budget_minutes": 60, + "stop_rule": "Stop after the caller list and the comparison with p^10. Do not prove cross-cut entries, do not retune HALO's exponents, and do not claim a new kappa.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-twonorm-guard", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the caller inventory, the exact comparison and the package text.", + "open_questions": [ + { + "question": "If both 2-norms are assumed only up to 16p^2, which of HALO's exponents 20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease while keeping the same error and coverage conclusions?", + "why_it_matters": "A decrease would change the halo and the normalizer. The present comparison shows those exponents need not increase, so a decrease is a separate ledger edit.", + "first_step": "Substitute the ceiling 16p^2 for p^10 in HALO's spectral interval and recompute the smallest integers J and A that keep the error at most exp(-p^2) and cover the polynomial bandwidth.", + "blocked_by": "None for that arithmetic. Applying a smaller exponent to H still requires the column gap after phase cuts, truncation and rounding." + } + ] +} diff --git a/research/gaussian-twonorm-guard/VERIFY.json b/research/gaussian-twonorm-guard/VERIFY.json new file mode 100644 index 0000000000..5a6648d73f --- /dev/null +++ b/research/gaussian-twonorm-guard/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/unconditional-batched-crt/AUDIT.md", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned caller phrases, the p=2 corner below p^10 and not below p^9, and the p=19 ceilings below p^6 and p^3." + } + ] +} diff --git a/research/gaussian-twonorm-guard/verify.py b/research/gaussian-twonorm-guard/verify.py new file mode 100644 index 0000000000..289450676f --- /dev/null +++ b/research/gaussian-twonorm-guard/verify.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""The written p^10 guards still cover both inverse 2-norm ceilings. + +Callers and exponents are read from the pinned #4100 notes. The comparison +uses exact integers. It does not prove a column gap for the rounded matrix H. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-twonorm-guard" +NOTES = ROOT / "research" / "unconditional-batched-crt" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load(name: str) -> str: + return (NOTES / name).read_text(encoding="utf-8") + + +def pins_match() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + expected = { + row["path"]: row["sha256"] + for row in sources["files"] + if row["usage"] == "input" + } + for path, sha in expected.items(): + assert digest(ROOT / path) == sha, path + + +def callers_write_these_exponents() -> None: + inverse = load("INVERSE-CONDITIONING.md") + gaussian = load("GAUSSIAN.md") + halo = load("HALO.md") + fine = load("vendor/FINE-PRIME.md") + proof = load("PROOF.md") + audit = load("AUDIT.md") + + assert "||H^-1||_infinity <= 1/delta," in inverse + assert "||H^-1||_1 <= 1/delta + 2 b rho/delta^2," in inverse + assert ( + "||H^-1||_2 <= sqrt((1/delta)(1/delta + 2 b rho/delta^2))." in inverse + ) + assert "establishes b

=1/(16p^2)" in inverse + + assert "row gap delta>=1/(16p^2) and row norm<2" in gaussian + assert "||H^-1||_1<=delta^-1+2w(1-delta)delta^-2." in gaussian + assert "less than p^10 eventually" in gaussian + assert "||K^-1||_2=p^400" in halo + assert "prove the p^10 narrow bounds" in halo + + assert "conservative common eventual bound p^10 covers" in fine + assert "2^ceil(100 log2 p)" in fine + assert "||H||_2,||H^-1||_2<=p^10" in fine + assert "Q=I-p^-20 H* H." in fine + assert "[0,1-p^-40]" in fine + assert "J=ceil(p^42)" in fine + assert "p^10 exp(-p^2)" in fine + assert "A=C_A p^48" in fine + assert "halo exponent 48 and core exponent 128" in fine + + assert "core exponent400 and halo48" in proof + assert "p^10" not in proof + assert "p^10" not in audit + assert "INVERSE-CONDITIONING.md bounds narrow principal restrictions" in audit + + selected = json.loads( + (ROOT / "certificates" / "selected-result.json").read_text(encoding="utf-8") + ) + assert selected["kappa"] == "836330098538459/500000000000000000" + + +def multiply(left: list[int], right: list[int]) -> list[int]: + """Product of polynomials, lowest degree first.""" + out = [0] * (len(left) + len(right) - 1) + for i, coeff in enumerate(left): + for j, other in enumerate(right): + out[i + j] += coeff * other + return out + + +def bracket_coefficients() -> list[int]: + """Coefficients of 1 + 2(p-1)(16p^2-1).""" + # (p-1)(16p^2-1) = 16p^3 - 16p^2 - p + 1, then double and add 1. + product = multiply([-1, 1], [-1, 0, 16]) + assert product == [1, -1, -16, 16] + doubled = [2 * coeff for coeff in product] + doubled[0] += 1 + assert doubled == [3, -2, -32, 32] + return doubled + + +def bracket(p: int) -> int: + coeffs = bracket_coefficients() + return sum(coeff * p**degree for degree, coeff in enumerate(coeffs)) + + +def corner_square(p: int) -> int: + """Squared bandwidth ceiling at b=p-1 and delta=1/(16p^2).""" + delta_den = 16 * p * p + rho_num = delta_den - 1 + inf = delta_den + # 2 b rho / delta^2 = 32 p^2 (p-1) (16p^2-1) + one_extra = 32 * p * p * (p - 1) * rho_num + return inf * (inf + one_extra) + + +def ceilings_stay_below_p10() -> None: + coeffs = bracket_coefficients() + # 32p^3 - bracket(p) = -3 + 2p + 32p^2. + difference = [-coeffs[0], -coeffs[1], -coeffs[2], 32 - coeffs[3]] + assert difference == [-3, 2, 32, 0] + # 16p^2 + p - 17 = (p-1)(16p+17), so the difference is + # 2(p-1)(16p+17) + 31 >= 31 for every integer p >= 1. + assert multiply([-1, 1], [17, 16]) == [-17, 1, 16] + assert [2 * coeff for coeff in [-17, 1, 16]] == [-34, 2, 32] + assert [-34 + 31, 2, 32] == [-3, 2, 32] + + for p in (2, 19): + assert corner_square(p) == 256 * p**4 * bracket(p) + assert 32 * p**3 - bracket(p) == 32 * p * p + 2 * p - 3 + + # At p=2 the loose multiple 8192 p^7 equals p^20, so the strict bracket + # step is what puts the corner below p^10. Exponent 9 does not. + assert 8192 * 2**7 == 2**20 + assert corner_square(2) < 2**20 + assert corner_square(2) >= 2**18 + assert 4 * 2 < 2**20 + assert (16 * 2 * 2) ** 2 < 2**20 + + # For p >= 3, 8192 < p^13, so even the loose multiple is below p^20. + assert 8192 < 3**13 + assert corner_square(3) < 8192 * 3**7 < 3**20 + + # From p=19 the bandwidth ceiling is already below p^6, the column-gap + # ceiling below p^3, and the squared ratio below p^6. + assert 8192 < 19**5 + assert bracket(19) == 207901 + assert corner_square(19) == 6936029752576 + assert corner_square(19) < 19**12 + assert 16 * 19 * 19 == 5776 < 19**3 + assert bracket(19) < 19**6 + assert 19**20 > corner_square(19) * 19**8 + assert 4 * 19 < 19**2 + + +def main() -> None: + pins_match() + callers_write_these_exponents() + ceilings_stay_below_p10() + print("p10 guards unchanged under both ceilings") + + +if __name__ == "__main__": + main()