isInitial
The definition packages the recursor of any Lawvere natural-number object into the unique homomorphism required for initiality of the associated Peano algebra. Researchers deriving arithmetic from categorical forcing in Recognition Science cite it to confirm that the forced numbers satisfy the universal property without external Nat. The construction directly supplies the lift from the recursor fields and obtains uniqueness by applying the recursor uniqueness clause twice followed by functional extensionality.
claimLet $(N,z,s)$ be a Lawvere natural-number object. Then the Peano algebra with carrier $N$, zero $z$ and successor $s$ is initial: for every other Peano algebra $B$ there exists a unique homomorphism $N→B$ that preserves zero and commutes with successor.
background
The module characterises the natural numbers forced by the Law of Logic via the Lawvere universal property: a triple $(N,z,s)$ is a natural-number object when, for every pointed endomap $(X,x,f)$, there is a unique map $h:N→X$ with $h(z)=x$ and $h∘s=f∘h$. This is captured by the structure IsNaturalNumberObject, whose recursor field supplies the unique map and whose recursor_unique field enforces uniqueness. The local setting is the categorical foundation in which arithmetic arises from the orbit under the generator without presupposing ℕ. Upstream, PeanoObject is the plain algebra (carrier, zero, step) and IsInitial asserts the existence of a unique homomorphism to any other such algebra; LogicNat supplies the concrete forced carrier with identity and step constructors.
proof idea
The definition builds the IsInitial structure by setting the lift to the recursor supplied by the hypothesis. Zero and step preservation are taken verbatim from the recursor_zero and recursor_step fields. Uniqueness proceeds by functional extensionality, applying the recursor_unique property once to each candidate map and equating the results.
why it matters in Recognition Science
It supplies the concrete link between the Lawvere natural-number object and initiality in the category of Peano algebras, completing one of the four main results listed in the module documentation. The construction ensures that every realization of the forced arithmetic, including the discrete Boolean one, yields the same iteration object. In the Recognition framework this aligns with the derivation of arithmetic from the J-uniqueness fixed point and the eight-tick octave without smuggling in external counting.
scope and limits
- Does not compute concrete values of the recursor for specific target algebras.
- Does not address induction principles beyond the basic recursor.
- Applies only to pointed endomap algebras; does not treat other categorical structures.
- Does not rule out non-standard models of the axioms.
formal statement (Lean)
68def isInitial (h : IsNaturalNumberObject z s) :
69 PeanoObject.IsInitial (toPeano h) where
70 lift := fun B =>
proof body
Definition body.
71 { toFun := h.recursor B.zero B.step
72 map_zero := h.recursor_zero B.zero B.step
73 map_step := fun n => h.recursor_step B.zero B.step n }
74 uniq := by
75 intro B f g
76 funext n
77 have hf := h.recursor_unique B.zero B.step f.toFun f.map_zero f.map_step n
78 have hg := h.recursor_unique B.zero B.step g.toFun g.map_zero g.map_step n
79 rw [hf, hg]
80
81end IsNaturalNumberObject
82
83/-! ## `LogicNat` is a natural-number object -/
84
85/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/