Encyclopedia Physics Physics Matter Wave From Rs

ARTICLE 2 claims 2 theorems

Physics Matter Wave From Rs

The de Broglie wavelength links a particle's momentum to a wave, and a machine-checked library shows how it fits a discrete ladder.

Matter waves

A matter wave is the wave associated with any moving particle. In 1924 Louis de Broglie proposed that a particle with momentum p has a wavelength λ = h/p, where h is Planck's constant. The relation is often written λ = ħ × 2π / p, with ħ (h-bar) the reduced Planck constant. The wavelength is tiny for everyday objects, but for electrons, neutrons, and atoms it is large enough to produce measurable interference patterns. Electron diffraction, neutron diffraction, atom interferometry, Bose-Einstein condensate (BEC) matter waves, and molecule diffraction are the five canonical demonstrations.

The classical account treats each phenomenon separately. A machine-checked library of formal theorems unifies them under a single framework. In Recognition Science, the framework models a discrete record of events, and the constant ħ is not a free parameter but a derived value: ħ = φ⁻⁵, where φ is the golden ratio. The de Broglie wavelength at a step k is defined as λk = (φk)⁻¹, and the framework proves that each step shrinks the wavelength by exactly the factor 1/φ: λk+1 / λk = φ⁻¹.

The framework's contribution is a certificate: a formal object that packages the count of five phenomena with the geometric decay law. The certificate is built from two proved theorems, with no unproved assumptions. The count of five is a definitional choice, not a derivation; the decay law is the proved content. The framework's library shows that the five phenomena share a common structural signature: each is an instance of a wavelength that decreases by the golden ratio at every step of a discrete ladder.

The consequence is a single lens for five experiments. Instead of five separate quantum effects, the framework presents one pattern: matter waves at successive rungs of a scale obey a fixed ratio. This does not replace the standard quantum mechanics, but it gives a compact, machine-checked account of why these five phenomena belong together. The practical lesson is portable: when a physical quantity is observed at discrete levels, a constant ratio between levels is a strong hint of an underlying scale, and here that scale is the golden ratio.

THEOREM deBroglieDecay · IndisputableMonolith/Physics/MatterWaveFromRS.lean
theorem deBroglieDecay (k : ℕ) :
    deBroglieWavelength (k + 1) / deBroglieWavelength k = phi⁻¹ := by
  unfold deBroglieWavelength
  have hk := (pow_pos phi_pos k).ne'
  rw [pow_succ, mul_inv]
  field_simp [hk, phi_ne_zero]
THEOREM matterWaveCert · IndisputableMonolith/Physics/MatterWaveFromRS.lean
noncomputable def matterWaveCert : MatterWaveCert where
  five_phenomena := matterWaveCount
  phi_decay := deBroglieDecay

What this page does not claim

The framework does not derive the existence of matter waves from first principles. The count of five phenomena is a definitional choice, not a theorem. No experimental measurement is cited in this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/MatterWaveFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND