pith. machine review for the scientific record. sign in
def definition def or abbrev high

one

show as:
view Lean formalization →

The multiplicative unit in the field of fractions of the integers obtained from the Grothendieck construction on logic naturals is supplied by pairing the integer unit with itself. Researchers building the cost functional or the phi-ladder in Recognition Science cite this when normalizing paths or actions to the fixed point at one. The definition applies the quotient constructor and discharges the nonzero-denominator condition by transporting the integer inequality through the recovery map to the standard integers.

claimLet $Q$ be the field of fractions of the integers $Z$ obtained as the Grothendieck completion of the logic naturals. The multiplicative identity $1_Q$ is the equivalence class of the pair $(1_Z,1_Z)$, where $1_Z$ is the successor of zero in $Z$, with the denominator verified nonzero via the bijection from $Z$ to the standard integers.

background

LogicRat is the quotient of PreRat pairs by the setoid ratRel, forming the field of fractions of LogicInt. LogicInt arises as the quotient of pairs of logic naturals under the Grothendieck equivalence for addition, with the constructor mk forming elements from such pairs. The upstream recovery map toInt supplies the bijection to standard integers, and the theorems toInt_one and toInt_zero fix the images of the unit and zero under this map.

proof idea

The definition applies the mk constructor to the pair of the integer unit with itself. The nonzero-denominator obligation is met by assuming equality to zero, applying congrArg toInt to obtain equality of the recovered integers, then rewriting with toInt_one and toInt_zero to reach the known integer inequality one_ne_zero.

why it matters in Recognition Science

This unit is required by downstream results including costRateEL_implies_const_one, which proves that critical points of the cost-rate action are constantly one, and the convexity statements actionJ_convex_on_interp together with actionJ_local_min_is_global in FunctionalConvexity. It completes the rational layer needed for the J-cost minimum at the self-similar fixed point and for the eight-tick octave in the forcing chain.

scope and limits

formal statement (Lean)

 117def one : LogicRat :=

proof body

Definition body.

 118  mk 1 1 (by
 119    intro h
 120    have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
 121    rw [toInt_one, toInt_zero] at this
 122    exact one_ne_zero this)
 123
 124instance : Zero LogicRat := ⟨zero⟩
 125instance : One LogicRat := ⟨one⟩
 126
 127/-- Negation: `-(a/b) = (-a)/b`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.