universal_forcing_map_step
plain-language theorem explainer
Between any two strict logic realizations, the universal forcing map sends successor in the source Peano arithmetic to successor in the target. Canonicity certificates, uniqueness characterizations, and forced-semiring successor laws all cite this intertwining. The proof is a one-line projection of the initial-object lift's built-in map_step field.
Claim. Let $R$ and $S$ be strict logic realizations, and let $x$ lie in the Peano carrier of the arithmetic forced by $R$. Writing $F_{R\to S}$ for the strict universal forcing map, one has $F_{R\to S}(\mathrm{succ}_R(x)) = \mathrm{succ}_S(F_{R\to S}(x))$.
background
In the CanonicalForcing module, each strict logic realization $R$ induces an arithmetic arith R whose Peano structure supplies a carrier, a zero, and a one-step successor. The universal forcing map $F_{R\to S}$ is the unique structure-preserving map obtained by lifting the target Peano algebra along the initiality of the source arithmetic.
Successor here is the Peano step, not a free generator: it is the same one-step extension that appears in the primitive recognition calculus as appending a single distinction act. The companion fact for zero (universal_forcing_map_zero) handles the base case; together they say $F_{R\to S}$ is a Peano homomorphism.
Initiality supplies a lift morphism whose map_step field already records that the lift intertwines successors. The present theorem simply names that field at the universal forcing map.
proof idea
One-line term proof. The universal forcing map is defined as the initial lift of the target Peano structure, (arith R).initial.lift (arith S).peano. Applying that morphism's map_step field at $x$ yields the equality directly. No extra rewriting or induction is required.
why it matters
This is the successor half of the canonicity package for forced arithmetic. The certificate canonicalForcingCert_holds plugs it in as preserves_step, alongside the zero case and uniqueness. The biconditional universal_forcing_iff uses it to prove that any map preserving zero and step equals the universal forcing map, so there is no representational freedom once zero/step data are fixed.
Downstream, forcingFn_succ re-exports the same fact for the forced-semiring presentation, where it seeds the inductive proof that the forcing map preserves addition. In the broader Recognition forcing chain, this locks the discrete arithmetic skeleton that later supports the eight-tick octave (T7) and dimension forcing (T8): successor is uniquely transported between any two strict realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.