MatterWaveCert
plain-language theorem explainer
The MatterWaveCert structure bundles the assertion that exactly five matter-wave phenomena are recognized with the requirement that de Broglie wavelengths decrease geometrically by the factor phi inverse between successive rungs. Researchers deriving quantum mechanics inside Recognition Science cite this certificate when confirming the predicted scaling against the enumerated cases. The definition is assembled directly from the inductive enumeration of phenomena and the explicit wavelength function without invoking further lemmas.
Claim. A certificate structure whose fields require that the set of matter-wave phenomena has cardinality five and that the de Broglie wavelength satisfies $λ(k+1)/λ(k)=φ^{-1}$ for every natural number $k$, where $λ(k)=φ^{-k}$.
background
In the Recognition Science treatment of matter waves the de Broglie wavelength at rung k is defined by the upstream function deBroglieWavelength k := φ^{-k}. The inductive type MatterWavePhenomenon enumerates five concrete cases (electron diffraction, neutron diffraction, atom interferometry, BEC waves, molecule diffraction) whose Fintype cardinality is asserted in the certificate. The module places this construction in the setting where five phenomena correspond to configuration dimension 5 and the wavelength scales geometrically as φ^{-k}, consistent with ħ = φ^{-5}.
proof idea
The structure is introduced by declaring two fields: the cardinality equality Fintype.card MatterWavePhenomenon = 5 and the universal ratio property ∀ k, deBroglieWavelength (k+1) / deBroglieWavelength k = φ^{-1}. No tactics or lemmas are applied; the definition simply packages the two assertions.
why it matters
This certificate supplies the bundled properties consumed by the downstream matterWaveCert definition that constructs an explicit instance. It records the five-phenomena count and the phi-decay law predicted by the RS matter-wave module, supporting the geometric progression across the five canonical cases. Within the framework it aligns with the self-similar scaling enforced by the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.