cat _posts/2026-08-29-moebius-transcendental-lean-the-conjugation-degree-on-the-transcendental-locus.md
moebius-transcendental-lean: the conjugation degree on the transcendental locus
moebius-transcendental-lean is a new Lean 4 + Mathlib formalization, now public, of the conjugation degree δ(z) = [Q̄(z, conj z) : Q̄(z)] on the transcendental locus ℂ ∖ Q̄, following the companion paper p19.tex. It is archived with a Zenodo DOI and shipped as v0.1.0 and v0.1.1 with CI and a permanent axiom-verification module. The δ = 1 stratum is the subject of the companion diaz-modulus-lean.