forcingFn_one
plain-language theorem explainer
The universal-forcing map between any two strict Law-of-Logic realizations sends the multiplicative unit to itself. Anyone assembling the forced-semiring certificate cites this as the unit-preservation clause. The proof is a one-line application of the general fact that any zero-and-successor-preserving endomap of the forced carrier fixes 1.
Claim. For any two strict Law-of-Logic realizations $R$ and $S$, the universal-forcing map $f_{R,S}:\mathrm{LogicNat}\to\mathrm{LogicNat}$ satisfies $f_{R,S}(1)=1$.
background
The ForcedSemiring module studies the unique map forced between any two strict realizations of the Law of Logic. A strict realization packages a carrier, a cost type with zero, a comparison map, and a composition operation, using native law data only (no externally supplied orbit).
The forcing map is the underlying function of the universal-forcing equivalence between two such realizations; both forced carriers are definitionally the same inductive type (LogicNat). Sibling results already record that this map sends zero to zero and commutes with successor.
A general lemma on that carrier states that any endomap preserving zero and successor automatically fixes one, since one is definitionally the successor of zero.
proof idea
Term-mode one-liner. Apply the general lemma that a zero-and-successor-preserving map on LogicNat fixes 1, feeding the forcing map together with the already-proved zero-preservation and successor-commutation facts for that map.
why it matters
Supplies the unit field of the forced-semiring certificate: the downstream certificate packages the forcing map with bijectivity, zero, one, and additivity witnesses, and this theorem is the one-witness. Without unit preservation the forced structure cannot be certified as a semiring on the forced carrier. Sits in the Foundation universal-forcing layer that underwrites uniqueness of the arithmetic forced by the Law of Logic, upstream of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.