toInt_mk
The recovery map toInt applied to the constructor mk a b yields the integer difference of the iteration counts of a and b. Workers on the integer layer of the Recognition Science foundation cite this when confirming that the quotient construction reproduces standard integer arithmetic. The proof reduces immediately by reflexivity once the definitions of mk and toInt are unfolded.
claimFor LogicNat elements $a$ and $b$, the integer recovery map satisfies $toInt([a, b]_ℓ) = toNat(a) - toNat(b)$.
background
LogicNat is the inductive type with constructors identity (representing the zero-cost element) and step (one iteration of the generator), mirroring the orbit {1, γ, γ², ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. The function toNat reads off the iteration count: identity maps to 0 and step n to the successor of toNat n. The mk constructor forms a LogicInt as the quotient of pairs (a, b) representing a − b, while toInt lifts the core difference map to the quotient.
proof idea
The proof is a one-line wrapper that applies the definitions of mk and toInt. Reflexivity holds because toInt (mk a b) is defined to be exactly toNat a − toNat b.
why it matters in Recognition Science
This result is invoked by the surrounding theorems that establish toInt as a ring homomorphism, including toInt_add, toInt_mul, toInt_neg, toInt_one, toInt_zero, toInt_fromInt, and fromInt_toInt. It closes the basic compatibility between the LogicInt construction and the standard integers, allowing Recognition Science arithmetic to inherit the properties of ℤ. In the forcing chain this supports the embedding of integer quantities into the J-cost and phi-ladder structures.
scope and limits
- Does not establish that toInt is injective on LogicInt.
- Does not address compatibility with addition or multiplication.
- Does not connect to J-uniqueness or the phi fixed point.
- Does not treat the rational or real extensions.
formal statement (Lean)
204@[simp] theorem toInt_mk (a b : LogicNat) :
205 toInt (mk a b) = (toNat a : Int) - toNat b := rfl
proof body
206