toInt_one
plain-language theorem explainer
The theorem establishes that the logic integer one, formed as the successor of zero in the logic naturals, maps under toInt to the standard integer 1. Researchers building the arithmetic foundation in Recognition Science cite this when verifying ring identities for the constructed integers. The proof reduces the claim by substituting the mk constructor for one, applying the successor and zero mappings from the naturals, and normalizing the resulting expression.
Claim. Let $Z_ℓ$ denote the Grothendieck completion of the logic naturals. Then $toInt(1) = 1$, where $1$ is the class $[succ(0), 0]_ℓ$ in $Z_ℓ$.
background
LogicNat is defined inductively with an identity constructor representing the zero-cost element and a step constructor for iteration of the generator, mirroring the orbit under multiplication by γ. LogicInt is the quotient setoid completion of pairs of LogicNat elements, allowing representation of integers as differences a − b. The toInt map sends the equivalence class of (a, b) to the difference of their toNat images in the standard naturals. This sits in the IntegersFromLogic module, which constructs integers after the naturals in ArithmeticFromLogic, prior to rationals. Upstream results include toNat_zero : toNat zero = 0 and toNat_succ : toNat (succ n) = Nat.succ (toNat n), which are used to compute the image of the unit element.
proof idea
The proof proceeds by first showing that the logic integer 1 equals mk (LogicNat.succ LogicNat.zero) LogicNat.zero. It then rewrites using toInt_mk to reduce to a difference of toNat values, applies toNat_succ and toNat_zero to obtain 1 - 0, and concludes with norm_num.
why it matters
This theorem is invoked in the proofs of mul_one' and one_mul' to establish that multiplication by one is the identity on logic integers. It also supports the definitions of one and ofLogicInt in the rationals module, as well as toRat_one. It forms part of the base arithmetic layer that precedes the forcing chain T0-T8 and the Recognition Composition Law in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.