Irrationality Exponents of Real CM Elliptic Periods and Powers of the Lemniscate Period
We give a determinant proof that every nonzero real period of a nonsingular elliptic curve over $\mathbb Q$ with complex multiplication, measured with a specified nonzero rational invariant differential, has irrationality exponent two. The proof uses an integral origin chart, matched local lengths, an actual compactification and weighted packet map, and arithmetic and analytic estimates for the same selected minor on a rectangular sublattice of the full CM period lattice. For the integral-defined lemniscate period $Ω=2\int_0^1(1-t^4)^{-1/2}\,dt$, we also give the uniform bound $μ(Ω^n)=O(n\log(2n))$ for integers $n\geq1$. Its new arithmetic ingredient clears integration denominators prime by prime while retaining the coefficient order; a one-root norm argument and an analytic estimate at algebraic centers complete the power proof. The two arguments are presented with their different charts and exact dependencies. Lean verifies the new CM determinant argument and rational normalization relative to explicit classical uniformization, CM-lifting and theta inputs; the lemniscate-power endpoint is also verified. The formalization record states the exact classical boundary and theorem references.