deBroglieDecay
plain-language theorem explainer
The theorem establishes that the de Broglie wavelength on the phi-ladder decreases by the exact factor phi inverse between consecutive rungs. A physicist deriving matter-wave scaling from the Recognition Science forcing chain would cite this result to confirm the geometric progression. The proof is a term-mode reduction that unfolds the wavelength definition, records the nonzero power of phi, and simplifies the ratio by field operations.
Claim. For each natural number $k$, the ratio of the de Broglie wavelength at rung $k+1$ to the wavelength at rung $k$ equals $phi^{-1}$, where the wavelength at rung $k$ is defined as $phi^{-k}$.
background
The module derives the de Broglie wavelength from Recognition Science constants with hbar equal to phi to the minus five. The wavelength at rung k is defined as the inverse of phi to the power k, which encodes the geometric progression for matter waves after absorbing the constant prefactors from lambda equals hbar times 2 pi over p. The module states that five canonical phenomena correspond to configDim D equals 5, with the RS prediction that wavelength at rung k equals lambda zero times phi to the minus k.
proof idea
The proof unfolds the wavelength definition to obtain the ratio of phi to the minus k plus one over phi to the minus k. It records that phi to the k is nonzero via the positive power lemma, rewrites the successor exponent and the multiplicative inverse, then applies field simplification using the nonzero hypothesis together with the phi nonzero lemma to reduce the expression directly to phi inverse.
why it matters
This theorem supplies the phi decay field inside the matterWaveCert definition that certifies the five matter wave phenomena. It implements the RS prediction of geometric decay on the phi ladder, consistent with the self similar fixed point phi arising from T5 J uniqueness and T6 in the forcing chain. The result is fully proved and closes the scaling step required for the A1 QM foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.