toComplex_re
The theorem records that the real part of an embedded LogicComplex equals the direct transport of its real component. Analysts verifying component-wise fidelity in the recovered-to-standard embedding cite it when checking consistency of the complex carrier. The proof is immediate reflexivity from the definition of the embedding map.
claimLet $z$ be a pair of recovered reals. The real part of the image of $z$ under the embedding into standard complex numbers equals the image of the real component of $z$ under the real transport map: $ (embedding(z)).re = transport(z.re) $.
background
LogicComplex is the structure whose fields are two recovered reals (re and im). The embedding toComplex sends such a pair to a standard complex number by applying the real transport separately to each field. The real transport converts a recovered real into a Mathlib real via an equivalence comparison on its underlying value. This module builds the carrier for complex numbers over the recovered reals and proves basic equivalence with Mathlib's complex line, deferring analytic development to later modules.
proof idea
The proof is a one-line reflexivity step. By the definition of the embedding, which constructs a standard complex number from the pair of transported components, the real-part projection matches the transport of the real component exactly.
why it matters in Recognition Science
The result closes the basic transport lemmas for the complex carrier, guaranteeing that component extraction commutes with the embedding. It supports the module's goal of recovering standard complex numbers from the logical foundation without redeveloping analysis. No downstream theorems are recorded yet, but the declaration underpins any future analytic work that invokes the equivalence.
scope and limits
- Does not establish holomorphy or any analytic continuation properties.
- Does not treat contour integration or residue calculus.
- Does not prove uniqueness of the embedding or other structural properties.
- Does not address arithmetic identities beyond the real-part projection.
formal statement (Lean)
42@[simp] theorem toComplex_re (z : LogicComplex) :
43 (toComplex z).re = toReal z.re := rfl
proof body
44