zero
The definition supplies the additive identity of the quotient field built from LogicInt by instantiating the mk constructor on the pair (0,1) and discharging the nonzero-denominator side condition. Foundation-layer work on Recognition Science number systems cites this when extending the integer construction to rationals. The body is a direct constructor application whose only nontrivial step invokes the integer recovery maps toInt_zero and toInt_one to obtain a contradiction with one_ne_zero.
claimDefine the zero element of the quotient field of fractions of LogicInt by the class of the pair (0,1) whose second component is nonzero.
background
LogicRat is the field of fractions of LogicInt, itself the Grothendieck completion of LogicNat under addition. The constructor mk forms an element of LogicRat from a pair of LogicInt values provided the second (denominator) component is nonzero. Upstream results supply the recovery map toInt : LogicInt → Int together with the explicit theorems toInt_zero and toInt_one that identify the images of the zero and unit elements.
proof idea
One-line wrapper that applies the mk constructor to the pair (0,1) and discharges the side condition by a short tactic block: assume the denominator equals zero, transport via toInt to obtain toInt(1) = toInt(0), rewrite with toInt_one and toInt_zero, then apply one_ne_zero.
why it matters in Recognition Science
This definition completes the basic constants needed to equip the quotient field with its ring operations inside the Recognition Science foundation layer. It sits immediately after the setoid and LogicRat construction and precedes the one element; together they allow the later definition of addition, multiplication, and the embedding of LogicInt. No open scaffolding remains at this node.
scope and limits
- Does not establish that LogicRat satisfies the field axioms.
- Does not define addition or multiplication on LogicRat.
- Does not prove uniqueness of the zero element.
- Does not relate LogicRat.zero to the zero of LogicInt via any embedding.
formal statement (Lean)
109def zero : LogicRat :=
proof body
Definition body.
110 mk 0 1 (by
111 intro h
112 have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
113 rw [toInt_one, toInt_zero] at this
114 exact one_ne_zero this)
115
116/-- One in `LogicRat`. -/