piL
plain-language theorem explainer
piL recovers the constant π inside the LogicReal structure by transporting Mathlib's Real.pi through the fromReal embedding. Researchers building analytic identities over the recovered reals cite this definition to access standard properties of π while staying inside the LogicReal wrapper. The construction is a direct one-line application of the fromReal constructor to Real.pi.
Claim. Let $π_L ∈ LogicReal$ be the image of the standard real constant $π$ under the transport map fromReal : ℝ → LogicReal.
background
The module defines transported transcendental functions on LogicReal. LogicReal is the wrapper structure around the Bourbaki completion of the recovered rationals, with fromReal given explicitly as noncomputable def fromReal (x : ℝ) : LogicReal := ⟨CompareReals.compareEquiv.symm x⟩. The recovered real line is equivalent to Mathlib's ℝ by LogicReal.equivReal, so definitions in this module reuse established real analysis while remaining inside the logic-derived setting.
proof idea
one-line wrapper that applies fromReal to Real.pi
why it matters
piL supplies the constant π for the transport theorem toReal_piL, which states toReal piL = Real.pi. It completes the first layer of transcendental constants on LogicReal, allowing later modules to reduce analytic identities to Mathlib while working over the recovered reals. This step supports the foundation layer for real analysis in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.