iso_map_forcedZero
plain-language theorem explainer
Between any two Law-of-Logic realizations, the canonical Peano isomorphism sends the forced zero of the source to the forced zero of the target. Anyone citing the ordered-semiring layer of universal forcing needs this constant-preservation fact. The proof is a short injectivity argument: both sides fold to the same LogicNat zero via fold-iso compatibility.
Claim. For any two Law-of-Logic realizations $R$ and $S$ (carriers in $\mathrm{Type}\,0$), if $\Phi_{R,S}$ denotes the canonical universal-forcing Peano equivalence $R\to S$, then $\Phi_{R,S}(0_R)=0_S$, where $0_R$ and $0_S$ are the zeros transported from the initial Peano object $\mathrm{LogicNat}$ along each realization's orbit fold.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator action. The Universal Forcing program does not treat the ambient carrier as the invariant; it extracts arithmetic from the identity/step data by folding onto the initial Peano object LogicNat via the orbit equivalence orbitEquivLogicNat.
This module is Part II of that program: after CanonicalIso established a unique structure-preserving Peano isomorphism (zero and successor), the ordered-semiring layer shows the same map respects the arithmetic that Peano structure determines. Forced zero is the image of LogicNat's zero under the inverse of the realization's fold. The load-bearing prior fact is fold-iso compatibility: composing the universal forcing map with $S$'s fold recovers $R$'s fold, by initiality of both as Peano homomorphisms into LogicNat.
proof idea
Term-mode proof in three moves. Apply injectivity of $S$'s orbit equivalence into LogicNat, so it suffices to check equality after folding both sides. Unfold the definition of forced zero on each side, then invoke fold-iso compatibility: the composite of the universal forcing equivalence with $S$'s fold equals $R$'s fold. The remaining identity is Equiv.apply_symm_apply (fold then un-fold is the identity on LogicNat's zero). No induction or case split is needed.
why it matters
This is the zero clause of the ordered-semiring isomorphism certificate. Downstream, forcedOrderedSemiringIsoCert packages it with the matching facts for one, addition, multiplication, and order, inhabiting the full element-level ordered-commutative-semiring content of the canonical map.
In the Recognition Science forcing chain, that certificate is the arithmetic upgrade of the bare Peano uniqueness from Part I: the invariant is not merely a successor algebra but the full arithmetic recovered from initiality. The module deliberately stops short of installing a Mathlib OrderedCommSemiring instance on the carriers; the element-level homomorphism laws are what the forcing statement needs. No open scaffold remains on this lemma itself; it is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.