quarter
plain-language theorem explainer
The quarter definition embeds each integer k as the rational k/4, supplying a uniform quarter-step placement on the phi-ladder for mass and state calculations. Modelers of fractional rung effects in quark sectors or neutrino ladders cite it to keep embeddings consistent across modules. The definition is a direct coercion from integers through rationals, inheriting simplification rules automatically.
Claim. The quarter-ladder embedding is given by $quarter(k) := k/4$ for $k ∈ ℤ$, where a rung is an element of $ℚ$ representing a (possibly fractional) position on the $φ$-ladder.
background
The Rung type is an abbreviation for the rationals, allowing fractional positions on the phi-ladder beyond the integer rungs used in the core mass model. This module supplies a minimal, type-light representation for such fractional rungs to support physics modules exploring quarter-ladder placements for observed ratios. Upstream, the half embedding performs the analogous division by 2, and lemmas in PhiClosed establish closure properties under inversion for these fractions.
proof idea
This is a one-line definition that coerces the integer k to a rational and divides by 4, yielding an element of the Rung type. It mirrors the structure of the sibling half definition and carries the simp attribute for automatic rewriting.
why it matters
This declaration supports downstream results such as down_generation_ordering in the quark mass sector and C_xi_pos in gravity parameters, as well as bounds on phi powers in the numerics module. It implements the representation seam described in the module documentation for fractional rung conventions, enabling uniform handling without yet proving canonicity. In the Recognition Science framework it connects to the phi-ladder mass formula by allowing rung adjustments like gap(Z) to include quarter steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.