pith. sign in
module module high

IndisputableMonolith.Physics.Hadrons

show as:
view Lean formalization →

This module defines simple hadrons as quark-antiquark pairs in the Recognition Science framework, with meson examples such as up-bar down. It supplies composite rung assignment, hadron mass formulas on the phi-ladder, and Regge slope certificates. Particle physicists deriving meson spectra or Regge trajectories from the recognition mass formula would cite these definitions. The module contains only definitions and supporting lemmas with no complex proof structure.

claimHadrons are modeled as quark pairs with mass $m = y_0 φ^{r-8 + F(Z)}$ where $F(Z) = ln(1 + Z/φ)/ln φ$ is the gap function, $r$ is the composite rung, and $Z$ is the charge-indexed index from the Z-map.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and the core bridge from RSBridge.Anchor. Anchor defines the 12 Standard Model fermions, the Z-map Z_i = q̃² + q̃⁴ (+4 for quarks), the gap function F(Z) = ln(1 + Z/φ)/ln φ, and the anchor-scale mass μ⋆. Hadrons are treated as composite objects whose rung on the phi-ladder is set by the recognition composition law and whose masses follow the yardstick formula yardstick · φ^(rung - 8 + gap(Z)).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the hadron mass and Regge trajectory definitions that feed directly into the ParticleSummary module for deriving Standard Model parameters from Recognition Science. It implements the phi-ladder mass formula using the gap function and Z-map from RSBridge.Anchor, closing the bridge from the T5 J-uniqueness and T6 phi fixed-point steps to observable meson spectra.

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)