pith. sign in
module module moderate

IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder

show as:
view Lean formalization →

The MesonSpectrumFromPhiLadder module supplies the type and functions that place observed mesons onto the Recognition Science phi-ladder. It defines MesonFamily together with mesonMass, mass_ratio and the certification predicate MesonSpectrumCert. Particle physicists seeking parameter-free hadron masses would cite these objects. The module is purely definitional and contains no theorems.

claimLet $M$ be the type of meson families. Define $m : M → ℝ$ by $m(f) = τ_0^{-1} φ^{r(f)-8+g(f)}$ where $r(f)$ is the rung index of family $f$, $g(f)$ its gap, $τ_0$ the base time quantum and $φ$ the golden ratio. The predicate MesonSpectrumCert asserts that the resulting masses reproduce the observed meson spectrum in RS-native units.

background

Recognition Science obtains all masses from the phi-ladder whose base scale is the fundamental time quantum $τ_0 = 1$ tick imported from Constants. The general mass formula assigns a particle to rung $r$ with correction $g(Z)$ so that $m = τ_0^{-1} φ^{r-8+g(Z)}$. This module specializes the ladder to the meson sector by introducing the inductive type MesonFamily that enumerates allowed combinations of quantum numbers together with the auxiliary functions mesonMass, mass_ratio and mass_pos.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module realizes the concrete mass formula for mesons and packages the certification object MesonSpectrumCert that later physics modules invoke to assert numerical agreement with experiment. It therefore supplies the missing link between the abstract phi-ladder (T6) and observable hadron masses inside the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)