diff --git a/research/gauge-column-check/README.md b/research/gauge-column-check/README.md new file mode 100644 index 0000000000..0e7da7af63 --- /dev/null +++ b/research/gauge-column-check/README.md @@ -0,0 +1,57 @@ +# Independent check of #4438: the within-cell gauge column transfer + +**Claim type:** an independent check by separate code, with exact rationals where possible. **No new κ.** +It covers jwr404's [#4438](https://github.com/CrocSwap/integer-mult-bounds/pull/4438) (head `6157a47b`). + +## What is checked + +1. **The factorization.** On a constant-phase run (`β_{i+h} = β_i + θh`), LOG-A's entry factors as + + n_{i,h} = (a_i / a_{i+h})·exp(−aρh²), with a_i = exp(aβ_i²/θ), + + because the exponent is `h²(1+2θ) + 2hβ_i`. This is checked in log form on 2,000 random runs + (`p ∈ {2,3,5,10}`, `a` up to `5 log 16p`, `θ ∈ [1/(4p²), 1/p²]`). The maximum log error is + `6·10⁻¹³`. +2. **The column bound.** For a downward kernel (`Ĝ/G ∈ [0.9, 1]` at random) and + `(1−ε)a ≤ â ≤ a` at random with `ε = 1/(16p²)`, every column off-sum of `diag(â)Ĝdiag(â)^{−1}` is + at most the ideal one divided by `1−ε`. The maximum observed ratio to the bound is 0.99977, so + the bound is nearly tight. +3. **The ceiling, in exact rationals.** An ideal off-sum `1 − 1/(8p²)` with `ε = 1/(16p²)` leaves + gap exactly `1/(16p² − 1)`. The gauge audit's `ε = 1/2` leaves no gap. +4. **The setup constant.** `C = 3` is the least integer with `2^{−Cp} ≤ 1/(16p²)` for every `p ≥ 2`. + There is equality at `p = 2` (`64 = 64`), and `C = 2` fails there. This is checked to `p = 10⁴`, + plus the induction ratio `(4/3)² < 8`. +5. **The downstream comparison.** `(2p−1)/(16p) > 1/(8p²)`, i.e. `p(2p−1) > 2`, for every `p`. + +All statements of #4438 check out. + +**Note.** `C = 3` meets the budget with *equality* at `p = 2`. That is fine for #4438's `ε ≤ 1/(16p²)`, +but there is no slack at `p = 2`. + +## Not covered + +- Across-cell entries (see #4442, #4449 and my #4462). +- The exponents of #4406. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gauge-column-check --check-only +python3.12 -B scripts/research_package.py --package research/gauge-column-check +``` + +The verifier prints `PASS_GAUGE_COLUMN_CHECK` in about a second, using only the standard library. + +## Open next questions + +1. **Does the δ-repaired weight (#4451) make `C` irrelevant here?** + - *First step:* replace `2^{−Cp}` by `δ = 2^{2−32760p}`. Every comparison then holds with slack. + +## Credit + +- The lemma is James Reed's (jwr404, #4438). +- The entry law is LOG-A's. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/gauge-column-check/SOURCES.json b/research/gauge-column-check/SOURCES.json new file mode 100644 index 0000000000..6a28c347a0 --- /dev/null +++ b/research/gauge-column-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + } + ] +} diff --git a/research/gauge-column-check/TASK.json b/research/gauge-column-check/TASK.json new file mode 100644 index 0000000000..1d2850fcc6 --- /dev/null +++ b/research/gauge-column-check/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": "Independent check of #4438's within-cell gauge column transfer.", + "scope_change_reason": "Independent check of an open author-checked lemma.", + "bottleneck_link": "Side result supporting the halo-exponent chain.", + "budget_minutes": 25, + "stop_rule": "Stop at #4438's statements.", + "outcome": "completed", + "evidence": "All #4438 statements confirmed: factorization (log error 6e-13), 1/(1-eps) bound (max ratio 0.99977), gap 1/(16p^2-1), C=3 least with equality at p=2, p(2p-1)>2.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Does the delta-repaired weight make C irrelevant?", + "why_it_matters": "Removes the zero-slack p=2 equality.", + "first_step": "Replace 2^(-Cp) by delta.", + "blocked_by": "None." + } + ] +} diff --git a/research/gauge-column-check/VERIFY.json b/research/gauge-column-check/VERIFY.json new file mode 100644 index 0000000000..12ed85caef --- /dev/null +++ b/research/gauge-column-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "#4438: factorization on 2,000 random constant-phase runs, the 1/(1-eps) column bound on random rounded blocks, exact gap 1/(16p^2-1) and eps=1/2 failure, least setup constant C=3 (equality at p=2), downstream comparison p(2p-1)>2." + } + ] +} diff --git a/research/gauge-column-check/verify.py b/research/gauge-column-check/verify.py new file mode 100644 index 0000000000..6034c12576 --- /dev/null +++ b/research/gauge-column-check/verify.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Independent check of #4438: the within-cell gauge column transfer. + +On a constant-phase run (beta_(i+h) = beta_i + theta h) LOG-A's entry n_(i,h) = exp(-a[(rho h + beta_i)^2 - beta_(i+h)^2]) +factors as (a_i / a_(i+h)) exp(-a rho h^2) with a_i = exp(a beta_i^2 / theta), since the exponent is +h^2 (1 + 2 theta) + 2 h beta_i. For a downward kernel 0 <= Ghat <= G and (1-eps) a <= ahat <= a, each within-cell +column off-sum of diag(ahat) Ghat diag(ahat)^-1 is at most the ideal one divided by 1-eps. Checks: + * the factorization on random runs (relative error < 1e-12); + * the 1/(1-eps) bound on 2,000 random rounded blocks, eps = 1/(16p^2), p in {2,3,5,10} (and its tightness); + * exact rationals: ideal off-sum 1-1/(8p^2) with eps = 1/(16p^2) leaves gap 1/(16p^2-1); eps = 1/2 leaves none; + * C = 3 is the least integer with 2^(-Cp) <= 1/(16p^2) for all p >= 2 (equality at p = 2; C = 2 fails at p = 2), + checked exactly to p = 10^4 plus 16 p^2 <= 8^p by induction (8 (p+1)^2 <= 8 * 2.25 p^2 < 8 * 8 p^2... ratio); + * the downstream comparison (2p-1)/(16p) > 1/(8p^2), i.e. p(2p-1) > 2. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as F +import hashlib +import json +import math +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + loga = (ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md").read_text(encoding="utf-8") + need("`n_i,h=exp(-a[(rho*h+beta_i)^2-beta_(i+h)^2])`" in loga, "LOG-A entry law") + rng = random.Random(4438) + worst_fact = 0.0 + tight = 0.0 + blocks = 0 + for p in (2, 3, 5, 10): + eps = 1 / (16 * p * p) + for _ in range(500): + a = rng.uniform(0.5, 5 * math.log(16 * p)) + theta = rng.uniform(1 / (4 * p * p), 1 / (p * p)) + n = p * 6 + b0 = rng.uniform(-0.5, 0.5 - theta * n) # a run of n indices stays inside [-1/2, 1/2) + beta = [b0 + theta * i for i in range(n)] + rho = 1 + theta + lw = [a * b * b / theta for b in beta] # log a_i (kept in log form to avoid overflow) + W = p - 1 + ideal = [[0.0] * n for _ in range(n)] + for i in range(n): + for j in range(max(0, i - W), min(n, i + W + 1)): + if i == j: + continue + h = j - i + le = -a * ((rho * h + beta[i]) ** 2 - beta[j] ** 2) + lf = lw[i] - lw[j] - a * rho * h * h + worst_fact = max(worst_fact, abs(le - lf) / max(1.0, abs(le))) + ideal[i][j] = math.exp(le) + u = [1 - eps * rng.random() for _ in range(n)] # ahat_i = a_i u_i with (1-eps) a <= ahat <= a + for j in range(n): + col_ideal = sum(ideal[i][j] for i in range(n)) + # entry ahat_i Ghat_h / ahat_j = ideal * (u_i / u_j) * (Ghat / G), with Ghat / G in [0.9, 1] + col_hat = sum(ideal[i][j] * u[i] / u[j] * rng.uniform(0.9, 1.0) for i in range(n) if ideal[i][j]) + need(col_hat <= col_ideal / (1 - eps) * (1 + 1e-12), "column bound 1/(1-eps)") + if col_ideal: + tight = max(tight, col_hat / col_ideal * (1 - eps)) + blocks += 1 + need(worst_fact < 1e-12, "factorization") + for p in range(2, 200): + g, eps = F(1, 8 * p * p), F(1, 16 * p * p) + need(1 - (1 - g) / (1 - eps) == F(1, 16 * p * p - 1), "gap 1/(16p^2-1)") + need((1 - g) / F(1, 2) > 1, "eps = 1/2 leaves no gap") + need(p * (2 * p - 1) > 2 and F(2 * p - 1, 16 * p) > F(1, 8 * p * p), "downstream comparison") + need(all(16 * p * p <= 8 ** p for p in range(2, 10001)) and 16 * 4 == 8 ** 2, "C = 3 works, equality at p = 2") + need(16 * 4 > 4 ** 2, "C = 2 fails at p = 2") + # induction for p >= 3: 16(p+1)^2 <= 16 * (16/9) p^2 < 8 * 16 p^2 <= 8 * 8^p + need(F(4, 3) ** 2 < 8, "induction ratio ((p+1)/p)^2 <= 16/9 < 8 for p >= 3") + print(json.dumps({"status": "PASS_GAUGE_COLUMN_CHECK", "random_blocks": blocks, + "factorization_max_log_error": f"{worst_fact:.1e}", "max_column_ratio_over_bound": round(tight, 6), + "least_setup_constant": 3, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())