v0.1.0 — genuine Lean proof layer

The genuine-proof layer: real Lean 4 theorems (no Mathlib, zero sorry), built from first principles on the UOR-Foundation substrate.

46 theorems across 6 modules, every one audited axiom-clean (#print axioms ⊆ {propext, Classical.choice, Quot.sound}; no sorry, no native_decide, no stray axioms — enforced in CI):

• Mechanism / Template — the function-field Hodge mechanism: the Hasse flip as the integer condition a² ≤ 4q, and the product-of-curves template with ample H²=2>0 and negative-definiteness on the primitive complement H⊥.
• CharOne — the characteristic-1 (max-plus) base: idempotency (R1), semiring laws, the reversal theorem (R12).
• CycleCounts — the Bowen–Lanford trace identity (R6) N₁…N₈ = tr(Bᵐ) = 0,2,6,2,10,14,14,34, kernel-checked on exact integer matrix powers.
• Bridge — the mechanism bridge (Hodge type ⟹ spectral bound) and the §2.3 control (a rank-1 Gram is PSD for any spectrum, so that positivity is vacuous w.r.t. RH).
• Crux — the Hodge-index property proved on the template; the crux CruxFor 𝕊 left open on the unconstructed square.

Mechanized-honesty gate (scripts/honesty_audit.sh, run in CI): a verifier, not a prohibition — it forbids sorry/native_decide/stray axioms, never a genuine proof.

Literature (§2): citation corrections from an independent full-text verification; the Feb-2026 Jacobian of Spec ℤ̄ proves moduli, not positivity; the deferred Hermitian-Jacobi computation on T5's critical path is still outstanding.

The Riemann Hypothesis remains open. The crux is proved nowhere. Honestly scoped (not done): the full κ⊥spectrum decidable counterexample (needs a tropical closure module) and exact λₙ bounds (RH-equivalent / needs transcendentals).

See the CHANGELOG.