PreRat
plain-language theorem explainer
The pre-rational structure supplies pairs of logic integers that become the rationals after quotienting by the cross-multiplication equivalence. It is cited whenever the rational field is constructed or its operations are defined. The declaration consists of a direct structure with a non-zero denominator constraint.
Claim. A pre-rational is a pair of integers $(n, d)$ with $d ≠ 0$, where the integers arise as the Grothendieck completion of the logic naturals.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as a quotient of pairs of logic naturals. PreRat takes pairs from this type and adds the single constraint that the denominator is nonzero. This carrier is then equipped with the relation ratRel, defined by cross-multiplication equality, whose quotient produces the rationals.
proof idea
The declaration is a direct structure definition. It introduces the three fields without applying any lemmas or tactics.
why it matters
This structure is the immediate predecessor to LogicRat, the rational field used in all subsequent arithmetic. It supports the definitions of addition, multiplication, and negation on the quotients. In the Recognition Science chain, the rationals enable the precise statements of the phi-ladder mass formulas and the eight-tick dynamics. It fills the step from integers to rationals in the foundation, directly feeding the constructions in NucleosynthesisTiers and LedgerFactorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.