piL
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.
claimLet $π_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 in Recognition Science
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.
scope and limits
- Does not prove any arithmetic or geometric properties of π inside LogicReal.
- Does not construct π from series or limits native to the recovered rationals.
- Does not connect to the phi-ladder, J-cost, or other Recognition Science constants.
Lean usage
theorem toReal_piL : toReal piL = Real.pi := toReal_fromReal _formal statement (Lean)
38def piL : LogicReal := fromReal Real.pi
proof body
Definition body.
39
40/-- Sine on recovered reals. -/