rpowL
plain-language theorem explainer
rpowL equips the recovered real line LogicReal with real exponentiation by transporting Mathlib's Real.rpow through the toReal and fromReal maps. Analysts working in the Recognition Science foundation layer cite this when manipulating powers while remaining inside the logic-derived reals. The definition is a direct one-line wrapper that applies the Mathlib operation after mapping the arguments.
Claim. Let $x, y$ be elements of the recovered real line $L$. The real power is defined by $x^y := f(R(x), R(y))$, where $R$ denotes the transport map from $L$ to the standard reals and $f$ denotes the standard real power function, with the result transported back into $L$.
background
LogicReal is the structure wrapping the Bourbaki real obtained as the Cauchy completion of the recovered rationals via the equivalence LogicRat ≃ ℚ. The wrapper prevents global instance pollution on Completion ℚ while still permitting reuse of Mathlib's completed real line. The maps fromReal and toReal realize the equivalence between this recovered line and Mathlib's ℝ.
proof idea
This is a one-line wrapper that applies toReal to the inputs, invokes Mathlib's Real.rpow, and embeds the result via fromReal.
why it matters
rpowL supplies the exponentiation operation required for analytic work on the recovered reals. It is used by the transport theorem toReal_rpowL, which establishes that toReal commutes with rpowL. The module positions this as the first layer so that later modules can reason over LogicReal while reducing identities to Mathlib's real-analysis library.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.