exp_mul_rearrange
plain-language theorem explainer
The lemma establishes the algebraic identity that the product of two complex exponentials with summed damping and phase parameters equals the product of the individual factors. Researchers formalizing path integrals or phase manipulations in physics would cite this rearrangement. The proof applies the exponential addition law four times, matches structures with congr, and reduces the expression via casting and the ring tactic.
Claim. $e^{-(c_1 + c_2)/2} e^{i (φ_1 + φ_2)} = [e^{-c_1/2} e^{i φ_1}] [e^{-c_2/2} e^{i φ_2}]$ for real $c_1, c_2, φ_1, φ_2$.
background
This identity sits in the ClassicalResults module, which assembles textbook facts from complex analysis for later use in cost and integral derivations. The complex exponential satisfies the addition formula exp(z + w) = exp(z) exp(w) for any complex z and w, a property drawn directly from Mathlib. The module context treats such results as standard, computationally verifiable facts justified by references including Ahlfors' Complex Analysis and Conway's Functions of One Complex Variable.
proof idea
The term-mode proof rewrites the left-hand side by applying Complex.exp_add four times to distribute the summed arguments, uses congr to align the resulting product structure, pushes the casts to reals, and finishes with the ring tactic to equate the exponents.
why it matters
The lemma supplies the body for the public theorem complex_exp_mul_rearrange, which in turn supports integral additivity statements such as piecewise_path_integral_additive_integrable. It supplies a standard complex-analysis step required for rearranging phase factors inside the Recognition Science cost framework. No open scaffolding remains attached to this fully proved identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.