Independently check #4437: the ideal column majorant holds (and is attained) across g = 2 steps (no new κ)

research/column-cut-check/README.md

@@ -0,0 +1,57 @@
+# Independent check of #4437: the ideal column majorant survives g = 2 steps
+
+**Claim type:** an independent numerical check with explicit tolerances. **No new κ.** It covers jwr404's
+[#4437](https://github.com/CrocSwap/integer-mult-bounds/pull/4437) (head `7ca94e97`). That PR extends
+#4402's column majorant from one constant-phase run to every column of the ideal narrow matrix,
+including steps `g = 2`.
+
+## What is checked
+
+The ideal matrix `N` is built directly from LOG-A's entry law, without #4437's code:
+
+- `n_{i,h} = exp(−a[(ρh + β_i)² − β_{i+h}²])`, with `ρ = 1 + θ`;
+- `β_i = ρi − q_i ∈ [−1/2, 1/2)`, so `q_i = ⌊ρi + β_0 + 1/2⌋` and every step is 1 or 2.
+
+1. **The majorant.** Every interior column off-sum is at most
+   `M = e^{−2aθ} + e^{−2a(1−θ)} + 2e^{−2a}/(1−e^{−4a})`. The grid is
+   `p ∈ {2,3,5,10}`, with `a` at both GAUSSIAN ends (`4 log 16p`, `5 log 16p`) and at 1, 1/2 and 1/4,
+   with `θ ∈ {1/(4p²), 1/p², 0.2, 0.25}`, and 20 phases `β_0`. That is **192,000 columns**, of which
+   **55,515 meet a `g = 2` step**. A local run of 704,000 columns (203,625 with `g = 2`) agrees.
+2. **Sharpness.** The maximum of off-sum/`M` is **1.0** to floating precision, so the majorant is
+   attained and cannot be improved uniformly.
+3. **The landing intervals.** At every column, #4437's table holds: incoming `g = 2` gives
+   `β ∈ [−1/2, −1/2+θ)`; both steps 1 give `β ∈ [−1/2+θ, 1/2−θ)`; outgoing `g = 2` gives
+   `β ∈ [1/2−θ, 1/2)`.
+4. **The gap.** `1 − M > 1/(8p²)` at both `θ` ends with `a = 4 log 16p`, the worst case since `M`
+   decreases in `a`, for every `p` from 2 to 10⁴. The minimum of `8p²·gap` is 26.3. The perturbed gap
+   stays above `1/(16p²)` once `2pε ≤ 1/(16p²)`.
+
+## Not covered
+
+- An all-`p` proof of item 4. #4437 gives the written argument, and this check only samples `p`
+  up to 10⁴.
+- The rounded reference `H`, `‖N^{−1}‖₁`, and any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/column-cut-check --check-only
+python3.12 -B scripts/research_package.py --package research/column-cut-check
+```
+
+The verifier prints `PASS_COLUMN_CUT_CHECK` in about 5 seconds, using only the standard library.
+
+## Open next questions
+
+1. **Does the attained majorant leave room for the δ-route ceiling?**
+   - *Why it matters:* my #4462 uses an ideal gap of `1/(8p²)`, while the true gap here is at least
+     `26/(8p²)`.
+   - *First step:* redo #4462's Lemma B with the measured gap `3.3/p²`.
+
+## Credit
+
+- The lemma and the proof are James Reed's (jwr404, #4437, building on #4402).
+- The entry law is LOG-A's.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/column-cut-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/column-cut-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 numerical check of #4437's ideal column majorant across g=2 steps.",
+  "scope_change_reason": "Independent check of an open author-checked lemma.",
+  "bottleneck_link": "Side result: supports the ideal-gap hypothesis used by the halo-exponent chain.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at numerical checks.",
+  "outcome": "completed",
+  "evidence": "192,000 columns (55,515 with g=2) within the majorant, which is attained; landing intervals hold; gap*8p^2 >= 26.3 for p<=1e4.",
+  "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": "Can #4462's Lemma B use the true gap (>= 26/(8p^2) for p<=1e4)?",
+      "why_it_matters": "Larger rounding tolerance and smaller constants.",
+      "first_step": "Redo Lemma B with gap 3.3/p^2.",
+      "blocked_by": "An all-p proof of the larger gap."
+    }
+  ]
+}

research/column-cut-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": "Ideal narrow matrix from LOG-A's entry law: 192,000 interior columns (55,515 meeting g=2) within #4437's majorant (attained), landing-interval table at every column, gap > 1/(8p^2) for p=2..1e4 at worst corners, perturbation step."
+    }
+  ]
+}

research/column-cut-check/verify.py

@@ -0,0 +1,87 @@
+#!/usr/bin/env python3
+"""Independent numerical check of #4437: the ideal column majorant survives g = 2 steps.
+
+Builds the ideal narrow matrix directly from LOG-A's entry law n_(i,h) = exp(-a[(rho h + beta_i)^2 - beta_(i+h)^2]),
+rho = 1 + theta, beta_i = rho i - q_i in [-1/2, 1/2) (so q_i = floor(rho i + beta_0 + 1/2) and every step is 1 or 2),
+and checks every interior column off-sum against
+    M(a, theta) = exp(-2 a theta) + exp(-2 a (1-theta)) + 2 exp(-2a) / (1 - exp(-4a))
+over 4 primes-sized p, 5 values of a (both GAUSSIAN ends and three outside), 4 values of theta and 20 phases beta_0.
+It also checks #4437's landing-interval table (incoming/outgoing g against beta_j), that the majorant is attained
+(sharp), and the gap 1 - M > 1/(8p^2) at the corners of a in [4 log 16p, 5 log 16p], theta in [1/(4p^2), 1/p^2] for
+p = 2..10^4 (M is monotone in a; both theta ends are checked), plus the 2p eps <= 1/(16p^2) perturbation step.
+Floating point with explicit tolerances. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import hashlib
+import json
+import math
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def majorant(a, th):
+    return math.exp(-2 * a * th) + math.exp(-2 * a * (1 - th)) + 2 * math.exp(-2 * a) / (1 - math.exp(-4 * a))
+
+
+def columns(a, th, b0, n=200, H=40):
+    rho = 1 + th
+    q = [math.floor(rho * i + b0 + 0.5) for i in range(n)]
+    beta = [rho * i + b0 - q[i] for i in range(n)]
+    need(all(-0.5 <= b < 0.5 for b in beta) and all(q[i] - q[i - 1] in (1, 2) for i in range(1, n)), "entry law")
+    out = []
+    for j in range(H, n - H):
+        s = sum(math.exp(-a * ((rho * (j - i) + beta[i]) ** 2 - beta[j] ** 2)) for i in range(j - H, j + H + 1) if i != j)
+        gin, gout = q[j] - q[j - 1], q[j + 1] - q[j]
+        b = beta[j]
+        if gin == 2:
+            need(gout == 1 and -0.5 <= b < -0.5 + th + 1e-12, "landing: incoming g = 2")
+        elif gout == 2:
+            need(0.5 - th - 1e-12 <= b < 0.5, "landing: outgoing g = 2")
+        else:
+            need(-0.5 + th - 1e-12 <= b < 0.5 - th + 1e-12, "landing: both steps 1")
+        out.append((s, gin == 2 or gout == 2))
+    return out
+
+
+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")
+    total = with_g2 = 0
+    worst = 0.0
+    for p in (2, 3, 5, 10):
+        L = math.log(16 * p)
+        for a in (4 * L, 5 * L, 1.0, 0.5, 0.25):
+            for th in (1 / (4 * p * p), 1 / (p * p), 0.2, 0.25):
+                M = majorant(a, th)
+                for k in range(20):
+                    for s, g2 in columns(a, th, -0.5 + k / 20):
+                        need(s <= M * (1 + 1e-11), f"column majorant p={p} a={a} theta={th}")
+                        worst = max(worst, s / M)
+                        total += 1
+                        with_g2 += g2
+    need(worst > 1 - 1e-9, "the majorant is attained (sharp)")
+    need(with_g2 > 0.2 * total, "a substantial share of columns meet a g = 2 step")
+    min_ratio = math.inf
+    for p in range(2, 10001):
+        L = math.log(16 * p)
+        for th in (1 / (4 * p * p), 1 / (p * p)):
+            gap = 1 - majorant(4 * L, th)
+            min_ratio = min(min_ratio, gap * 8 * p * p)
+            need(gap > 1 / (8 * p * p), f"gap > 1/(8p^2) at p={p}")
+            need(gap - (2 * p - 1) / (2 * p) / (16 * p * p) > 1 / (16 * p * p), "perturbed gap > 1/(16p^2)")
+    print(json.dumps({"status": "PASS_COLUMN_CUT_CHECK", "columns": total, "columns_meeting_g2": with_g2,
+                      "max_offsum_over_majorant": round(worst, 12), "min_gap_times_8p2_p_to_1e4": round(min_ratio, 4),
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())