half
plain-language theorem explainer
The half-ladder map sends an integer rung k to the rational position k/2 on the phi-ladder. Modules that refine mass ratios or orbital scales with fractional placements cite this convention to maintain uniformity across integer and half-integer assignments. The definition is realized by a direct coercion from integers to rationals followed by division by two.
Claim. The half-ladder embedding is the map $k/2$ for $k$ an integer, with the result viewed as a (possibly fractional) rung on the phi-ladder.
background
Rung is the type of rational numbers, introduced to allow fractional placements on the phi-ladder while the core mass model retains integer rungs for rigidity. The module supplies this representation seam so that physics modules exploring quarter- or half-ladder refinements (quark masses, neutrino ladders) share a mechanically uniform convention. Upstream rung definitions in Constants, AnchorPolicy, and RSBridge.Anchor supply the integer assignments that this map halves.
proof idea
This is a definition, not a theorem. It is realized by coercing the integer argument to a rational and dividing by two, with the simp attribute attached for automatic simplification in downstream expressions.
why it matters
The definition feeds AgreesAtHalfRung and planetaryFormationCert in astrophysics, pleasure_symmetric in aesthetics, and cross_cousin_count in anthropology. It closes the representation seam described in the module doc-comment, allowing the phi-ladder mass formula and T5 J-uniqueness to be applied uniformly to half-integer rungs without altering the integer core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.