matterWaveCount
plain-language theorem explainer
The declaration fixes the number of canonical de Broglie matter wave phenomena at exactly five by computing the cardinality of the enumerated type. Modelers of quantum interference in Recognition Science cite the result to set the configuration dimension for observable wave effects. The proof is a direct decision procedure that evaluates the finite type cardinality from its five-constructor inductive definition.
Claim. The set of canonical matter wave phenomena has cardinality $5$.
background
The module derives de Broglie matter waves from Recognition Science, expressing the wavelength as $λ = φ^{-5} × 2π / p$ with the RS-native ħ = φ^{-5}. The inductive type enumerates five phenomena: electron diffraction, neutron diffraction, atom interferometry, Bose-Einstein condensate waves, and molecule diffraction. This enumeration is identified with configuration dimension D = 5, and the wavelength is predicted to scale as λ₀ × φ^{-k} on the phi-ladder.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the finite type whose inductive definition contains exactly five constructors.
why it matters
The result supplies the five_phenomena component of the MatterWaveCert definition, anchoring the quantum foundation for matter waves. It confirms the five enumerated phenomena as the complete set matching configDim D = 5 and supports the RS de Broglie scaling prediction across phi-ladder rungs. The supplied documentation flags no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.