hadron_equal_z_degenerate
plain-language theorem explainer
Hadrons sharing the same effective rung (quark rung difference plus binding) have identical masses at leading order. Researchers modeling Regge trajectories or rho/omega degeneracy in hadron spectroscopy would cite this for equal-Z relations. The proof is a one-line simplification that unfolds the mass definition under the rung equality hypothesis.
Claim. If two hadrons $h_1$ and $h_2$ satisfy composite rung$(h_1)=$ composite rung$(h_2)$, where the composite rung is the sum of the first fermion rung, the negative of the second fermion rung, and the binding integer, then their masses coincide: $m(h_1)=m(h_2)$.
background
The Hadron structure models simple mesons as pairs of fermions (quarks) together with an integer binding defaulting to 1. The composite rung function computes the effective level as rung(q1) minus rung(q2) plus binding, placing the hadron on the phi-ladder for mass assignment. This module derives leading-order masses and Regge trajectories m^2 = n alpha' phi^{2r} from these rungs, with eight-beat binding supplying the offset; the local setting is Phase 6 scaffolding for hadron mass relations and rho/omega degeneracy from equal effective Z.
proof idea
The proof is a one-line wrapper that applies simp to the hadron mass definition together with the rung equality hypothesis, reducing both sides to the same expression on the phi-ladder.
why it matters
This result supplies the degeneracy step needed for equal-Z relations such as rho/omega in the hadron mass module. It supports the Regge slope derivations that follow from phi-tier spacing and eight-beat binding. The module remains Phase 6 scaffolding, outside Level A completion, and connects to the eight-tick octave structure via the binding term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.