Hadron
plain-language theorem explainer
The Hadron structure models mesons as pairs of RSBridge fermions with an integer binding offset defaulting to 1. Researchers deriving composite rung masses or Regge trajectories from the phi-ladder would cite this definition when building hadron mass formulas. It is introduced as a direct structure declaration with no proof obligations or additional constraints.
Claim. A hadron is a pair of fermions $q_1, q_2$ drawn from the RSBridge enumeration together with an integer binding offset $b$ (default value 1).
background
The Physics.Hadrons module derives hadron masses from composite rungs and Regge slopes using phi-tier spacing, with the eight-beat octave supplying the binding term. The Fermion type is an inductive enumeration of quarks (d, s, b, u, c, t) and leptons imported from RSBridge.Anchor and SMVerification modules, carrying decidable equality. RSBridge itself is a structure extending the minimal Bridge with geometric edge counts and fine-structure exponents for mixing angles.
proof idea
Direct structure definition declaring three fields: q1 and q2 of type RSBridge.Fermion and binding of type ℤ defaulting to 1. No lemmas or tactics are invoked; the declaration is a pure data structure with the default value supplied inline.
why it matters
This definition supplies the basic object for all downstream hadron mass relations in the Recognition framework. It is used by composite_rung to form the effective rung as RSBridge.rung q1 minus RSBridge.rung q2 plus binding, and by hadron_mass to scale E_coh by phi to that power. It fills the Phase 6 scaffolding for relating light-hadron masses to the phi-ladder and eight-tick octave, feeding into confinement results that attribute most proton mass to string energy rather than quark rest masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.