IsInitial
IsInitial packages the universal property of an initial Peano algebra: a unique homomorphism exists from it to every other Peano algebra. Researchers extracting arithmetic from logic realizations or constructing Lawvere natural-number objects cite it to guarantee uniqueness up to unique isomorphism. The declaration is a bare structure definition that records the lift and uniqueness data with no further proof obligations.
claimA Peano algebra $A$ is initial when, for every Peano algebra $B$, there exists a homomorphism $A$ to $B$ and any two such homomorphisms agree on their underlying functions.
background
PeanoObject consists of a carrier type equipped with a zero element and a successor map. Hom records the structure-preserving maps between two such objects, requiring that zero is sent to zero and successor commutes with the map. The module ArithmeticOf extracts arithmetic from a Law-of-Logic realization precisely by exhibiting an object that satisfies this initiality condition, which supplies the uniqueness mechanism behind Universal Forcing.
proof idea
This is a structure definition that directly records the two fields lift and uniq; no tactics or lemmas are applied.
why it matters in Recognition Science
It supplies the initiality data required by the ArithmeticOf structure and by the concrete constructions logicNat_initial and realization_initial. The same data appears in LawvereNNO and in the NaturalNumberObject.isInitial wrapper. The declaration therefore closes the step from a logic realization to a unique arithmetic object, consistent with the initial-object uniqueness that drives the forcing chain.
scope and limits
- Does not construct any concrete Peano object.
- Does not prove existence of an initial object.
- Does not encode physical constants or dimensional constraints.
- Does not supply the actual lift or uniqueness proofs for any specific algebra.
formal statement (Lean)
58structure IsInitial (A : PeanoObject) where
59 lift : ∀ B : PeanoObject, Hom A B
60 uniq : ∀ (B : PeanoObject) (f g : Hom A B), f.toFun = g.toFun
61
62end PeanoObject
63
64/-- The arithmetic object forced by a Law-of-Logic realization. -/