toReal_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that LogicReal coincides with ℝ beyond the transport map.
- Does not derive the unit element from the Law of Logic axioms without the completion step.
- Does not address ordering, field operations, or completeness properties of LogicReal.
formal statement (Lean)
137@[simp] theorem toReal_one : toReal (1 : LogicReal) = 1 := toReal_fromReal 1