toComplex_div
plain-language theorem explainer
The embedding of recovered complex numbers into Mathlib complexes preserves division. Researchers transporting algebraic identities from the logical carrier to standard analysis cite this when moving field operations across the equivalence. The proof is a one-line simplification that unfolds the division operator definitions on both sides.
Claim. Let $z, w$ be recovered complex numbers. The transport map satisfies $ι(z / w) = ι(z) / ι(w)$, where $ι$ sends a pair of recovered reals to the corresponding Mathlib complex number.
background
LogicComplex is the structure whose elements are pairs of recovered reals, serving as the carrier for complex numbers recovered from the logical foundation. The map toComplex extracts the real and imaginary parts via the real embedding toReal and packages them as a standard complex number. The module constructs this carrier and establishes its equivalence to Mathlib's ℂ without developing complex analysis inside the recovered setting. Upstream, the div lemma from RecogSpec.Core shows that division of PhiClosed elements remains PhiClosed, supplying the algebraic closure needed for the recovered division to be well-defined.
proof idea
The proof is a term-mode one-liner that invokes simp on the identifiers HDiv.hDiv and Div.div. This reduces both sides of the equality by expanding the division notation on the recovered carrier and on the target complex line, confirming that the embedding commutes with the operation.
why it matters
The lemma guarantees that the carrier embedding is a ring homomorphism at least for division, allowing algebraic identities to transfer without additional justification. It supports the equivalence construction later in the same module and fits the Recognition Science pattern of recovering arithmetic structures before analytic extensions. No downstream uses are recorded yet, leaving open whether it will be invoked in contour-integration or residue statements that rely on the complex equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.