fold_iso_compat
plain-language theorem explainer
For any two logic realizations R and S, folding the universal-forcing Peano isomorphism R → S down to LogicNat recovers exactly R's own fold. Anyone transporting forced arithmetic (0, 1, +, ×, ≤) along the canonical map cites this. The proof is pure initiality: both composites are Peano homs out of the initial forced arithmetic of R into LogicNat, so uniqueness gives equality pointwise.
Claim. Let $R$ and $S$ be logic realizations (carriers in $\mathrm{Type}\,0$). For every element $x$ of the forced Peano carrier of $R$, $$S.\mathrm{fold}\bigl(\Phi_{R,S}(x)\bigr) = R.\mathrm{fold}(x),$$ where $\Phi_{R,S}$ is the universal-forcing Peano isomorphism $R\xrightarrow{\sim}S$ and each fold is the canonical orbit equivalence from the forced carrier onto the reference initial object $\mathrm{LogicNat}$.
background
This module is Universal Forcing, Part II: the ordered-semiring layer. Part I (CanonicalIso) already upgrades the forcing invariant from a bare carrier bijection to a unique structure-preserving isomorphism of Peano algebras (zero and successor). Here the goal is to show that same map also respects the arithmetic the Peano structure determines: addition, multiplication, order, and the constants 0 and 1.
LogicNat is the reference initial Peano object forced by the Law of Logic: two constructors, identity (zero-cost / multiplicative unit of the orbit) and step (one more iteration of a generator). Every realization $R$ folds its forced Peano carrier onto LogicNat by a canonical orbit equivalence. Arithmetic on forced carriers is defined by transporting the recovered LogicNat operations back along that fold.
The module doc isolates this lemma as the single load-bearing fact: once the two paths $R\to S\to\mathrm{LogicNat}$ and $R\to\mathrm{LogicNat}$ agree, every forced operation (defined via the fold) automatically intertwines with the universal-forcing isomorphism by ordinary Equiv algebra.
proof idea
Term-mode, two steps. First invoke initiality uniqueness on the forced arithmetic of $R$: both
- the composite Peano homomorphism (fold of $S$) ∘ (universal-forcing Peano iso $R\to S$), and
- the fold of $R$
are Peano homs from the initial object (forcedArith R).peano into logicNatPeano. Initiality supplies a unique such hom, so the two homs are equal as functions on the carrier.
Second, apply function congruence at the given element $x$ to obtain the pointwise identity. No arithmetic identities are needed; only the universal property of the initial Peano algebra.
why it matters
This is the hinge of the ordered-semiring layer of universal forcing. All five element-level structure theorems in the same module reduce to it: the iso sends forced zero to forced zero, forced one to forced one, is additive and multiplicative for the forced operations, and is an order isomorphism for forced $\le$. Downstream proofs typically inject along $S$'s fold and rewrite via this compatibility (order even uses a one-line simp only with it).
In the broader Recognition program this closes the gap between "unique Peano isomorphism" and "unique ordered-commutative-semiring isomorphism at the element level," so arithmetic recovered from logic is realization-independent. It does not yet install a Mathlib OrderedCommSemiring instance; that is a separate LogicNat-side enrichment and is not required for the forcing statement. Universes are pinned so forced carriers match LogicNat : Type 0 and initiality typechecks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.