realizationLift
Supplies the homomorphism from the Peano algebra extracted from a logic realization orbit to an arbitrary target Peano algebra. Workers on initiality and universal forcing cite it to witness the lift component of the initial object. Construction installs realizationFold as the carrier map and verifies zero and successor preservation by rewriting through the orbit equivalence to LogicNat.
claimLet $R$ be a logic realization and $B$ a Peano algebra. The map $R.Orbit → B$ defined by $n ↦ (logicNatLift B)(R.orbitEquivLogicNat n)$ preserves zero and successor, hence yields a homomorphism from the Peano algebra with carrier $R.Orbit$, zero $R.orbitZero$ and step $R.orbitStep$ to $B$.
background
PeanoObject is a structure with a carrier type, a zero element and a successor map. Hom is the structure of functions between two PeanoObjects that send zero to zero and commute with successor. The module extracts arithmetic from an abstract Law-of-Logic realization by packaging its orbit as the initial Peano algebra; the orbit carries certified zero and step operations equivalent to the standard naturals via orbitEquivLogicNat. Upstream, realizationPeano packages the orbit into a PeanoObject while realizationFold defines the recursive map by composing the equivalence with logicNatLift.
proof idea
The definition sets toFun to realizationFold R B. map_zero unfolds the fold, rewrites by R.orbitEquiv_zero and reduces to B.zero. map_step unfolds, rewrites by R.orbitEquiv_step and reduces using that logicNatLift preserves successor.
why it matters in Recognition Science
Supplies the lift required by realization_initial to prove that realizationPeano R is initial in the category of Peano algebras. It realizes the initiality mechanism the module documentation identifies as the basis for Universal Forcing. In the Recognition framework this step closes extraction of arithmetic from logic realizations and supports the forcing chain from logic data to Peano structure.
scope and limits
- Does not prove uniqueness of the homomorphism.
- Does not construct realizations from scratch.
- Does not address properties beyond zero and successor preservation.
- Does not depend on the concrete cellular automaton rule.
Lean usage
def example (R : LogicRealization) (B : PeanoObject) : PeanoObject.Hom (realizationPeano R) B := realizationLift R Bformal statement (Lean)
134def realizationLift (R : LogicRealization) (B : PeanoObject) :
135 PeanoObject.Hom (realizationPeano R) B where
136 toFun := realizationFold R B
proof body
Definition body.
137 map_zero := by
138 unfold realizationFold
139 change (logicNatLift B).toFun (R.orbitEquivLogicNat R.orbitZero) = B.zero
140 rw [R.orbitEquiv_zero]
141 rfl
142 map_step := by
143 intro x
144 unfold realizationFold
145 change (logicNatLift B).toFun (R.orbitEquivLogicNat (R.orbitStep x)) =
146 B.step ((logicNatLift B).toFun (R.orbitEquivLogicNat x))
147 rw [R.orbitEquiv_step]
148 rfl
149