Pith. sign in
module module high

IndisputableMonolith.Physics.Hadrons

show as:
view Lean formalization →

The module defines simple hadrons as quark-antiquark pairs using the Z-map and gap function. Particle physicists deriving masses in the Recognition Science framework cite it for meson and Regge relations. It supplies definitions for composite rungs, mass formulas, and linearity checks with no complex proofs.

claimHadrons are quark pairs with charge index $Z = \tilde{q}^2 + \tilde{q}^4$ (+4 for quarks) and mass $m = \mu_* \phi^{r-8 + F(Z)}$ where $F(Z) = \ln(1 + Z/\phi)/\ln(\phi)$. Regge trajectories satisfy $m^2$ linear in angular momentum with nonnegative slope.

background

The module sits in the RSBridge.Anchor setting that maps the 12 Standard Model fermions to an integer charge index ZOf and a gap function F. Constants supplies the base time quantum $\tau_0 = 1$ tick while Compat provides project shims. Hadrons are treated as the simplest composites (meson = quark-antiquark) on the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the hadronic sector that ParticleSummary imports to obtain Standard Model parameters from Recognition Science. It closes the bridge from the anchor definitions (Fermion, ZOf, gap, massAtAnchor) to observable meson masses and Regge slopes.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (10)