toReal_one
plain-language theorem explainer
The declaration shows that the transport map from logic-derived reals sends the multiplicative unit to the standard real 1. Foundation-layer developers in Recognition Science cite it when confirming that arithmetic constants survive the recovery from the Law of Logic via rational completion. The proof is a direct one-line application of the general transport identity toReal_fromReal at the argument 1.
Claim. Let $L$ denote the Cauchy completion of the logic rationals and let $t : L → ℝ$ be the canonical transport. Then $t(1_L) = 1$.
background
LogicReal wraps Mathlib's Bourbaki completion of ℚ, built on the equivalence LogicRat ≃ ℚ recovered from the Law of Logic. The map toReal extracts the underlying real via CompareReals.compareEquiv, while fromReal embeds standard reals back into the wrapper. This yields a transport-first API: algebra and order on LogicReal are defined by pullback along toReal so every statement reduces to a standard real theorem and returns.
proof idea
The proof is a one-line wrapper that applies the upstream theorem toReal_fromReal at the concrete argument 1.
why it matters
It supplies the base case for the constant 1 under transport, enabling simp reduction in any arithmetic expression involving the unit in LogicReal. The result sits inside the reals-from-logic recovery that supplies the real line for the phi-ladder and mass formulas downstream in the Recognition framework. No direct parent theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.