zero
plain-language theorem explainer
The zero element in the logic integers is introduced as the equivalence class of the pair of zero logic naturals. Researchers constructing the arithmetic hierarchy from the forced naturals in Recognition Science cite this when establishing the additive identity for the Grothendieck completion. It is supplied by a direct definition that applies the pair constructor to the zero of the logic naturals.
Claim. Let $Z_L$ be the Grothendieck completion of the logic natural numbers $N_L$ under addition. The zero element is $0_L := [0_N, 0_N]_L$, where $[a,b]_L$ denotes the equivalence class of the pair $(a,b)$ of logic naturals.
background
Logic natural numbers are the inductive type with an identity constructor (the zero-cost multiplicative identity) and a step constructor that iterates the generator, forming the smallest orbit closed under multiplication by the forced constant. Logic integers are the quotient of pairs of these naturals by the equivalence that identifies $(a,b)$ with $(c,d)$ precisely when $a+d = b+c$, yielding the Grothendieck group completion under addition. The local module builds the integers directly from the arithmetic layer that supplies the logic naturals.
proof idea
Direct definition that applies the pair constructor to the zero logic natural in each component.
why it matters
This supplies the additive identity required for the integer ring that later feeds the construction of rationals and the full number system. It completes the base case in the passage from the forced naturals to the integers within the Recognition Science foundation. No downstream theorems are recorded in the current graph, so the declaration remains a pure base definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.