quarter_eq
plain-language theorem explainer
The quarter-ladder embedding satisfies quarter(k) = k/4 for any integer k. Modelers of quark masses or neutrino ladders in the Recognition framework cite this to maintain uniform fractional rung conventions. The proof reduces immediately to reflexivity on the defining equation of the quarter embedding.
Claim. For any integer $k$, the quarter-ladder map satisfies quarter$(k) = k/4$ in the rationals.
background
The module supplies a minimal representation for fractional rungs on the φ-ladder. Core mass models employ integer rungs for rigidity, while selected physics modules (quark masses, neutrino refinements) adopt fractional placements such as quarter steps to match observed ratios. The file records the convention explicitly as a reporting seam rather than a derivation of canonicity.
proof idea
The proof is a one-line reflexivity that matches the theorem statement directly to the definition of quarter.
why it matters
This equality anchors the fractional rung convention inside the Recognition mass formula (yardstick times phi to the power of rung offset). It supports downstream refinements in quark and neutrino sectors without altering the integer core or invoking the T0-T8 forcing chain, RCL, or J-uniqueness. The module functions as an explicit seam rather than a proved physical necessity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.