diff --git a/research/gaussian-ratio-budget/README.md b/research/gaussian-ratio-budget/README.md new file mode 100644 index 0000000000..51ade7c94e --- /dev/null +++ b/research/gaussian-ratio-budget/README.md @@ -0,0 +1,114 @@ +# The published weight error meets the 1/(16p^2) ratio budget + +**Claim type:** a uniform relative-error comparison inside one cell. +**No new κ.** Across-cell rounding is outside this claim. The selected +record remains `23/10000`. + +## Question + +Downstream rounds each weight by a downward exponential routine with +absolute error below `4η`, where `P = 32768 p` and `η = 2^{-P}`, and it +records `2^{-8p} < a_j ≤ 1`. The within-cell entry is the ratio +`ahat_j Ghat_(j-l) / ahat_l`. Does that absolute error keep the ratio +inside the relative budget `ε ≤ 1/(16p^2)` for every integer `p ≥ 2`? + +## Lemma + +Let `p ≥ 2` be an integer. Suppose a true weight satisfies +`a > 2^{-8p}`, its repaired value satisfies `a - 4η < ahat ≤ a`, and a +repaired kernel coefficient satisfies `0 ≤ Ghat ≤ G`. Then each +within-cell off-diagonal entry obeys + +```text +ahat_j Ghat / ahat_l < (a_j G / a_l) / (1 - δ), +``` + +where `δ = 2^{2 - 32760 p}`. This `δ` is strictly less than `1/(16p^2)`. +The factor `1/(1-δ)` is therefore strictly smaller than +`1/(1 - 1/(16p^2))`. + +## Proof + +The downward kernel bound and the downward numerator give + +```text +ahat_j Ghat / ahat_l ≤ (a_j / ahat_l) G. +``` + +The denominator satisfies `ahat_l > a_l - 4η`. The room `4η < 2^{-8p}` is +the comparison `32760 p > 2`, since `32768 - 8 = 32760` and `4 = 2^2`. +Thus `ahat_l > 0` and + +```text +a_l / ahat_l < 1 / (1 - 4η/a_l) < 1 / (1 - 4η/2^{-8p}) = 1/(1-δ). +``` + +The exponent of `δ` is `2 + 8p - 32768p = 2 - 32760p`. + +It remains to prove `16 p^2 δ < 1`. First, `p^2 < 2^{2p}` for every +integer `p ≥ 2`. The base is `4 < 16`. If it holds at `p`, the next square +obeys `4(p+1)^2 ≤ 9 p^2`: the difference `4(p+1)^2 - 9p^2 = -5p^2 + 8p + 4` +is 0 at `p = 2`, and raising `p` by one changes it by `-10p + 3`, which is +already `-17` at `p = 2` and becomes more negative. Since `9 < 16`, + +```text +(p+1)^2 ≤ (9/4) p^2 < 4 p^2 < 4 · 2^{2p} = 2^{2(p+1)}. +``` + +Second, `2p < 32760 p - 6` for every integer `p ≥ 2`. At `p = 2` the +slack is positive, and it increases by `32758` at each later integer. +Therefore `2^{2p} < 2^{32760 p - 6}`, and `p^2 < 2^{32760 p - 6}`. +Multiplying by the remaining power of two, + +```text +16 p^2 δ < 16 · 2^{2-6} = 2^4 · 2^{-4} = 1. +``` + +The inequality is strict because both comparisons above are strict. At +`p = 2` the same exponent is concrete: `4 < 2^{65514}`. + +So the relative weight error `ρ = 4η/a` satisfies `ρ < δ < 1/(16p^2)`, +which is the budget used for the within-cell factor `1/(1-ε)`. The gauge +audit's allowance `ε ≤ 1/2` is a larger number. At `p = 2`, +`1/2 > 1/64 = 1/(16·4)`. + +## Not covered + +- Across-cell entries. That rounding question is claimed separately. +- A proof that the ideal row and column gaps exceed `1/(8p^2)` for every + prime. The ratio bound above takes the true entry `a_j G / a_l` as given. +- The halo exponents. Meeting `ε ≤ 1/(16p^2)` is the budget comparison, + not a new assignment of 12, 26, 28 or 6. +- Any new κ, and any edit to the #4100 notes. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-ratio-budget --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-ratio-budget +``` + +Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection +refresh κ = `23/10000`. + +Overlap on 2026-10-21: discussion 4444 claims the across-cell two-ulp +repair left open by #4442. This package is the within-cell ratio under the +published absolute error. A search hit is not a novelty certificate. + +## Open next questions + +1. **Do 12, 26, 28, 28 and 6 now apply inside one cell for every integer + `p ≥ 2`, with this `δ` in place of a separate `ε` hypothesis?** The + ratio factor is strictly stronger than `1/(1 - 1/(16p^2))`. The ideal + gaps `1/(8p^2)` are still the eventual statements in GAUSSIAN and + #4402. The first step is to substitute `δ = 2^{2-32760p}` into the + within-cell ceiling arithmetic. + +## Credit + +- The absolute error `4η`, the weight floor `2^{-8p}`, and the ratio entry + are the phase-cell downstream note's. +- The budget `1/(16p^2)` is #4438. The within-cell exponents are #4439. +- The allowance `ε ≤ 1/2` is the capped-gauge audit's. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-ratio-budget/SOURCES.json b/research/gaussian-ratio-budget/SOURCES.json new file mode 100644 index 0000000000..261886d293 --- /dev/null +++ b/research/gaussian-ratio-budget/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": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "usage": "input", + "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841", + "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730" + }, + { + "path": "references/semantic-bulk/rad20/reports/review-phase-cell-inverse.md", + "usage": "input", + "git_blob": "395eab8ee1d58e84353f554dcfe9473b5913dda5", + "sha256": "113927dd4fb77a55a457bd5f6da8cbfc7262d0fbc4e9d708b591a1d632e6caf6" + }, + { + "path": "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md", + "usage": "input", + "git_blob": "a2d1c5ae923db7649627dbf419434e36267e57c6", + "sha256": "1030a34922709ab8d3434a4c57a4a58934ae268c237fb598cb415697da411c9f" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + } + ] +} diff --git a/research/gaussian-ratio-budget/TASK.json b/research/gaussian-ratio-budget/TASK.json new file mode 100644 index 0000000000..2ee67106fd --- /dev/null +++ b/research/gaussian-ratio-budget/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 the published absolute weight error below 4\u03b7 keeps a within-cell ratio inside \u03b5 \u2264 1/(16p^2) for every integer p \u2265 2.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only compares that published absolute error with the within-cell relative budget. The across-cell repair is claimed elsewhere, and this package does not claim a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. The ratio factor is the within-cell input to the 16p^2 ceiling.", + "budget_minutes": 60, + "stop_rule": "Stop once \u03b4 = 2^{2-32760p} is compared with 1/(16p^2). Do not redo the claimed across-cell repair, 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-ratio-budget", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the exponent comparison and the package text.", + "open_questions": [ + { + "question": "Do 12, 26, 28, 28 and 6 apply inside one cell for every integer p \u2265 2 once \u03b5 is replaced by \u03b4 = 2^{2-32760p}?", + "why_it_matters": "The published weight error is stronger than 1/(16p^2). The within-cell exponent proof still treats that larger budget as a hypothesis.", + "first_step": "Substitute \u03b4 into the within-cell ceiling and check whether 16p^2-1 is still the inverse bound.", + "blocked_by": "The ideal gaps 1/(8p^2) remain eventual statements, so the ceiling still depends on them." + } + ] +} diff --git a/research/gaussian-ratio-budget/VERIFY.json b/research/gaussian-ratio-budget/VERIFY.json new file mode 100644 index 0000000000..476e0e248c --- /dev/null +++ b/research/gaussian-ratio-budget/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "references/semantic-bulk/rad20/reports/review-phase-cell-inverse.md", + "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md", + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "4\u03b7 is below the weight floor and 16 p^2 \u03b4 < 1 for every integer p \u2265 2; \u03b5 = 1/2 is larger than 1/(16p^2) at p = 2." + } + ] +} diff --git a/research/gaussian-ratio-budget/verify.py b/research/gaussian-ratio-budget/verify.py new file mode 100644 index 0000000000..1f6b4edb7e --- /dev/null +++ b/research/gaussian-ratio-budget/verify.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Published 4η weight error against the 1/(16p^2) ratio budget. + +Every comparison is an integer identity. Across-cell entries are not bounded. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-ratio-budget" + + +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 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"] + downstream = ( + ROOT / "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md" + ).read_text(encoding="utf-8") + review = ( + ROOT / "references/semantic-bulk/rad20/reports/review-phase-cell-inverse.md" + ).read_text(encoding="utf-8") + gauge = ( + ROOT / "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md" + ).read_text(encoding="utf-8") + log_a = ( + ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ).read_text(encoding="utf-8") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "Set P=32768p and eta=2^(-P)." in downstream + assert "2^(-8p) None: + # 4η < 2^{-8p} iff 32760 p > 2. The gap grows with p. + assert 32768 - 8 == 32760 + assert 32760 * 2 > 2 + assert 32760 > 0 + + +def relative_budget() -> None: + # 4(p+1)^2 - 9p^2 = -5p^2 + 8p + 4 is 0 at p=2 and decreases by 10p+3. + assert -5 * 4 + 8 * 2 + 4 == 0 + assert -10 * 2 + 3 == -17 + assert -17 < 0 + # 9/4 < 4, so (p+1)^2 < 4 p^2 once 4(p+1)^2 <= 9 p^2. + assert 9 < 16 + # Base: 2^2 < 2^{4}. The step gives p^2 < 2^{2p} for every integer p>=2. + assert 4 < 16 + # 2p < 32760 p - 6, and the slack 32758 p - 6 increases by 32758. + assert 4 < 32760 * 2 - 6 + assert 32760 - 2 == 32758 + assert 32758 > 0 + # Therefore p^2 < 2^{32760 p - 6}. With δ = 2^{2-32760 p} and 16 = 2^4, + # 16 δ p^2 < 16 * 2^{2-6} = 1. + assert 2 ** 4 * 2 ** (2 - 6) == 1 + # At p=2 the exponent room is concrete. + assert 4 < 2 ** (32760 * 2 - 6) + # The gauge allowance 1/2 is larger than 1/(16p^2) at p=2: 1/2 > 1/64. + assert 2 * 64 == 128 + assert 128 > 2 + + +def main() -> None: + pins_and_phrases() + weight_room() + relative_budget() + print("PASS_GAUSSIAN_RATIO_BUDGET") + + +if __name__ == "__main__": + main()