forcedZero
plain-language theorem explainer
For any Law-of-Logic realization R, the forced zero is the unique carrier element obtained by transporting 0 from LogicNat along the inverse orbit equivalence. Anyone proving that the universal forcing map preserves arithmetic constants cites this definition. The body is a one-line transport: apply the inverse of R's orbit equivalence to LogicNat's zero.
Claim. Given a Law-of-Logic realization $R$, write $\mathrm{forcedArith}(R)$ for its forced Peano arithmetic. The forced zero of $R$ is the element of the Peano carrier obtained by sending $0 \in \mathrm{LogicNat}$ across the inverse of the orbit equivalence $R \simeq \mathrm{LogicNat}$.
background
This module sits in Universal Forcing Part II: the ordered-semiring layer. 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 canonical map also respects the arithmetic those Peano data determine: addition, multiplication, order, and the constants 0 and 1.
LogicNat is the natural-number object forced by the Law of Logic: an inductive type with constructors identity (zero-cost element) and step (one generator iteration), mirroring the orbit ${1, \gamma, \gamma^2, \ldots}$. A LogicRealization supplies a carrier, comparison cost, identity, and step action; forcedArith packages the ArithmeticOf structure extracted from that data. Every realization folds onto LogicNat via orbitEquivLogicNat; arithmetic is recovered on LogicNat and transported back along that fold.
proof idea
One-line definition. The carrier of forcedArith R is identified with LogicNat through R.orbitEquivLogicNat. The forced zero is simply the inverse image of LogicNat's zero (the identity constructor, written 0) under that equivalence: R.orbitEquivLogicNat.symm 0. No lemmas are applied; the definition is pure transport of the reference zero.
why it matters
This is the constant-0 leg of the ordered-semiring content of universal forcing. Downstream, iso_map_forcedZero proves that the canonical Peano equivalence between any two realizations sends forcedZero R to forcedZero S, by injectivity of S's fold and the fold_iso_compat initiality identity. That preservation clause is packaged into ForcedOrderedSemiringIsoCert, which asserts that forced arithmetics are canonically isomorphic as ordered commutative semirings across all realizations (preserving 0, 1, +, ×, and ≤). Together with the Peano-level UniversalForcingIsoCert, this closes the arithmetic layer of the forcing chain: the initial object determines not only successor structure but the full semiring constants and operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.