v0.2.0 — finite tropical stack + exact-ℚ analysis brick

Resolves the finite/decidable open questions as kernel-checked Lean theorems and lays the first analysis brick — exact ℚ, built the UOR way. Pure Lean 4, no Mathlib, no sorry; +26 theorems (72 total), all axiom-clean (#print axioms ⊆ {propext, Classical.choice, Quot.sound}; no sorry/native_decide/stray axioms — enforced in CI).

Tropical κ / spectrum stack (F1Square/Tropical/)

• Closure — R2 Kleene-star idempotence W* ⊗ W* = W*; the canonical W* matches the companion.
• Spectrum — R3 κ permutation-invariance, R4 the cycle-mean spectrum, and the headline R9/R10 κ⊥spectrum counterexample (same content-address, different dynamics) + R11 the κ-fiber.
• Siblings — R14 boolean κ permutation-invariance, R15 the faceted (κ_trop, κ_bool) address, R16 boolean-facet degeneracy on a strongly-connected graph.

Tropical Hodge-index signatures (F1Square/Tropical/Signature.lean)

• The §2.3 parallel pencil Δ·Γ_n = 0 (det((1,1),(1,1)) = 0); the fan-vs-fiber correction (the fan recession form is degenerate, so the (1,ρ−1) shape belongs to the fiber form); and a Babaee–Huh counterexample — the Hodge signature is NOT automatic.

First analysis brick — exact ℚ (F1Square/Analysis/Rat.lean)

• Exact rationals from ℤ the UOR way: the canonical reduced form is the content-address; decidable exact equality/order; idempotent reduce. The analysis-substrate roadmap is documented: ℚ → constructive ℝ → ℂ + transcendentals → ζ / λₙ, one brick per release.

Honest demarcation

RH remains open. v0.2.0 resolves the finite questions and starts the analysis substrate; it does not resolve λₙ / Weil-positivity / the crux — those are RH. Building the substrate makes them statable and finitely checkable, never proven. R7/R8 (limit/asymptotic) await the constructive-ℝ brick (v0.3.0).

See the CHANGELOG.