ofLogicNat_zero
The canonical embedding of logic-forced natural numbers into their Grothendieck completion sends the zero element to the class of the pair (zero, zero). Researchers building the arithmetic hierarchy in Recognition Science cite this when confirming that the additive identity is preserved under the embedding from the monoid to the group. The proof is a one-line reflexivity reduction that matches the definitions of the embedding and the pair constructor.
claimLet $N_L$ be the natural numbers generated by the Law of Logic and let $Z_L$ be their Grothendieck completion under addition. The canonical embedding $i: N_L to Z_L$ satisfies $i(0_L) = [0_L, 0_L]_L$, where $[a,b]_L$ denotes the class of the pair $(a,b)$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the base element. LogicInt is the quotient of pairs of LogicNat elements under the relation identifying (a,b) with (c,d) when a + d = b + c, yielding the Grothendieck group completion. The map ofLogicNat sends each natural n to the class [n, zero], embedding the additive monoid into the group. This sits inside the module that constructs integers directly from the logic-forced naturals, immediately after the arithmetic definitions in the sibling module.
proof idea
The proof is a one-line term-mode reflexivity that unfolds the definition of the embedding as the pair constructor applied to (n, zero) and instantiates n at zero, matching the right-hand side directly.
why it matters in Recognition Science
This identity confirms preservation of the zero element when passing from the logic-derived naturals to integers. It supports later construction of rationals and the full number system in the Recognition framework, consistent with the forcing chain that derives the integer layer as part of the T0-T8 sequence. No open questions are addressed here.
scope and limits
- Does not prove that [0,0] is the additive identity in the completed group.
- Does not detail the equivalence relation or quotient axioms.
- Does not treat negative elements or arithmetic operations.
- Does not link to physical constants or the phi-ladder.
formal statement (Lean)
100@[simp] theorem ofLogicNat_zero : ofLogicNat LogicNat.zero = mk LogicNat.zero LogicNat.zero := rfl
proof body
Term-mode proof.
101
102/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
103
104/-- Zero in `LogicInt`. -/