IsNaturalNumberObject
plain-language theorem explainer
The Lawvere natural-number object is a triple (N, z, s) equipped with a unique recursion operator that satisfies the zero and successor equations for every target pointed endomap. Categorical foundations researchers and Recognition Science workers cite it to certify that arithmetic forced by the Law of Logic is initial among such algebras. The declaration is a structure definition that directly encodes existence and uniqueness of the recursor without reference to any concrete Nat.
Claim. A triple $(N, z, s)$ with $z : N$ and $s : N → N$ is a natural-number object when equipped with a recursor operation $r : ∀X, X → (X → X) → N → X$ satisfying $r(x,f,z) = x$, $r(x,f,s(n)) = f(r(x,f,n))$, and the uniqueness property that any $h : N → X$ obeying $h(z) = x$ and $h(s(n)) = f(h(n))$ coincides with $r$.
background
Recognition Science derives arithmetic from the Law of Logic rather than postulating it. The module characterizes the forced iteration object categorically as the initial pointed endomap algebra: for any target $(X, x, f)$ there exists a unique $h : N → X$ with $h(z) = x$ and $h ∘ s = f ∘ h$. Upstream, LogicNat is the inductive orbit {identity, step} that is the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity; its doc-comment states that identity represents the zero-cost element and step represents one more iteration.
proof idea
This is a structure definition that packages the four fields (recursor map together with its zero, step, and uniqueness axioms) directly from the Lawvere universal property. No tactics or lemmas are applied; the declaration itself serves as the interface that downstream constructions instantiate for specific carriers such as LogicNat and Tick.
why it matters
The structure is the central interface used to prove that Tick with tickZero and tickSucc satisfies the natural-number object property and is canonically equivalent to LogicNat, yielding the TimeAsOrbitCert. It fills the categorical foundation step by showing that the arithmetic forced from the Law of Logic is initial, supporting the eight-tick octave and the emergence of D = 3 from the same object. Downstream results such as tick_orbit_eq_logicNat rely on it to equate temporal iteration with the recognition orbit across realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Point-free relations recovered from a parallel pair of frame operators
"The main result is an adjunction with identity counit between the category of locales equipped with open cone localic relations, and the opposite of the category of conic frames."