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}.