Independently check #4438: within-cell gauge column transfer (C = 3 least, equality at p = 2; no new κ)

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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())