Independently check #4439/#4442: halo exponents 12, 26, 28, 28, 6 under eps = 1/(16p^2) (no new κ)

research/eps-halo-exponent-check/README.md

@@ -0,0 +1,65 @@
+# Independent check of #4439 and #4442: halo exponents under ε = 1/(16p²)
+
+**Claim type:** an independent check of conditional exponent arithmetic, by separate code with exact
+rationals. **No new κ.** It covers jwr404's
+[#4439](https://github.com/CrocSwap/integer-mult-bounds/pull/4439) (within one cell, head `26af8afb`)
+and [#4442](https://github.com/CrocSwap/integer-mult-bounds/pull/4442) (across cells under the downward
+reading, head `d079c2b0`). It is the ε-route counterpart of my #4460, which covers the δ route.
+
+## What is checked
+
+- **The ceiling.** The split identity `(1−ε)[T_in/(1−ε) + T_out] − T = −ε·T_out` is proved as a
+  polynomial identity on a 3×3×3 grid. It gives `off ≤ (1−g)/(1−ε) = (16p²−2)/(16p²−1)`, so the gap is
+  exactly `1/(16p²−1)` and the absolute sums are below 2. Exact for `p` in 2..64.
+- **The exponents**, with `B = 16p²−1`. Exact for `p` in 2..64, plus all-`p` arguments.
+
+  | Role | Value | Reason |
+  | --- | --- | --- |
+  | spectral endpoint | 12 | `B² ≤ p^{12}`; for `p ≥ 3`, `(16p²)² < p^{12}` |
+  | series length | 26 | error `< B·e^{−p²} < p⁶e^{−p²}` |
+  | bandwidth and agreement distance | 28 | `(2p^{26} ± 1)(p−1) < p^{28}` |
+  | normalizer | 6 | `B < p⁶`; 7 also works |
+
+- **The "fails" entries.**
+
+  | Exponent | Where it fails | Reason |
+  | --- | --- | --- |
+  | endpoint 11 | `p = 2` | `63² > 2^{11}` |
+  | length 25 | `p = 2` | certified lower bound `(1−x)^L ≥ e^{−xL−x²L}` |
+  | 27 | `p = 2` (loose count) and `p ≥ 3` (sharp count) | |
+  | normalizer 5 | `p = 2` | `63 > 32` |
+
+- **#4442's tightness at `p = 2`.** An overshoot of 1/64 exceeds the ceiling, since
+  `63·63 = 3969 > 3968 = 62·64`.
+- **#4442's bare-kernel example.** With `θ = β = 1/4`, `h = 1`, `g = 2`, the next phase is `−1/2`.
+  The square gap is `2 = 32/16`, against `ρh² = 5/4 = 20/16`.
+
+All statements check out.
+
+## Not covered
+
+- The ideal gaps.
+- The rounding contract, which is #4449.
+- The δ route, which is my #4460 and #4462.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/eps-halo-exponent-check --check-only
+python3.12 -B scripts/research_package.py --package research/eps-halo-exponent-check
+```
+
+The verifier prints `PASS_EPS_HALO_EXPONENT_CHECK` in under a second, using only the standard library.
+
+## Open next questions
+
+1. **None specific to the ε route.** It is superseded by the δ route (#4452, #4460, #4462).
+
+## Credit
+
+- The lemmas and exponents are James Reed's (jwr404: #4439 and #4442).
+- The entry law is LOG-A's.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/eps-halo-exponent-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/eps-halo-exponent-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 #4439/#4442's epsilon-route halo exponents.",
+  "scope_change_reason": "Independent check of open author-checked lemmas.",
+  "bottleneck_link": "Side result on the #4100 precision/conditioning obligation.",
+  "budget_minutes": 25,
+  "stop_rule": "Stop at the stated arithmetic.",
+  "outcome": "completed",
+  "evidence": "All #4439/#4442 statements confirmed exactly for p=2..64 with all-p arguments; fails entries and p=2 tightness confirmed.",
+  "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": "None specific; superseded by the delta route.",
+      "why_it_matters": "n/a",
+      "first_step": "See #4460/#4462.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/eps-halo-exponent-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": "#4439/#4442 epsilon route: split identity (grid-proved), exact gap 1/(16p^2-1), exponents 12/26/28/28 and normalizer 6 for p=2..64 plus all-p arguments, every 'fails' entry, p=2 tightness 63*63>62*64, bare-kernel example."
+    }
+  ]
+}

research/eps-halo-exponent-check/verify.py

@@ -0,0 +1,81 @@
+#!/usr/bin/env python3
+"""Independent check of #4439 and #4442: halo exponents under the relative weight budget eps = 1/(16p^2).
+
+Ceiling. Ideal off-sums T <= 1 - g (g = 1/(8p^2)); within-cell entries <= ideal/(1-eps); across-cell entries in [0, n].
+Split T = T_in + T_out: off <= T_in/(1-eps) + T_out <= T/(1-eps) <= (16p^2-2)/(16p^2-1), so the gap is 1/(16p^2-1),
+||H^-1||_2 <= B = 16p^2 - 1 and ||H||_2 < 2. Exponents: endpoint 12 (B^2 <= p^12), length 26 (error < B e^-p^2 < p^6 e^-p^2),
+bandwidth/agreement 28, normalizer 6 (B < p^6; 7 also works). Fails: 11 (B^2 > p^11 at p = 2), 25 (length p^25 at
+p = 2), 27 (loose count at p = 2, sharp count p >= 3), normalizer 5 (63 > 32). Tightness at p = 2: an across-cell
+overshoot of 1/64 over the ideal off-sum (S-2)/S exceeds (S-2)/(S-1): 63*63 > 62*64. Bare-kernel example: theta = beta
+= 1/4, h = 1, g = 2 gives square gap 2 = 32/16 against rho h^2 = 5/4 = 20/16. Exact rationals p = 2..64, all-p
+arguments where stated. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as F
+import hashlib
+import itertools
+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 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")
+    # split identity: (1-e)[a/(1-e) + (t-a)] - t = -e (t-a), polynomial of degree <= 2 per variable, 3x3x3 grid
+    vals = [F(1, 7), F(2, 5), F(3, 4)]
+    for a, t, e in itertools.product(vals, repeat=3):
+        need((1 - e) * (a / (1 - e) + (t - a)) - t == -e * (t - a), "split identity")
+    for p in range(2, 65):
+        S = 16 * p * p
+        g, eps = F(1, 8 * p * p), F(1, S)
+        off = (1 - g) / (1 - eps)
+        need(off == F(S - 2, S - 1) and 1 - off == F(1, S - 1), "ceiling: gap 1/(16p^2-1)")
+        need(1 + off < 2, "absolute sums below 2")
+        B = S - 1
+        need(B * B <= p ** 12 and B < p ** 6, "endpoint 12, normalizer 6")
+        need(B < p ** 7, "normalizer 7 also works")
+        L = p ** 26
+        need((2 * L - 1) * (p - 1) < p ** 28 and (2 * L + 1) * (p - 1) < p ** 28, "bandwidth/agreement 28")
+        # error at length p^26: B (1 - p^-24)^(p^26) <= B e^-(p^2) < p^6 e^-(p^2)
+        need(B < p ** 6, "series error")
+        if p >= 3:
+            need((2 * p ** 26 - 1) * (p - 1) > p ** 27, "27 fails (sharp count, p >= 3)")
+    need(63 * 63 > 2 ** 11, "endpoint 11 fails at p = 2")
+    need(63 > 2 ** 5, "normalizer 5 fails at p = 2")
+    need((2 * 2 ** 26 + 1) > 2 ** 27, "27 fails (loose count, p = 2)")
+    # length p^25 fails at p = 2 on this route: B (1-x)^L >= B exp(-xL - x^2 L) with x = 2^-24, L = 2^25
+    x, L = F(1, 2 ** 24), 2 ** 25
+    need(math.log(63) - float(x * L + x * x * L) > math.log(64) - 4, "length 25 fails at p = 2")
+    # all p >= 2: (16p^2-1)^2 <= p^12 and 16p^2-1 < p^6 (p^4 >= 16, room 1 at p = 2)
+    need(all((16 * p * p - 1) ** 2 <= p ** 12 for p in range(2, 1000)), "endpoint 12 sample")
+    need(16 * 16 < 3 ** 8, "p >= 3: (16p^2)^2 < p^12 since p^8 >= 3^8 > 256")
+    # tightness at p = 2
+    Sx = 64
+    need(F(Sx - 2, Sx) + F(1, 64) > F(Sx - 2, Sx - 1) and 63 * 63 == 3969 and 62 * 64 == 3968, "p = 2 tightness")
+    # bare-kernel example
+    theta, beta, h, gstep = F(1, 4), F(1, 4), 1, 2
+    rho = 1 + theta
+    beta_next = beta + rho * h - gstep
+    gap = (rho * h + beta) ** 2 - beta_next ** 2
+    need(beta_next == F(-1, 2) and gap == 2 and rho * h * h == F(5, 4) and gap * 16 == 32 and rho * 16 == 20,
+         "bare-kernel example: square gap 32/16 against 20/16")
+    print(json.dumps({"status": "PASS_EPS_HALO_EXPONENT_CHECK", "exact_p_range": [2, 64],
+                      "exponents": {"spectral_endpoint": 12, "series_length": 26, "bandwidth": 28,
+                                    "agreement_distance": 28, "normalizer": 6},
+                      "fails_confirmed": ["11 at p=2", "25 at p=2", "27 (loose p=2, sharp p>=3)", "normalizer 5 at p=2"],
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())