Connection Coefficient Composition

Abstract

Connection coefficients compose multiplicatively along a two-step path.

Theorem 1.1 (Connection coefficients multiply along composition).

$$\begin{gathered} (\forall R,M:Type,(\mathrm{CommSemiring}(R)\wedge \mathrm{AddCommMonoid}(M)\wedge \mathrm{Module}(R,M))\Rightarrow \forall a,b:R,X,Y,Z:M,(Y=a\cdot X\wedge Z=b\cdot Y)\Rightarrow Z=a\times b\cdot X)\wedge \\ (\forall x\in \mathbb{R},0<x\Rightarrow \sqrt{\frac{\pi \times \exp (x)}{2\times x}}=\sqrt{\frac{\pi }{2}}\times \exp (\frac{x}{2})\times x^{-\frac{1}{2}}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Constants/Characterizations/ConnectionCoefficientComposition.connection_coefficient_composition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first clause quantifies the scalar and module carriers and states both successive path equations before deriving the product coefficient. Commutativity presents the coefficient in source order.

The second clause exposes the displayed positive-real certificate. The strictly positive x premise is the domain on which the reciprocal square-root scale is defined and the three factors multiply exactly.

References

• Truth anchor: D5/S3/Constants/Characterizations/ConnectionCoefficientComposition.connection_coefficient_composition