toNat_zero
plain-language theorem explainer
The iteration-count map from logic naturals to ordinary naturals sends the zero element to zero. Recovery theorems for addition, multiplication, and integer embeddings cite this as the base case. The proof reduces immediately by reflexivity once the recursive definition of the map is unfolded.
Claim. Let $phi : mathbb{N}_{Logic} to mathbb{N}$ be the iteration-count map with $phi(text{identity}) = 0$ and $phi(text{step } n) = text{succ}(phi(n))$. Then $phi(0_{Logic}) = 0$.
background
The module ArithmeticFromLogic builds natural-number arithmetic on the inductive type LogicNat whose constructors are identity (serving as zero) and step. The function toNat is defined by recursion on this type: identity maps to 0 while step n maps to the successor of toNat n. This construction sits in the foundation layer that extracts arithmetic directly from the functional equation of Recognition Science.
proof idea
The proof is a one-line reflexivity after the definition of toNat on the identity constructor is applied.
why it matters
This base case is invoked by the recovery theorems toNat_add and toNat_mul that establish agreement between logic operations and ordinary arithmetic. It also supports toInt_zero, toInt_fromInt, and the ordered realization natOrderedRealization. In the Recognition framework it anchors the translation between the logic carrier and standard naturals before lifting to integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.