v0.18.0 — the bridge: the two faces of the crux are equivalent; the attempt under the gate

Stage D — the bridge and the crux attempt. Pure Lean 4, no Mathlib, choice-free (#print axioms = {propext, Quot.sound}); every non-private proof-layer theorem audited; build green and the mechanized-honesty gate passes. RH stays OPEN — the crux hodgeIndexHolds/liPositivityHolds remain none, exactly per the bright line.

The Castelnuovo–Severi anchor (BridgeFF.lean)

The function-field model of "Hodge index ⟹ RH" as a genuine lattice derivation, no governor shortcut: the E × E lattice {F_h, F_v, Δ, Γ} with the trace datum Δ·Γ = q+1−a (Lefschetz) inside it; the primitive projection of xΔ + yΓ has D°² = −2(x² + a·xy + q·y²); and ff_hodge_iff_hasse: negativity for all x, y ⟺ a² ≤ 4q — the Hasse/Weil bound (forward: instantiate (a, −2); backward: 4(x²+axy+qy²) = (2x+ay)² + (4q−a²)y²). The v0.1.0 governor is now derived (ff_hodge_iff_hodgeType): "the mechanism is not the gap" (§0.3) is a theorem — and re-deriving the proven Hasse bound from the lattice is a built-in consistency check of the implementation against established mathematics.

The λ₂ Bombieri–Lagarias decomposition (Analysis/LiTwo.lean)

λ₂ = [2γ − (γ² + 2γ₁)] + [(1−γ) − log 4π + ¾ζ(2)] as a constructive-real identity (Rlambda2_decomposition; standard Stieltjes convention pinned — η₀ = −γ, η₁ = γ² + 2γ₁). Li.LiDecomposition realized with two genuine slices (li_decomposition_two_realized), both certified positive (certified λ₁ ≥ 0.0231, λ₂ ≥ 0.0043; true values ≈ 0.0230957, ≈ 0.0923457 — the pinned λ₂ closed form matches the literature value, independently re-verified to 30 digits).

THE BRIDGE (Square/Spectral.lean) — the release goal

SpectralSquare: the H¹-bearing enrichment of 𝕊 as an interface — Li/trace data lam, primitive self-intersections cSq, and the dictionary ⟨Cₙ,Cₙ⟩ = −2λₙ (the Deninger-type Hodge-index reading, conjectural at number fields and hence interface DATA, sourced through the verified Connes–Consani account, Selecta Math. 27 (2021); normalization derived by BridgeFF.primDG_sq). The equivalence is a constructive theorem: spectral_bridge_nonneg, spectral_bridge_pos, and crux_faces_equivalent : SpectralCrux S ⟺ Li.LiCrux S.lam — the geometric and analytic faces of the crux are the same proposition. The classical chain is cited with its verified statements (Weil 1952 on C_c^∞(0,∞), proven directly for the restricted class by Burnol; Bombieri 2000; Li 1997; Bombieri–Lagarias 1999). Inhabited with the genuine certified λ₁, λ₂ (spectral_evidence_two: ⟨C₁,C₁⟩ < 0, ⟨C₂,C₂⟩ < 0). Honesty guards as theorems, in both directions: spectralTwoSlice_not_crux (no finite assembly of certified slices can be passed off as RH) and spectral_template_crux (the property is satisfiable — the encoding hides no impossibility; the attempt is not biased toward failure), plus the finite-check guard spectral_iff_all_upTo.

The crux attempt, under the gate (Square/Attempt.lean)

Run, recorded, honestly concluded. Certified: strict Hodge negativity through n = 2 (spectral_strict_upTo_two). The frontier, exact: crux_attempt_frontier — given the certified slices, the crux ⟺ ∀ n ≥ 3, λₙ > 0 (the next slice needs the second Stieltjes constant γ₂). The post-mortem records why the general routes are blocked, with the program's own controls as evidence (the §2.3 vacuity control; pencil-blindness; the BL cancellation; the Conrey–Li precedent), the literature's own open question on finite truncations (Bombieri 2000 covers only the finitely-many-off-line-zeros case), and what would close it (the genuine H¹ instance — Connes–Consani's unconditional archimedean positivity, support [2^{−1/2}, 2^{1/2}], being the strongest partial result). Conclusion: the universal did not close; the fields stay none.

Fidelity

All attributions, sign conventions, and constants reconciled against an adversarially-verified literature report (103 research agents; 21 confirmed, 4 refuted paraphrases excluded): the Stieltjes-convention trap pinned, the certified-bound-vs-true-value phrasing corrected repo-wide, the dictionary sourced to its verified status.

Full details in CHANGELOG.md.