foldHom
plain-language theorem explainer
Packages the orbit equivalence of a Law-of-Logic realization onto the reference LogicNat as a Peano-algebra homomorphism from the realization's forced Peano object. Anyone citing the ordered-semiring layer of universal forcing, or the fold-compatibility initiality argument, needs this map. The body is a three-field structure instance: underlying function plus zero and successor preservation from the realization's orbit laws.
Claim. For a Law-of-Logic realization $R$, the orbit equivalence of $R$ onto $\mathrm{LogicNat}$ is a homomorphism of Peano algebras from the forced Peano object of $R$ to the reference Peano object on $\mathrm{LogicNat}$: it sends forced zero to $\mathrm{LogicNat}$ zero and intertwines forced successor with $\mathrm{LogicNat}$ successor.
background
A Peano object is a carrier with a distinguished zero and a step (successor) map. Homomorphisms of Peano algebras are functions that preserve zero and commute with step. The reference object logicNatPeano is LogicNat with its zero and successor; every realization $R$ also determines a forced Peano object via forcedArith R (the arithmetic extracted from $R$'s identity/step data, universes pinned to the carrier).
A LogicRealization supplies a carrier, a comparison cost, an identity element, and a generator/step action, together with the structural laws the Universal Forcing program needs. The invariant target is not the ambient carrier but the arithmetic object extracted from that identity/step data. In particular $R$ carries an orbit equivalence onto LogicNat that already preserves zero and step.
This module is Universal Forcing, Part II: the ordered-semiring layer. CanonicalIso upgraded the forcing invariant to a unique structure-preserving isomorphism of Peano algebras; the present file transports $0,1,+, imes,\le$ along the canonical fold to LogicNat and proves the forcing isomorphism commutes with them.
proof idea
Definitional packaging, not a tactic proof. The underlying map is $R$'s orbit equivalence onto LogicNat. Zero preservation is the realization lemma that the orbit equivalence sends forced zero to LogicNat zero; step preservation is the companion lemma that the orbit equivalence intertwines forced successor with LogicNat successor. Those two fields complete the Peano-homomorphism structure.
why it matters
This is the canonical fold the rest of the ordered-semiring layer is built on. Downstream, a simp lemma records that the homomorphism's underlying function is definitionally the orbit equivalence, and the load-bearing result fold_iso_compat uses the fold: the universal forcing Peano isomorphism $R\simeq S$, followed by $S$'s fold to LogicNat, equals $R$'s fold, because both composites are Peano homs out of the initial forced arithmetic of $R$. Module doc: "pure initiality — both are Peano homomorphisms ... hence identical. Everything else follows by Equiv algebra."
In the broader Recognition Science forcing chain this sits in the foundation layer that extracts unique arithmetic structure before physical constants and the T0–T8 landmarks are read off. It does not itself force $\varphi$, eight-tick, or $D=3$; it supplies the Peano fold those later steps rely on being unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.