one
plain-language theorem explainer
The definition supplies the multiplicative unit inside LogicRat, the quotient field of LogicInt pairs. Foundation-layer users cite it when the cost functionals or symmetry arguments need the standard rational 1. The construction applies the mk constructor to the pair of LogicInt ones and discharges the nonzero-denominator condition by transporting the integer fact 1 ≠ 0 through the recovery map toInt.
Claim. Let $1$ denote the multiplicative identity in the field of fractions $LogicRat$ of $LogicInt$. Then $1 := mk(1,1)$ where $mk$ forms the class of a pair whose second component is nonzero, verified by transporting the equality $toInt(1) = 1$ and $toInt(0) = 0$ through the embedding $toInt : LogicInt → Int$.
background
LogicRat is the quotient of PreRat pairs by the setoid equivalence, yielding the field of fractions over LogicInt. LogicInt itself is the Grothendieck completion of LogicNat under addition, with constructor mk forming classes [a, b]ₗ. The recovery map toInt : LogicInt → Int satisfies toInt_one : toInt(1 : LogicInt) = 1 and toInt_zero : toInt(0 : LogicInt) = 0, both proved by direct reduction on the underlying mk terms.
proof idea
Direct definition that calls the mk constructor on the pair (1,1) from LogicInt. The nonzero-denominator obligation is met by assuming the pair equals the zero class, applying congrArg toInt, rewriting with toInt_one and toInt_zero, then invoking one_ne_zero.
why it matters
This unit is required by downstream results including costRateEL_implies_const_one (which forces admissible paths to the constant 1) and the convexity statements actionJ_convex_on_interp and actionJ_local_min_is_global. It completes the rational arithmetic layer that supports J-cost evaluations and the Recognition Composition Law in the forcing chain from T0 through T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.