toReal_rpowL
plain-language theorem explainer
The theorem shows that the power operation rpowL on the recovered real line commutes with the transport map to Mathlib reals. Researchers building analytic identities inside Recognition Science would cite it to reduce power expressions on LogicReal to standard real analysis. The proof is a one-line wrapper applying the general transport identity toReal_fromReal.
Claim. For all $x, y$ in the recovered real line, the transport of the transported power equals the standard real power: toReal(rpowL(x, y)) = Real.rpow(toReal(x), toReal(y)).
background
The module defines transcendental functions on LogicReal by transport through the equivalence to Mathlib's ℝ. LogicReal is realized as a wrapper around the Bourbaki completion of ℚ to prevent global instance pollution while reusing Mathlib's completed reals. The operation rpowL is defined by first transporting its arguments to ℝ, applying Real.rpow, and transporting the result back via fromReal. The key upstream identity is toReal_fromReal, which states that toReal(fromReal x) = x for any real x.
proof idea
The proof is a one-line wrapper that applies the general transport lemma toReal_fromReal directly to the definition of rpowL.
why it matters
This result guarantees that exponentiation on LogicReal reduces exactly to Mathlib's real power, preserving analytic identities under the equivalence LogicReal ≃ ℝ. It completes the transport layer for rpow in the same module that supplies the other transcendentals. No downstream uses appear yet, but the lemma supports later reduction of Recognition Science identities involving powers to established real analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.