universal_forcing_iff
plain-language theorem explainer
A carrier map between the Peano arithmetic of two strict logic realizations is exactly the universal forcing map if and only if it sends zero to zero and commutes with successor. Anyone citing uniqueness or canonicity of the forced arithmetic morphism needs this biconditional. The proof is a two-line constructor: uniqueness one way, the zero/step lemmas the other.
Claim. Let $R$ and $S$ be strict logic realizations, and let $f$ map the Peano carrier of the arithmetic of $R$ into that of $S$. Then $f$ preserves zero and successor if and only if $f$ equals the underlying function of the universal forcing morphism $R\to S$.
background
In the Universal Forcing / Canonical Forcing layer, each strict logic realization $R$ carries an arithmetic object arith R whose Peano surface supplies a carrier, a zero, and a successor (step). The canonical arithmetic object for a realization is the initial Peano object: "the realization supplies the interpretation; initiality supplies the invariant arithmetic content."
Universal forcing assembles the unique structure morphism between those Peano surfaces. Sibling facts already record that this morphism sends zero to zero and commutes with step, and that any map with those two properties is unique. The present statement packages those facts into a single iff characterization of the forcing map as a function on carriers.
The local setting is foundation-level: no continuum physics, no mass ladder, only the forced arithmetic skeleton that later layers interpret.
proof idea
Term-mode constructor on the biconditional.
Left-to-right: from a pair of hypotheses (zero preservation and pointwise step commutation), apply universal_forcing_unique to conclude $f$ equals the forcing map's underlying function.
Right-to-left: rewrite by reflexivity so $f$ is definitionally the forcing map, then return the pair universal_forcing_map_zero and universal_forcing_map_step.
No induction is replayed here; uniqueness and the two structure lemmas do all the work.
why it matters
This is the complete functional characterization of universal forcing between strict realizations: the forced map is not merely one zero-and-step morphism among many, it is exactly the class of such maps (a singleton). The next sibling, uniqueness of forcing equivalences, rests on the same idea: "The forcing isomorphism is not 'an' iso among many; it is the only structure morphism, hence canonical."
In the Recognition forcing chain this sits under foundation arithmetic initiality, the substrate on which later T5–T8 content (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) is interpreted once realizations are fixed. There are presently no recorded downstream uses, so the lemma is a terminal characterization inside CanonicalForcing rather than a workhorse import.
It closes the "which maps count as forcing" question at the carrier level without residual hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.