E-035-zero-count-perimeter-derivations.py

{
  "experiment": "E-035",
  "title": "Grid check of Paper A Appendix C: the three zero-counting perimeter Props (ZeroCountGlobalProp / ZeroCountProp / ZeroCountProp2) derived from Rosser Thm 19 + Trudgian-II (1.2)/Cor.1/Thm 1",
  "session": "045",
  "thread": "paper-A-expert-review-revision",
  "design_doc": "paperA.tex Appendix C",
  "checks": {
    "A1_global_rosser": true,
    "A2_global_low": true,
    "A3_FAlt_positive_below_14": true,
    "A3_FAlt_increasing_below_14": true,
    "B0_C0hat_positive_below_14": true,
    "B1_unit_low": true,
    "B2_unit_rosser": true,
    "B2x_sign_change_beyond_1e8": true,
    "B3_unit_trudgian": true,
    "C1_two_unit_low": true,
    "C2_two_unit_rosser": true,
    "B1_reduced_at_u14_positive": true,
    "B2_reduced_at_u1e8_positive": true,
    "B3_reduced_at_u1e8_positive": true,
    "C1_reduced_at_t10_positive": true
  },
  "all_checks_pass": true,
  "dps": 60,
  "constants": {
    "1/(2pi)": "0.159154943092",
    "log(2pi)/(2pi)": "0.292507219914",
    "(1+log 2pi)/(2pi)": "0.451662163006",
    "R(14)": "2.3794477",
    "FAlt(2)": "2.6162315",
    "C0hat(3)": "4.0185207",
    "C0hat(14)": "5.0040573",
    "Z2hat(10)": "4.9974123",
    "unit_rosser_log_coeff": "0.4331549431",
    "unit_rosser_const": "2.883765445",
    "two_unit_rosser_const": "2.591258225"
  },
  "reduced_slacks": {
    "B1_reduced_at_u14": "0.743968",
    "B2_reduced_at_u1e8": "0.0133748",
    "B3_reduced_at_u1e8": "0.0521152",
    "C1_reduced_at_t10": "0.690851"
  },
  "notes": "ZeroCountProp (unit window) is Rosser-derivable only for u <= ~e^106.5 (log-coefficient 0.433155 > 0.433); Trudgian Thm 1 (published constants 0.112/0.278/2.510) covers u >= 1e8. The other two Props are Rosser-derivable for all heights in range. All counts with multiplicity."
}

