isInitial
plain-language theorem explainer
Any Lawvere natural-number object (N, z, s) yields an initial Peano algebra under the toPeano construction. Categorical arithmetic researchers in Recognition Science cite this to link the forced iteration object to Peano initiality without presupposing numbers. The definition directly supplies the unique lift map via the recursor and verifies uniqueness from the NNO uniqueness axiom.
Claim. Let $(N, z, s)$ be a Lawvere natural-number object. Then the Peano algebra obtained from it is initial: for every Peano algebra $B$ there exists a unique homomorphism from the obtained algebra to $B$.
background
A Lawvere natural-number object consists of a type N with zero z and successor s such that for any pointed endomap (X, x, f) there is a unique map h: N → X satisfying the recursion equations. This is defined with fields recursor, recursor_zero, recursor_step, and recursor_unique. PeanoObject is a carrier with zero and step. IsInitial provides a lift homomorphism to any other PeanoObject together with uniqueness of that lift. The module establishes that the arithmetic forced by the Law of Logic satisfies the Lawvere universal property, making ℕ the initial pointed endomap algebra in any categorical foundation without presupposing numbers.
proof idea
The definition constructs the IsInitial structure. The lift is defined by applying the recursor of the NNO to the zero and step of the target B. Uniqueness follows by applying the recursor_unique field to both candidate maps and rewriting.
why it matters
This definition bridges the Lawvere NNO characterization to the initiality property in the Peano algebra category. It supports the module's goal of showing that LogicNat with identity and step forms a natural-number object and that every realization's forced arithmetic is a natural-number object. It addresses the concern that iteration-counting might be smuggled in by confirming the iteration object is the same across realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.