mk
plain-language theorem explainer
The definition supplies the standard constructor for elements of the rational field obtained as the field of fractions of the logic integers. Workers on the Recognition Science ledger algebra cite it to form quotients from integer pairs. The implementation is a direct application of the quotient maker to the pre-rational record.
Claim. The map sending a pair of logic integers $(a, b)$ with $b ≠ 0$ to its equivalence class in the field of fractions of the logic integers.
background
The logic integers are the Grothendieck completion of the logic naturals under addition, formed as the quotient of pairs of naturals. The rational field is defined as the quotient of the pre-rational setoid, making it the field of fractions over the logic integers. This construction sits in the foundation layer deriving number systems directly from logic without external arithmetic.
proof idea
One-line wrapper that applies the quotient constructor to the pre-rational triple formed by the two logic integers and the proof that the second is nonzero.
why it matters
This constructor feeds the ledger algebra proof that paired events sum to zero and supports definitions of elements in the phi-ring. It completes the passage from integers to rationals in the foundation, enabling rational coefficients on the phi-ladder that appear in mass formulas and the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.