#!/usr/bin/env python3
"""E-035 — grid check of Paper A Appendix C: the three zero-counting
perimeter hypotheses of the Lean development derived from published
explicit Riemann–von Mangoldt error bounds (session 045, expert-review
revision, reviewer suggestion 5).

The three declared Props (LiContour.lean; majorants in LiSkeleton.lean):
  (A) ZeroCountGlobalProp : N(T) <= FAlt(T)                         (T >= 2)
      FAlt(T) = T log T/(2 pi) + 0.137 log T + 0.443 log log T + 2.463
  (B) ZeroCountProp       : #{t <= gamma <= t+1} <= C0hat(t+1)      (t >= 2)
      C0hat(s) = 0.433 log(s+2) + 0.886 log log(s+2) + 2.9
  (C) ZeroCountProp2      : #{|gamma - t| <= 1} <= Z2hat(t)         (t >= 10)
      Z2hat(t) = 0.6 log(t+2) + 0.886 log log(t+2) + 2.7

Inputs (Appendix C (R1)-(R5)):
  (R1) Rosser Thm 19: |N(T) - P(T)| <= R(T) = 0.137 log T + 0.443 log log T
       + 1.588, T >= 1467, P(T) = T/(2pi) log(T/(2 pi e)) + 7/8; used in the
       reading-independent form |N - P| <= R + 0.2/T.
  (R2) Trudgian-II (1.2): |S(T)| <= 2 for T <= 6.8e6.
  (R3) Trudgian-II Cor. 1 remainder: |theta(T)/pi + 1 - P(T)| <= 0.2/T, T >= e.
  (R4) Trudgian-II Thm 1 (published constants; HSW 2022 Table 1):
       |S(T)| <= R_T(T) = 0.112 log T + 0.278 log log T + 2.510, T >= e.
  (R5) N(T) = 0 for T < 14.

The window bound (W): #{T1 <= gamma <= T2} <= (T2 - T1) P'(T2) + beta(T1)
+ beta(T2) + 0.2/T1 + 0.2/T2 with P'(T) = log(T/(2 pi))/(2 pi).

CHECKS (each = the appendix inequality evaluated on a grid; "slack" =
declared majorant minus the derived upper bound; PASS iff min slack > 0):
  A1: T in [1467, e^400]   via (R1)+(R3)        (log-grid)
  A2: T in [14, 1467]      via (R2)+(R3)        (step 0.05)
  A3: FAlt(T) > 0 and increasing on [2, 14)     (N = 0 by (R5))
  B1: u in [14, 1467]      via (W), beta = 2    (step 0.05)
  B2: u in [1468, 1e8]     via (W), beta = R    (log-grid)
  B2x: the Rosser-based bound fails for u > e^{106.5}: report the sign
       change (informational — explains the 1e8 split)
  B3: u in [1e8, e^400]    via (W), beta = R_T  (log-grid)
  B0: C0hat(u) > 0 for u in [3, 14)             (count 0 by (R5))
  C1: t in [10, 1467]      via (W), beta = 2    (step 0.05)
  C2: t in [1468, e^400]   via (W), beta = R    (log-grid)
Also prints the reduced-inequality slacks quoted in the appendix text
(0.74 at u = 14, 0.052 at u = 1e8, 0.69 at t = 10) for cross-reference.

Deterministic; dps 60 (widths passed exactly); no caching needed (runs in seconds).
"""
import json
import sys
from pathlib import Path

import mpmath as mp

mp.mp.dps = 60

DATA = Path(__file__).resolve().parent.parent / "data"
CSV = DATA / "E-035-zero-count-perimeter-derivations.csv"
JSON = DATA / "E-035-zero-count-perimeter-derivations.json"

pi, e = mp.pi, mp.e
mpf = mp.mpf
log = mp.log


def R(T):
    return mpf("0.137") * log(T) + mpf("0.443") * log(log(T)) + mpf("1.588")


def RT(T):
    return mpf("0.112") * log(T) + mpf("0.278") * log(log(T)) + mpf("2.510")


def P(T):
    return T / (2 * pi) * log(T / (2 * pi * e)) + mpf(7) / 8


def Pp(T):
    return log(T / (2 * pi)) / (2 * pi)


def FAlt(T):
    return (T * log(T) / (2 * pi) + mpf("0.137") * log(T)
            + mpf("0.443") * log(log(T)) + mpf(7) / 8 + mpf("1.588"))


def C0hat(s):
    return mpf("0.433") * log(s + 2) + mpf("0.886") * log(log(s + 2)) + mpf("2.9")


def Z2hat(t):
    return mpf("0.6") * log(t + 2) + mpf("0.886") * log(log(t + 2)) + mpf("2.7")


def window_bound(T1, T2, beta, width):
    """(W): upper bound for #{T1 <= gamma <= T2}, T2 - T1 = width (passed
    exactly: at T ~ 1e31 and beyond, T2 - T1 computed in floating point
    loses the unit width — the first run of this script tripped on that)."""
    return (width * Pp(T2) + beta(T1) + beta(T2)
            + mpf("0.2") / T1 + mpf("0.2") / T2)


def two(_T):
    return mpf(2)


def lin_grid(a, b, h):
    x = mpf(a)
    out = []
    while x <= mpf(b) + mpf("1e-12"):
        out.append(x)
        x += mpf(h)
    if out[-1] < mpf(b):
        out.append(mpf(b))
    return out


def log_grid(a, b, nsteps):
    la, lb = log(mpf(a)), log(mpf(b))
    return [mp.exp(la + (lb - la) * k / nsteps) for k in range(nsteps + 1)]


