Independently check #4449: across-cell downward rounding contract (exact exponent, repair lemma, sharpness; no new κ)

research/cross-rounding-check/README.md

@@ -0,0 +1,54 @@
+# Independent check of #4449: downward rounding of the across-cell Gaussian coefficient
+
+**Claim type:** an independent check by separate code, with exact rationals. **No new κ.** It covers
+mihir-s-05's [#4449](https://github.com/CrocSwap/integer-mult-bounds/pull/4449) (head `1fb77b37`). That PR
+supplies the across-cell contract `0 ≤ H ≤ n`, `n − H < 4·2^{−P}`, used by #4442 and by my #4462.
+
+## What is checked
+
+Setting: `s < t`, `u = α²`, `ρ = t/s`, `q_i = ⌊ti/s + 1/2⌋`, `b_i = ti − s·q_i`.
+
+1. **The exact exponent.** `u((ρh + β_i)² − β_{i+h}²) = j/k`, with `j = u((th + b_i)² − b_{i+h}²)`
+   and `k = s²`. So `n_{i,h} = exp(−πj/k)` exactly. Checked on 24,000 random cases with
+   `s ≤ 60`, `t ≤ 3s`, `u ≤ 50`, `|i| ≤ 500`, `|h| ≤ 40`, including both signs of `h`.
+2. **Ranges.** `−s/2 ≤ b_i < s/2`, with `j > 0` for every `h ≠ 0` and `j = 0` at `h = 0`.
+3. **The second form.** `j/k = u·d(d + 2b_{i+h}/s)`, with `d = q_{i+h} − q_i`.
+4. **The period cut.** `q_{i+s} = q_i + t` and `b_{i+s} = b_i`.
+5. **The repair `H = max(0, z − 2η)`.** Tested against every admissible P-grid oracle output `z`
+   (`|z − n| < 2η`) for 200 rational true values `n`: 794 cases, all giving `0 ≤ H ≤ n`,
+   `n − H < 4η`, and `H` on the grid.
+   - One ulp is not enough: `n = 3η/2` with `z = 3η` overshoots.
+   - The constant 4 is a sharp supremum: `z = 2η` with `n → 4η`.
+6. **The row bound.** At most `2W` entries give an across-cell rounding sum below `8Wη`.
+
+All statements check out.
+
+## Not covered
+
+- Whether an existing page generator uses this construction. #4449 states the same limit.
+- The fast exponential routine itself.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/cross-rounding-check --check-only
+python3.12 -B scripts/research_package.py --package research/cross-rounding-check
+```
+
+The verifier prints `PASS_CROSS_ROUNDING_CHECK` in about a second, using only the standard library.
+
+## Open next questions
+
+1. **Does the across-cell bound `8Wη` fit inside my #4462 robust budget `1/(32p³)`?**
+   - *First step:* with `W ≤ p − 1` and `η = 2^{−32768p}`, check `8(p−1)·2^{−32768p} ≤ 1/(32p³)`. It
+     holds easily, so FINE-PRIME-style rounding at this grid is covered.
+
+## Credit
+
+- The construction and the proof are mihir-s-05's (#4449). The repair method comes from the retained
+  phase-cell review.
+- The entry law is LOG-A's.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/cross-rounding-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/cross-rounding-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 #4449's across-cell downward rounding contract.",
+  "scope_change_reason": "Independent check of an open PR that #4442 and #4462 rely on.",
+  "bottleneck_link": "Supports the across-cell premise of the halo-exponent transfer.",
+  "budget_minutes": 25,
+  "stop_rule": "Stop at #4449's statements.",
+  "outcome": "completed",
+  "evidence": "All #4449 statements confirmed: exact exponent identity (24,000 cases), positivity, second form, period cut, repair lemma (794 adversarial cases), one-ulp counterexample, sharpness of 4.",
+  "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 8W eta fit #4462's robust budget 1/(32p^3)?",
+      "why_it_matters": "Covers FINE-PRIME-style rounding at this grid.",
+      "first_step": "Check 8(p-1) 2^(-32768p) <= 1/(32p^3).",
+      "blocked_by": "None."
+    }
+  ]
+}

research/cross-rounding-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": 60,
+      "checks": "#4449: exact exponent identity n=exp(-pi j/k) on 24,000 random cases, j>0 off-diagonal, second form, period cut, repair lemma against every admissible grid oracle output (794 cases), one-ulp counterexample, sharpness of 4, 8W eta row bound."
+    }
+  ]
+}

research/cross-rounding-check/verify.py

@@ -0,0 +1,89 @@
+#!/usr/bin/env python3
+"""Independent check of #4449: downward rounding of the across-cell Gaussian coefficient.
+
+With positive integers s < t, u (u = alpha^2), rho = t/s, q_i = floor(t i/s + 1/2), b_i = t i - s q_i, beta_i = b_i/s:
+  (1) exact rationals: (rho h + beta_i)^2 - beta_(i+h)^2 = j / (u k) with j = u((t h + b_i)^2 - b_(i+h)^2), k = s^2,
+      so n_(i,h) = exp(-pi u (...)) = exp(-pi j / k);
+  (2) -s/2 <= b_i < s/2 and j > 0 for every h != 0 (j = 0 at h = 0);
+  (3) the second form j/k = u d (d + 2 b_(i+h)/s), d = q_(i+h) - q_i;
+  (4) period cut: q_(i+s) = q_i + t and b_(i+s) = b_i;
+  (5) repair H = max(0, z - 2 eta) for any oracle |z - n| < 2 eta on the P-grid: 0 <= H <= n, n - H < 4 eta
+      (adversarial grid of n and admissible z, exact rationals); one ulp is not enough (n = 3eta/2, z = 3eta);
+      the constant 4 is a sharp supremum (z = 2 eta, n -> 4 eta);
+  (6) 2W entries give an absolute across-cell rounding sum below 8 W eta.
+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 and "`beta_i=rho*i-q_i`" in loga, "LOG-A entry law")
+    rng = random.Random(4449)
+    cases = 0
+    for _ in range(3000):
+        s = rng.randint(1, 60)
+        t = rng.randint(s + 1, 3 * s)  # any t > s, as in #4449 (rho up to 3)
+        u = rng.randint(1, 50)
+        rho = F(t, s)
+        q = lambda i: math.floor(F(t * i, s) + F(1, 2))
+        b = lambda i: t * i - s * q(i)
+        for _ in range(8):
+            i = rng.randint(-500, 500)
+            h = rng.randint(-40, 40)
+            bi, bh = b(i), b(i + h)
+            need(F(-s, 2) <= bi < F(s, 2), "(2) b range")
+            beta_i, beta_h = F(bi, s), F(bh, s)
+            need(beta_i == rho * i - q(i), "beta definition")
+            j = u * ((t * h + bi) ** 2 - bh ** 2)
+            k = s * s
+            need(u * ((rho * h + beta_i) ** 2 - beta_h ** 2) == F(j, k), "(1) exact exponent")
+            need((j > 0) if h else (j == 0), "(2) j > 0 off the diagonal")
+            d = q(i + h) - q(i)
+            need(F(j, k) == u * d * (d + F(2 * bh, s)), "(3) second form")
+            need(q(i + s) == q(i) + t and b(i + s) == b(i), "(4) period cut")
+            cases += 1
+    # (5) repair lemma on an adversarial exact grid
+    P = 12
+    eta = F(1, 2 ** P)
+    reps = 0
+    for num in range(0, 200):
+        n = F(num, 37) * eta  # true value, arbitrary rational
+        lo = math.floor((n - 2 * eta) / eta) + 1
+        hi = math.ceil((n + 2 * eta) / eta) - 1
+        for zz in range(lo, hi + 1):
+            z = zz * eta
+            if not abs(z - n) < 2 * eta:
+                continue
+            H = max(F(0), z - 2 * eta)
+            need(0 <= H <= n and n - H < 4 * eta and (H / eta).denominator == 1, "(5) repair")
+            reps += 1
+    n, z = F(3, 2) * eta, 3 * eta
+    need(abs(z - n) < 2 * eta and z - eta > n, "(5) one ulp is not enough")
+    for dl in (F(1, 2), F(1, 10), F(1, 1000)):
+        n, z = (4 - dl) * eta, 2 * eta
+        need(abs(z - n) < 2 * eta and max(F(0), z - 2 * eta) == 0 and n - 0 == (4 - dl) * eta, "(5) 4 is sharp")
+    for W in range(1, 50):
+        need(2 * W * 4 * eta == 8 * W * eta, "(6) 2W entries below 8 W eta")
+    print(json.dumps({"status": "PASS_CROSS_ROUNDING_CHECK", "exponent_cases": cases, "repair_cases": reps,
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())