realizationFold
plain-language theorem explainer
The definition supplies a canonical map from the orbit of any logic realization into the carrier of an arbitrary Peano algebra. It routes through the certified equivalence of the orbit with LogicNat and then applies the primitive recursion lift. Researchers extracting initial arithmetic objects from logic realizations cite it when constructing homomorphisms to target Peano algebras. The construction is a direct one-line composition of the orbit equivalence with the logicNat lift.
Claim. Let $R$ be a logic realization and $B$ a Peano algebra. The fold map is the function $R.Orbit → B.carrier$ defined by $n ↦ (logicNatLift B)(R.orbitEquivLogicNat n)$.
background
ArithmeticOf extracts Peano arithmetic from an abstract law-of-logic realization. A PeanoObject is a structure consisting of a carrier type, a zero element, and a step map; homomorphisms between such objects preserve zero and step. The module shows that once a realization supplies identity and step data, the extracted arithmetic object is the initial Peano algebra generated by that data, with uniqueness up to unique isomorphism.
proof idea
One-line wrapper that applies logicNatLift after the orbit equivalence to LogicNat.
why it matters
The definition is invoked inside realizationLift to produce the homomorphism from the extracted realization Peano algebra to any target PeanoObject. It thereby supports the initiality mechanism that drives Universal Forcing in the module. The parent result is realizationLift, which in turn feeds the extracted arithmetic construction used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.