carlok — zsh — 88×30

cat _posts/2026-09-02-moebius-transcendental-lean-v0-2-0-the-conjugation-degree-spectrum-is-classified.md

moebius-transcendental-lean v0.2.0: the conjugation-degree spectrum is classified

moebius-transcendental-lean tagged v0.2.0, which classifies the conjugation-degree spectrum on the transcendental locus: conjDegree attains every value in ℕ∞ except 0, which it never attains. Every finite degree gets the same explicit witness, zₙ = sⁿ + i·s with s = liouvilleNumber 2, while the ⊤ stratum comes from an algebraically independent real pair. It compiles against Mathlib v4.32.0 with no sorry, and the permanent axiom-verification module confirms the ten new declarations close over exactly {propext, Classical.choice, Quot.sound}.