complex_exp_mul_rearrange
plain-language theorem explainer
The theorem encodes the multiplicative property of the complex exponential when its argument splits into a summed real damping term and a summed imaginary phase. Researchers manipulating wave-like cost functionals or phase factors in Recognition Science cost models would cite this identity to factor products of complex amplitudes. The proof is a one-line term wrapper that invokes the supporting private lemma exp_mul_rearrange.
Claim. For all real numbers $c_1,c_2,φ_1,φ_2$, the identity holds: Complex.exp$(-(c_1+c_2)/2)$ ⋅ Complex.exp$((φ_1+φ_2)⋅I)$ = [Complex.exp$(-c_1/2)$ ⋅ Complex.exp$(φ_1⋅I)$] ⋅ [Complex.exp$(-c_2/2)$ ⋅ Complex.exp$(φ_2⋅I)$].
background
The ClassicalResults module assembles textbook facts from real and complex analysis to support cost calculations in Recognition Science. These include the rearrangement of complex exponentials, norm identities for exp(r) and exp(iθ), and limits involving log sin. The local setting treats such results as standard (citing Rudin, Ahlfors, Conway) rather than new physical axioms, with most entries as axioms pending full Mathlib formalization.
proof idea
The proof is a one-line term wrapper that applies the private lemma exp_mul_rearrange. That lemma rewrites the left-hand side four times via Complex.exp_add, then uses congr 1 and push_cast to equate the summed arguments on each side.
why it matters
The identity supplies a basic algebraic tool inside the Cost domain for rearranging products of complex amplitudes that appear in phase and damping factors. It sits among other classical results (real_cosh_exponential_expansion, complex_norm_exp_I_mul) that enable later cost manipulations, though it has no recorded downstream uses. It aligns with the framework's reliance on standard analytic identities rather than new Recognition Science postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.