Hom
The Hom structure encodes maps between Peano algebras that send zero to zero and commute with the successor operation. Researchers deriving arithmetic from logic realizations or proving uniqueness of initial objects in Recognition Science cite it when constructing lifts. It is introduced as a plain record with three fields and no proof obligations.
claimA homomorphism between Peano algebras $A$ and $B$ is a function $f: A.carrier → B.carrier$ satisfying $f(A.zero) = B.zero$ and $f(A.step(x)) = B.step(f(x))$ for all $x$.
background
PeanoObject is the structure with a carrier type, zero element, and successor map step; this module extracts arithmetic from an abstract Law-of-Logic realization. The local setting emphasizes initiality: once a realization supplies identity and step data, the generated Peano algebra is initial, yielding unique isomorphisms. Upstream, the Identity definition from LogicAsFunctionalEquation enforces zero comparison cost for self-equality, while the step operation from CellularAutomata supplies the successor rule used in the preservation axioms.
proof idea
Direct record definition declaring the three fields toFun, map_zero, and map_step. No lemmas or tactics are invoked; the structure simply packages the carrier map together with the two preservation conditions.
why it matters in Recognition Science
Hom supplies the morphisms required to formulate IsInitial and the unique lift in equivOfInitial and logicNatLift. It implements the initiality mechanism behind Universal Forcing, where arithmetic is extracted from the logic functional equation. The definition feeds composition and identity homomorphisms that close the category of Peano objects.
scope and limits
- Does not assert existence of a homomorphism between arbitrary Peano objects.
- Does not impose continuity, measurability, or other analytic conditions on the map.
- Does not address preservation of derived operations such as addition or multiplication.
formal statement (Lean)
31structure Hom (A B : PeanoObject) where
32 toFun : A.carrier → B.carrier
33 map_zero : toFun A.zero = B.zero
34 map_step : ∀ x : A.carrier, toFun (A.step x) = B.step (toFun x)
35
36namespace Hom
37
38instance (A B : PeanoObject) : CoeFun (Hom A B) (fun _ => A.carrier → B.carrier) where
39 coe f := f.toFun
proof body
Definition body.
40
41/-- Identity homomorphism. -/