def min_slack(points, slack_fn):
    best = None
    for x in points:
        s = slack_fn(x)
        if best is None or s < best[0]:
            best = (s, x)
    return best


def main():
    rows = []
    checks = {}

    def record(name, best, extra=""):
        s, x = best
        ok = s > 0
        checks[name] = bool(ok)
        rows.append({"check": name, "min_slack": mp.nstr(s, 8),
                     "at": mp.nstr(x, 10), "pass": str(bool(ok)), "note": extra})
        print(f"{name}: min slack {mp.nstr(s, 8)} at {mp.nstr(x, 10)} -> {'PASS' if ok else 'FAIL'} {extra}")

    # ---- (A) global -------------------------------------------------------
    record("A1_global_rosser", min_slack(
        log_grid(1467, mp.exp(400), 4000),
        lambda T: FAlt(T) - (P(T) + R(T) + mpf("0.2") / T)),
        "T in [1467, e^400]; slack ~ 0.4517 T")
    record("A2_global_low", min_slack(
        lin_grid(14, 1467, "0.05"),
        lambda T: FAlt(T) - (P(T) + 2 + mpf("0.2") / T)),
        "T in [14, 1467], |S| <= 2")
    fa = lin_grid(2, 14, "0.01")
    fa_vals = [FAlt(T) for T in fa]
    incr = all(fa_vals[i + 1] >= fa_vals[i] for i in range(len(fa) - 1))
    record("A3_FAlt_positive_below_14", (min(fa_vals), fa[fa_vals.index(min(fa_vals))]),
           f"FAlt(2) = {mp.nstr(FAlt(2), 6)}; increasing on grid: {incr}")
    checks["A3_FAlt_increasing_below_14"] = bool(incr)

    # ---- (B) unit window [u-1, u], bound C0hat(u) ------------------------
    record("B0_C0hat_positive_below_14", min_slack(
        lin_grid(3, 14, "0.01"), lambda u: C0hat(u)),
        f"C0hat(3) = {mp.nstr(C0hat(3), 6)}")
    record("B1_unit_low", min_slack(
        lin_grid(14, 1467, "0.05"),
        lambda u: C0hat(u) - window_bound(u - 1, u, two, 1)),
        "u in [14, 1467], |S| <= 2")
    record("B2_unit_rosser", min_slack(
        log_grid(1468, mpf(10) ** 8, 4000),
        lambda u: C0hat(u) - window_bound(u - 1, u, R, 1)),
        "u in [1468, 1e8], Rosser")
    # informational: where does the Rosser-based bound stop working?
    cross = None
    for u in log_grid(mpf(10) ** 8, mp.exp(130), 2000):
        if C0hat(u) - window_bound(u - 1, u, R, 1) <= 0:
            cross = u
            break
    rows.append({"check": "B2x_rosser_bound_sign_change", "min_slack": "n/a",
                 "at": mp.nstr(cross, 8) if cross is not None else "none",
                 "pass": "info",
                 "note": f"log u at sign change = {mp.nstr(log(cross), 6) if cross is not None else 'none'} (expected ~106.5)"})
    print(f"B2x: Rosser-based unit bound first fails at u = {mp.nstr(cross, 6)} (log u = {mp.nstr(log(cross), 6)})")
    checks["B2x_sign_change_beyond_1e8"] = bool(cross is not None and cross > mpf(10) ** 8)
    record("B3_unit_trudgian", min_slack(
        log_grid(mpf(10) ** 8, mp.exp(400), 4000),
        lambda u: C0hat(u) - window_bound(u - 1, u, RT, 1)),
        "u in [1e8, e^400], Trudgian Thm 1")

    # ---- (C) two-unit window [t-1, t+1], bound Z2hat(t) -------------------
    record("C1_two_unit_low", min_slack(
        lin_grid(10, 1467, "0.05"),
        lambda t: Z2hat(t) - window_bound(t - 1, t + 1, two, 2)),
        "t in [10, 1467], |S| <= 2")
    record("C2_two_unit_rosser", min_slack(
        log_grid(1468, mp.exp(400), 4000),
        lambda t: Z2hat(t) - window_bound(t - 1, t + 1, R, 2)),
        "t in [1468, e^400], Rosser")

    # ---- reduced-inequality slacks quoted in the appendix text -------------
    u14 = mpf(14)
    red_B1 = (mpf("0.2738") * log(u14) + mpf("0.886") * log(log(u14)) - mpf("0.8384"))
    u8 = mpf(10) ** 8
    red_B3 = (mpf("0.049845") * log(u8) + mpf("0.33") * log(log(u8)) - mpf("1.82751"))
    t10 = mpf(10)
    red_C1 = (mpf("0.28169") * log(t10 + 1) + mpf("0.886") * log(log(t10 + 1)) - mpf("0.7595"))
    red_B2 = mpf("0.01623") - mpf("0.000155") * log(u8)
    reduced = {"B1_reduced_at_u14": mp.nstr(red_B1, 6),
               "B2_reduced_at_u1e8": mp.nstr(red_B2, 6),
               "B3_reduced_at_u1e8": mp.nstr(red_B3, 6),
               "C1_reduced_at_t10": mp.nstr(red_C1, 6)}
    print("reduced-inequality slacks (appendix text):", reduced)
    for k, v in reduced.items():
        checks[k + "_positive"] = bool(mpf(v) > 0)

    consts = {
        "1/(2pi)": mp.nstr(1 / (2 * pi), 12),
        "log(2pi)/(2pi)": mp.nstr(log(2 * pi) / (2 * pi), 12),
        "(1+log 2pi)/(2pi)": mp.nstr((1 + log(2 * pi)) / (2 * pi), 12),
        "R(14)": mp.nstr(R(14), 8),
        "FAlt(2)": mp.nstr(FAlt(2), 8),
        "C0hat(3)": mp.nstr(C0hat(3), 8),
        "C0hat(14)": mp.nstr(C0hat(14), 8),
        "Z2hat(10)": mp.nstr(Z2hat(10), 8),
        "unit_rosser_log_coeff": mp.nstr(1 / (2 * pi) + mpf("0.274"), 10),
        "unit_rosser_const": mp.nstr(mpf("3.176") - log(2 * pi) / (2 * pi) + mpf("0.4") / 1467, 10),
        "two_unit_rosser_const": mp.nstr(mpf("3.176") - log(2 * pi) / pi + mpf("0.4") / 1467, 10),
    }
    print("constants:", consts)

    allpass = all(checks.values())
    DATA.mkdir(parents=True, exist_ok=True)
    with CSV.open("w") as f:
        f.write(",".join(rows[0].keys()) + "\n")
        for r in rows:
            f.write(",".join(str(v).replace(",", ";") for v in r.values()) + "\n")
    sidecar = {
        "experiment": "E-035",
        "title": "Grid check of Paper A Appendix C: the three zero-counting perimeter "
                 "Props (ZeroCountGlobalProp / ZeroCountProp / ZeroCountProp2) derived "
                 "from Rosser Thm 19 + Trudgian-II (1.2)/Cor.1/Thm 1",
        "session": "045",
        "thread": "paper-A-expert-review-revision",
        "design_doc": "paperA.tex Appendix C",
        "checks": checks,
        "all_checks_pass": bool(allpass),
        "dps": 60,
        "constants": consts,
        "reduced_slacks": reduced,
        "notes": "ZeroCountProp (unit window) is Rosser-derivable only for u <= ~e^106.5 "
                 "(log-coefficient 0.433155 > 0.433); Trudgian Thm 1 (published constants "
                 "0.112/0.278/2.510) covers u >= 1e8. The other two Props are Rosser-derivable "
                 "for all heights in range. All counts with multiplicity.",
    }
    with JSON.open("w") as f:
        json.dump(sidecar, f, indent=2)
    print("ALL CHECKS PASS" if allpass else "SOME CHECKS FAIL")
    print(f"wrote {CSV} + {JSON}")
    return 0 if allpass else 1


if __name__ == "__main__":
    sys.exit(main())