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

mk

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  87def mk (a b : LogicInt) (hb : b ≠ 0) : LogicRat :=

proof body

Definition body.

  88  Quotient.mk' ⟨a, b, hb⟩
  89

used by (40)

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

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.