v0.17.0 — the canonical arithmetic square 𝕊 with its derived intersection lattice

Stage C — the canonical arithmetic square. Pure Lean 4, no Mathlib, choice-free (#print axioms = {propext, Quot.sound}); all 1683 non-private proof-layer theorems audited; build green and the mechanized-honesty gate passes. RH stays OPEN — the crux hodgeIndexHolds/liPositivityHolds remain none.

Canonical 𝕊 = Spec ℤ ×_𝔽₁ Spec ℤ, with its universal property proved

Deitmar 𝔽₁-algebras are commutative monoids and 𝔽₁ (the trivial monoid) is proved initial, so the tensor F ⊗_𝔽₁ F is the plain coproduct — realized as ℕ₊ × ℕ₊.

• copair_inl/copair_inr/copair_unique, sq_factor — the universal property; the 𝔽₁-cocone condition is automatic (coproduct = pushout over 𝔽₁).
• IsCoproduct, sq_isCoproduct, coproduct_unique_upto_iso — canonicality as a theorem: "the" tensor is well-defined, unique up to canonical isomorphism, not a candidate model.
• Strict 2-dimensionality (gen2_injective — the monomial family 2^a ⊗ 2^b is free of rank 2); the §3.1 ℤ-collapse avoided by theorems (inl_ne_inr, non-injective codiagonal); both projections recover the curve. T1 for all points.
• Level precision: the canonical object is the monoid-level ⊗_𝔽₁; the semiring-level ⊗_𝔹 concrete description (Sagnier, arXiv 1703.10521) remains open and is not claimed.

The intersection lattice — derived, never entered by hand

Every primitive number is a point count on the constructed square, with classes moved along their translation pencils: V·H = 1, V² = H² = 0, Δ·V = Δ·H = 1, Δ² = 0 from the parallel-pencil disjointness itself (Δ ∩ Γ_n = ∅), Γ·V = Γ·H = 1, Γ·Γ = Δ·Γ = 0. Bilinearity then forces E₃² = −2 (e3_sq_forced), and the sourced product-of-curves template emerges (sqPair_eq_template) — T3's intrinsic realization, closed by derivation. The five §2.2 gate self-checks are theorems; the class lattice is finitely generated (T2 on 𝕊); the graph class is forced (graph_class_unique), so [Γ_n] = [Δ] — the pencil is numerically trivial.

The parallel pencil carries the arithmetic as shift lengths

logN_mul_general (log(ab) = log a + log b, all positive naturals, by exp injectivity) and logN_pow_general; pencil_shift (the affine shift log y = log x + log n on Γ_n, exact), pencil_parallel (slope 1 ⇒ direction (1,1)), pencil_det_zero (stable Δ·Γ_n = 0), pencil_separation (constant log n) — and the Λ-tie on the full prime-power support: pencil_separation_vonMangoldt (= Λ(p) = log p at primes) and pencil_separation_pow_vonMangoldt (= k·Λ(pᵏ)), the latter via Euclid's lemma built from scratch (prime_dvd_mul, Bézout-free — core Lean has no Nat.Coprime) giving Λ(pᵏ) = log p in general (vonMangoldt_prime_pow).

Polarized 𝕊, its Hodge index — and the boundary that keeps RH open

squarePolarized — the Crux.Polarized instance is now 𝕊's own derived lattice; ample H = [V]+[H], H² = 2 > 0 (verified — not automatic tropically); H^⊥ negative-definite; square_hodgeIndex holds. And square_hodge_pencil_blind: the lattice is pencil-blind ([Γ_n] = [Δ], Δ·Γ_n = 0 for all n) — the function-field trace input (Δ·Γ_q = q+1−a) is provably absent, the positivity carries no spectral content (the §2.3-control discipline, geometric face), so it is not the crux. The crux is the Hodge index / Weil positivity of the H¹-bearing pairing (⟺ λₙ ≥ 0 ∀n), faithfully stated in stage D.

De-hedges

surfaceConstructed and parallelPencilFinding flip none → some true (honest scope: the T1–T3 monoid-scheme level; the H¹-bearing spectral enrichment is NOT constructed); classGroupFinitelyGen / intersectionTemplateValid / ampleClassExists are now carried by canonical 𝕊.

Full details in CHANGELOG.md.