realizationLift
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.