composite_rung
plain-language theorem explainer
The composite_rung definition computes an integer tier for any hadron by subtracting the rung of its second quark from the rung of the first and adding the binding offset. Modelers of hadron spectra on the phi-ladder cite this when building mass formulas or proving degeneracy for equal-Z states. The definition is a direct one-line arithmetic combination of the rung function on the two fermion fields plus the binding integer.
Claim. For a hadron $h$ formed by fermions $q_1$, $q_2$ and binding integer $b$, the composite rung equals $r(q_1) - r(q_2) + b$, where $r$ denotes the integer rung assignment on fermions.
background
The Physics.Hadrons module treats hadrons as quark pairs via the Hadron structure, which packages two RSBridge.Fermion values and a default binding integer of 1. The rung function, drawn from upstream RSBridge and Anchor modules, supplies the integer tier for each fermion species (for example, 4 for both up and down quarks). Composite rung then assembles these tiers to feed the phi-ladder mass scaling used throughout the module.
proof idea
One-line definition that applies the rung function to the first quark field, subtracts the rung of the second quark field, and adds the binding field.
why it matters
This definition supplies the rung argument to hadron_mass, which multiplies the coherence energy by phi raised to the composite rung, and to the degeneracy theorem hadron_equal_z_degenerate. It realizes the Recognition Science mass formula on composite states, consistent with the eight-tick octave and the phi-ladder spacing that underlies Regge trajectories in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.