Skip to content

v0.20.0 — stage F: H¹-object construction + certified γ₂ ≥ −0.02 bracket

Choose a tag to compare

View all tags
@afflom afflom released this 15 Jun 16:06
v0.20.0
bc191bf

v0.20.0 — stage F: the UOR construction of the crux (H¹-object + FORCED dictionary) and the certified γ₂ ≥ −0.02 bracket

Pure Lean 4 (no Mathlib, no sorry, no native_decide), choice-free {propext, Quot.sound}, warning-free; CI green; honesty audit passes (1940 non-private proof-layer theorems audited).

The H¹-object and the forced dictionary

The v0.18.0 bridge carried ⟨Cₙ,Cₙ⟩ = −2λₙ as interface data. Stage F derives it: a genuine rank-4 Néron–Severi-style lattice (Square/WeilLattice.lean) whose vanishing cycle Δ−Γ is proven primitive, the H¹ carrier named by its universal property (Square/Cohomology.lean), self-pairing computed from the Gram. The gate ran on the constructed object and located the frontier (Square/Forced.lean): the forced signature is exactly λₙ > 0 ∀n = RH — it did not come out positive, so hodgeIndexHolds/liPositivityHolds stay none.

The certified bracket γ₂ ≥ −0.02 (the v0.18.0 open computational frontier, now closed)

Rgamma2_ge_neg002 (Analysis/GammaTwoBracket.lean) proves γ₂ ≥ −1/50 constructively, via discrete Euler–Maclaurin (no constructive integration) on a new Real "ring engine" (RAddNF + RMulNF):

  • sStep_decomp — the trapezoidal residual s_p = b²·C2 + b·R1 + R0 as a free polynomial identity (both sides reduced to the same 7 canonical monomials, matched by an explicit choice-free permutation);
  • C2_nonneg (C2 ≥ 0, trapezoid ≥ integral) — dissolved by the coincidence dPlusQ(0,p) = ½(1/p+1/(p+1)) exactly;
  • sStep_lower_tele → hSeq_tele → Rgamma2_ge_hSeq — a single telescoping per-step bound, summed, lifted to the limit γ₂ = Rlim g2SeqDyadic (one-sided Archimedean);
  • gamma2_decide — one big-integer kernel decide (≈3 s, depth T=3, denominator D=10⁸).

Honest scope

This is a certified constant bound (evidence), not a positivity-of-all-λₙ (= RH) claim. Pos λ₃ remains open: λ₃ ≈ 0.0173 is a small difference of Θ(1) terms (λ₃^arith ≈ +1.22, λ₃^∞ ≈ −1.20), needing the full λ₃-formula numeric assembly. The crux fields stay none; RH stays OPEN.

See CHANGELOG.md for the full entry.

Assets 2
Loading