v0.19.0 — stage E + the genuine pairing: four equivalent faces of the crux

v0.19.0 — Stage E + the genuine pairing

The completion arc of the F1-square program, in pure Lean 4 (Lean core + UOR-Foundation, no Mathlib, no sorry/native_decide, choice-free {propext, Quot.sound}), every commit green and #print axioms-audited. RH remains OPEN — hodgeIndexHolds/liPositivityHolds stay none, exactly as the bright line requires.

The crux now has FOUR provably equivalent faces

• geometric ⟨Cₙ,Cₙ⟩ < 0 ∀n, analytic λₙ > 0 ∀n (Li), dominance (one uniform bound under which the arithmetic oscillation never overwhelms the archimedean trend), and pairing (positivity of the assembled Weil functional). All equivalences are genuine constructive theorems; the shared proposition is RH and is never asserted.

Stage E (the explicit formula, the roll-up)

• The explicit-formula trace completed at the built Bombieri–Lagarias slices; the Li.LiAgreesWith/ExplicitFormulaTrace interfaces retired there.
• The dominance face (Square/Dominance.lean): Dominated ⟺ SpectralCrux ⟺ LiCrux, with the closure route's head discharged as a theorem.
• The genuine archimedean trend, all n (ArchTrend.lean) and the genuine Li sequence in closed form modulo the Stieltjes tail (GenuineLi.lean).

The genuine pairing (formerly planned v0.20/v0.21, folded in)

• The Weil functional assembled (Analysis/Weil.lean, Square/Pairing.lean): W = poles − primes − archimedean, the zero side as the defect of the built sides — no zeros as inputs. The finite-place side and archimedean constant are constructed; the integral terms stay honest interfaces (their piecewise-linear closed forms are unverified in print).
• The first computed pairing value (weilPrime_demo): the finite-place side at the tent peaked at 2 is exactly log 2.
• The window theorem on the built object: inside the prime-free window the finite-place side vanishes identically, so W = poles − archimedean.
• ψ(1/4) — the first exact non-trivial digamma value, a genuine constructive real with ψ(1/4) ≥ −4.32; α(0) > 0 — Burnol's window multiplier at the center, an axiom-clean theorem (≈ 5.94).
• The honest finding (DigammaWindow.lean): the bare multiplier α(τ) is indefinite (dips to ≈ −1.0 near τ ≈ 2.27) — α(τ) ≥ 0 ∀τ is NOT a theorem; windowed positivity is the restricted-class/Sonine statement. The τ-parameterized kernel Re ψ(1/4+iτ/2) is built with its monotonicity (the correct object for v0.20.0).

Verified against the literature

Two deep-research sweeps (101 + 99 agents, primary PDFs): Voros's dichotomy, Lagarias's unconditional archimedean asymptotics, Burnol's direct equivalence and window multiplier, the Connes–Consani unconditional window, Bombieri's truncations — conventions pinned, traps flagged.

Honest scope

Every surrounding construction ships; the crux stays one open proposition. The roadmap plans all remaining work as v0.20.0 — the UOR-based construction of the canonical H¹-object whose intrinsic self-pairing's signature is derived (not assumed), mirroring the proven function-field bridge column-for-column.

🤖 Generated with Claude Code