foldHom_toFun
plain-language theorem explainer
The fold homomorphism from a realization's forced Peano arithmetic into LogicNat has underlying map definitionally equal to that realization's orbit equivalence onto LogicNat. Anyone rewriting along foldHom, or transporting 0/1/+/×/≤ via the fold, cites this simp fact. The proof is pure definitional equality (rfl).
Claim. Let $R$ be a Law-of-Logic realization (carrier pinned to $\mathrm{Type}\,0$). For every element $x$ of the Peano carrier of the forced arithmetic of $R$, the underlying function of the fold homomorphism $\mathrm{foldHom}(R)$ equals the orbit equivalence of $R$ onto $\mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the canonical map from a bare Peano-algebra iso to a map that also respects the arithmetic Peano determines: $0$, $1$, $+$, $\times$, and $\le$. The module works by folding every forced carrier onto the reference initial object $\mathrm{LogicNat}$ and transporting structure along that fold.
A $\mathrm{LogicRealization}$ supplies a carrier, a comparison cost, an identity element, and a step/generator action. From that data one extracts forced Peano arithmetic (forcedArith). $\mathrm{LogicNat}$ is the two-constructor inductive forced by the Law of Logic (identity / step), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$; it already carries recovered $+$ and $\times$ from ArithmeticFromLogic.
The fold $R.\mathrm{orbitEquivLogicNat}$ is the canonical Peano homomorphism from the forced carrier of $R$ into $\mathrm{LogicNat}$. The structure foldHom R packages that fold as a homomorphism; this lemma names its underlying function.
proof idea
Term-mode one-liner: rfl. By construction, (foldHom R).toFun is defined to be R.orbitEquivLogicNat, so the equality holds definitionally and is marked @[simp] for downstream rewriting.
why it matters
This is the definitional hinge between the packaged fold homomorphism and the orbit equivalence used throughout CanonicalSemiringIso. The module's load-bearing lemma is fold compatibility (pure initiality): the universal forcing iso $R\simeq S$, followed by $S$'s fold onto $\mathrm{LogicNat}$, equals $R$'s fold; both are Peano homs out of the initial forced arithmetic of $R$. Exposing toFun as the orbit map lets every later transport of $0$, $1$, $+$, $\times$, and $\le$ (the sibling iso_map_forced* and forced* facts) reduce by simp to statements about orbitEquivLogicNat.
In the Recognition forcing chain this sits in the foundation layer that extracts arithmetic from logic before cost uniqueness (T5 J-cost) and the phi fixed point (T6). No downstream edges are recorded yet; the lemma is infrastructure for the ordered-semiring content of the canonical iso, not a physics endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.