ofLogicNat
plain-language theorem explainer
The definition supplies the canonical embedding of logic natural numbers into logic integers by sending each n to the class of the pair (n, zero). Foundation researchers building the integers as the Grothendieck group of the additive monoid would invoke this map when extending operations. It is introduced directly via the pair constructor applied to the input and the zero element.
Claim. The map from the logic natural numbers to the logic integers defined by $nmapsto [n,0]$, where $[a,b]$ denotes the equivalence class of the pair $(a,b)$ in the quotient realizing the Grothendieck group completion of the additive monoid.
background
LogicNat is the inductive type of natural numbers forced by the Law of Logic, generated by an identity constructor (the zero-cost element) and a step constructor that iterates the generator, mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. LogicInt is the quotient of pairs of logic naturals by the setoid equivalence that identifies (a,b) with (c,d) precisely when a+d equals b+c, yielding the Grothendieck group completion of the additive monoid. The upstream inductive definition of LogicNat from ArithmeticFromLogic supplies the monoid whose group completion is formed here.
proof idea
One-line definition that applies the mk constructor to the input n and the zero element of LogicNat.
why it matters
This embedding is required to define zero and one in LogicInt and to prove the basic identity ofLogicNat_zero. It completes the passage from the additive monoid of logic naturals to the integers in the foundation layer. In the Recognition Science framework it supports the number system underlying the phi-ladder and mass formulas by furnishing the integers needed for the Grothendieck completion step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.