PreRat
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not define field operations on the pairs.
- Does not verify the equivalence relation properties.
- Does not provide an embedding into the real numbers.
- Does not address ordering or positivity.
formal statement (Lean)
40structure PreRat where
41 num : LogicInt
42 den : LogicInt
43 den_nonzero : den ≠ 0
44
45/-- The field-of-fractions equivalence: `(a, b) ~ (c, d)` iff
46`a * d = c * b`. -/