logicNatFold
logicNatFold supplies the recursive map sending each element of the logic-forced naturals into the carrier of an arbitrary Peano algebra B. Researchers establishing initiality of the natural-number object or constructing unique homomorphisms out of LogicNat cite this definition. It is realized directly by pattern-matching on the two constructors, routing the identity case to B.zero and the step case through B.step on the recursive image.
claimFor any Peano algebra $B$ with carrier set $|B|$, zero element $0_B$, and successor $s_B$, there is a function $f$ from the logic-forced naturals to $|B|$ satisfying $f(0) = 0_B$ and $f(s(n)) = s_B(f(n))$.
background
PeanoObject is the structure consisting of a carrier type together with a distinguished zero element and a successor map. LogicNat is the inductive type whose constructors are identity (the zero-cost element at the J-cost minimum) and step (one further iteration of the generator), mirroring the smallest subset of the positive reals closed under multiplication by the generator and containing 1. The module extracts arithmetic from an abstract Law-of-Logic realization; once identity and step data are supplied, the forced arithmetic object is the initial Peano algebra generated by that data, with initiality guaranteeing uniqueness up to unique isomorphism.
proof idea
The definition is given by direct pattern matching on the constructors of LogicNat. The identity case returns the zero of the target algebra; the step case applies the target's successor to the image of the predecessor under the same recursive map. No auxiliary lemmas are invoked; the recursion is the standard primitive recursion for the initial algebra.
why it matters in Recognition Science
This definition supplies the recursor used to prove that LogicNat is a Lawvere natural-number object and to construct the unique homomorphism logicNatLift into any other Peano algebra. It realizes the initiality step that converts the Law-of-Logic realization into arithmetic, which is the mechanism behind Universal Forcing. The construction is independent of specific constants such as phi or the J-cost function and sits upstream of the uniqueness and lifting results in the same module.
scope and limits
- Does not prove that the resulting map preserves zero and successor.
- Does not establish uniqueness of the map among all possible functions.
- Does not impose any metric, ordering, or algebraic structure on the carrier beyond the Peano data.
- Does not depend on the value of phi, the J-cost function, or any Recognition Science constants.
Lean usage
def exampleHom (B : PeanoObject) : PeanoObject.Hom logicNatPeano B := { toFun := logicNatFold B, map_zero := rfl, map_step := by intro _; rfl }formal statement (Lean)
90def logicNatFold (B : PeanoObject) : LogicNat → B.carrier
91 | LogicNat.identity => B.zero
92 | LogicNat.step n => B.step (logicNatFold B n)
93
94/-- Lift from `LogicNat` to any Peano object by primitive recursion. -/