universal_forcing_map_zero
plain-language theorem explainer
Between any two strict Law-of-Logic realizations, the canonical universal-forcing equivalence sends the forced Peano zero of the source to the forced Peano zero of the target. Anyone citing canonicity of forced arithmetic, the forcing certificate, or the zero clause of the forcing-map characterization needs this fact. The proof is a one-line appeal to the initial-object lift's built-in zero preservation.
Claim. For any two strict Law-of-Logic realizations $R$ and $S$, the canonical universal-forcing equivalence $U_{R,S}$ satisfies $U_{R,S}(0_R)=0_S$, where $0_R$ and $0_S$ are the forced Peano zeros of the arithmetic objects extracted from $R$ and $S$.
background
A strict Law-of-Logic realization supplies only native law data: a carrier, a cost type with zero, a comparison map, and a composition operation. No orbit is handed in. From each such realization one extracts forced arithmetic arith R by passing through the derived lightweight realization; the Peano surface of that arithmetic carries a distinguished zero and a one-step successor.
Universal forcing is the meta-theorem that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects. Concretely, universal_forcing R S is the equivalence of Peano carriers obtained by lifting along the initiality of the source arithmetic into the target Peano structure. That lift is a structure-preserving map, so in particular it is required to send zero to zero.
The local module packages the strict-realization form of this equivalence and records the elementary preservation lemmas (zero and step) needed for the canonicity certificate.
proof idea
One-line term proof. The universal-forcing map is defined as the initial-object lift of the source arithmetic into the target Peano structure. That lift already carries a map_zero field; the proof simply projects it. No extra algebraic work is required beyond the definition of the equivalence.
why it matters
Zero preservation is one of the four fields of the canonicity certificate canonicalForcingCert_holds (existence of the map, preserves zero, preserves step, uniqueness). Downstream, universal_forcing_iff uses it as the left-to-right zero clause in the characterization that a map is the forcing map exactly when it preserves zero and step. The ForcedSemiring layer reuses it as forcingFn_zero, identifying the forced zero with LogicNat.zero under the forcing function.
In the Recognition Science spine this is bookkeeping for the Universal Forcing Meta-Theorem: forced arithmetic is independent of which strict realization one starts from. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live further down the T0–T8 chain. It does close the zero half of the structure-preservation obligation that makes the forced Peano object canonical across realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.