toReal_mul
The theorem shows that the canonical transport from recovered reals to standard reals preserves multiplication. Researchers verifying the field structure on logic-derived reals would cite it when reducing algebraic identities back to classical analysis. The proof is a one-line wrapper that invokes the round-trip property of the transport.
claimLet $ϕ$ be the canonical equivalence from the Cauchy completion of the recovered rationals to the standard reals. Then $ϕ(x · y) = ϕ(x) · ϕ(y)$ for all recovered reals $x, y$.
background
The module recovers the reals from the Law-of-Logic rational layer by completing the recovered rationals LogicRat ≃ ℚ via Mathlib's Bourbaki construction. LogicReal is a thin wrapper around CompareReals.Bourbakiℝ that isolates instances while exposing the comparison equivalence to ℝ. Algebra on LogicReal is defined by pullback along this map, so every operation reduces to the corresponding operation on ℝ after transport. The key upstream result is the round-trip theorem stating that transport of the image of any standard real recovers the original real.
proof idea
This is a one-line wrapper that applies the round-trip theorem. Multiplication on LogicReal is defined by transporting the product from ℝ back through the inverse map, so the claimed equality is immediate from the fact that transport composed with its section is the identity.
why it matters in Recognition Science
The result confirms that the recovered reals carry a ring structure isomorphic to the standard reals, completing the transport for multiplication in the foundation layer. It directly supports the module's transport-first API, allowing any downstream algebraic identity on LogicReal to reduce to a Mathlib theorem on ℝ. No open questions are touched; the declaration simply closes one operation in the equivalence.
scope and limits
- Does not address addition or other ring operations.
- Does not prove existence or uniqueness of the completion.
- Applies only to the specific transport defined in this module.
- Does not treat topological or order properties.
formal statement (Lean)
144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
proof body
One-line wrapper that applies toReal_fromReal.
145 toReal_fromReal _