map_preserves_one
plain-language theorem explainer
Any endomap of the logic-forced naturals that fixes zero and commutes with successor also fixes one. Semiring and forcing-map authors cite it when checking that the unit is preserved. The argument is a two-line rewrite: one is successor of zero, so the two hypotheses force the image of one to equal one.
Claim. Let $h$ be a function on the logic-forced natural numbers. If $h(0)=0$ and $h(n+1)=h(n)+1$ for every $n$, then $h(1)=1$.
background
In ArithmeticFromLogic, the carrier LogicNat is the inductive type forced by the Law of Logic: a zero-cost identity constructor and a step constructor that applies the generator once more. Successor is one more application of that generator; the Peano axioms are theorems of the inductive structure, not postulates. The two-constructor shape mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive ray closed under multiplication by the generator and containing the unit.
This module (ForcedSemiring) builds the universal-forcing map between strict logic realizations as a self-map of that forced carrier, and then shows it is a semiring isomorphism. The present lemma is the unit case of structure preservation: any map that already preserves zero and successor automatically preserves the multiplicative unit $1=\mathrm{succ},0$. Upstream, the same carrier appears as the initial Peano object in ArithmeticOf.canonical and as the arithmetic skeleton under calibration and cost-projector forcing.
proof idea
Unfold the goal as preservation of $\mathrm{succ},0$. Rewrite once with the successor-commutation hypothesis, then once with the zero-fixing hypothesis. Both sides become $\mathrm{succ},0$, and the goal closes. No induction and no external lemmas beyond the two hypotheses.
why it matters
The immediate parent is forcingFn_one, which specializes this lemma to the universal-forcing map between two strict realizations: that map already preserves zero and successor, so it preserves one. That fact is one of the structure-preservation legs needed before the forcing map can be certified as a semiring isomorphism (and later as bijective and unique among such maps).
In the broader Recognition stack this sits inside UniversalForcing: arithmetic content is not chosen, it is the initial object forced by logic, and maps between realizations must respect that initiality. Preserving the unit is the multiplicative counterpart of preserving zero, and is required before addition and multiplication preservation can assemble into a full semiring morphism. It does not itself invoke the J-cost, phi, or the T5–T8 forcing chain; those enter only once the arithmetic carrier is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.