Treffer: Face north Observatory Riemann

We present a formally grounded and computationally auditable result of uniform lower rigidity on logarithmic grids for windowed potentials with bounded variation. The core theorem (S13b) shows that for aligned grid blocks the potential satisfiesE(LN)−E(Lk1)≥−(K+2A)\displaystyle E(L_N)-E(L_{k_1}) \ge -\big(K+2A\big)E(LN)−E(Lk1)≥−(K+2A),and that the same bound persists under off-grid endpoints via explicit prefix/suffix absorption (each ≤A\le A≤A). The result is delivered with (i) Lean 4/mathlib formal statements and proofs for the telescoping identity and structural lemmas; (ii) headless Python (stdlib-only) checks that emit CI-parsable PASS/FAIL artifacts (CSV/MD/txt) and optional SHA256/HMAC sealing; and (iii) a CI gating setup (exact-set, repro-latch, deny/allow-list) to guarantee reproducibility and auditability. This paper consolidates the L3→L12f lemma chain (integrability, BV windows, integral split, aligned interior lower bound) and provides a robust bridge from density to counting (S14) through log-adapted kernels (Fejér/Abel). While we do not claim a proof of the Riemann Hypothesis, the S13b module stabilizes the analytic pipeline required for density→counting transfers, and serves as a reusable template for open, auditable mathematics: formal layer + internal attacks + computational artifacts, all reproducible under CI. Keywords: Riemann hypothesis; analytic number theory; bounded variation; log-grid telescoping; formal verification; Lean; mathlib; reproducibility; continuous integration; auditable research. Suggested upload set: PDF of the paper; appendix figures (PNG or northface_annex_figs.zip); Lean source files (e.g., src/lean/L13b.lean); headless scripts (S13/S13b/S14 checks); CI workflow YAML; LICENSE; CITATION.cff; README.md. Related identifiers (recommended): “isSupplementTo” → GitHub release/tag; “isCompiledBy” → Overleaf project (if public); DOI of previous “Face North” papers (as “isPartOf” or “isPreviousVersionOf”).