quarter_eq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove physical necessity or canonicity of quarter rungs.
- Does not supply conversion from rational rungs to real exponents for rpow.
- Does not interact with the Recognition Composition Law or J-uniqueness.
- Does not constrain phi-ladder spacing or mass gaps beyond the embedding definition.
formal statement (Lean)
36theorem quarter_eq (k : ℤ) : quarter k = (k : ℚ) / 4 := rfl