ofInt
plain-language theorem explainer
The integer-to-rung embedding converts an integer into a rational value for use on the φ-ladder. Neutrino sector calculations and spin statistics modules cite it when adding fractional offsets to integer bases. It is realized as a direct type coercion from integers to rationals with a simplification attribute.
Claim. The embedding from integers to rungs is defined by sending each integer $z$ to the rational $z$, where rungs are represented by the rational numbers as possibly fractional positions on the $φ$-ladder.
background
This module defines a lightweight type for fractional rungs on the φ-ladder to support refinements in mass models. The rung type is the set of rational numbers. This permits constructions such as quarter-ladder embeddings while keeping the core model on integers. The module documentation describes it as a representation seam that makes the convention for fractional placements explicit and uniform without asserting canonicity. It parallels an upstream construction in the spin statistics module that builds spin values from integers.
proof idea
The definition is a direct coercion of the input integer to a rational number. It requires no lemmas and consists of a single line with the simp attribute for automatic rewriting.
why it matters
This embedding is used to construct the upgraded neutrino rung that combines an integer base with a quarter offset, as well as in spin and unit gate definitions. It supports the Recognition Science approach to mass ladders by allowing fractional adjustments to match observed ratios within the phi-ladder framework. It leaves open whether such fractions are forced by the underlying axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.