forcedSemiringCert_holds
plain-language theorem explainer
Certificate that distinction forces the full arithmetic semiring, not merely a successor tower. Between any two strict Law-of-Logic realizations the canonical forcing map on the free orbit is a unique bijection preserving zero, one, addition, and multiplication. Anyone citing forced arithmetic in Universal Forcing would point here. The body is a pure structure assembly of the already-proved forcing-map lemmas.
Claim. There is a certificate asserting: for any two strict realizations of the Law of Logic, the canonical forcing map $F$ on the free orbit $\mathrm{LogicNat}$ is bijective, satisfies $F(0)=0$, $F(1)=1$, $F(a+b)=F(a)+F(b)$, $F(a\cdot b)=F(a)\cdot F(b)$, and is the unique map that preserves zero and successor. The forced object is canonically the semiring $(\mathbb{N},0,1,+,\times)$.
background
Universal Forcing asks what arithmetic structure is forced once a realization of the Law of Logic is fixed. The free orbit LogicNat is the inductive type with constructors identity (zero-cost unit) and step (one generator iterate); it mirrors the multiplicative orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive set closed under multiplication by the generator and containing 1.
A strict realization uses that same free orbit uniformly as carrier. The arithmetic object of a realization is an initial Peano object; the canonical choice is realization-independent at the surface, with the realization supplying only the interpretation. The certificate structure packages the claim that the canonical map between any two such free orbits is not just a Peano morphism but a full semiring isomorphism, and the unique zero/step-preserving map.
Sibling lemmas already establish that the forcing function preserves zero, one, addition, and multiplication, is bijective, and is unique among zero/step maps. The module note records that under the strict presentation the two carriers coincide, so the map is literally the identity; the non-trivial content sits in the general preservation lemmas and in cross-carrier canonicity proved elsewhere.
proof idea
One-line structure construction. The certificate fields are filled by the sibling lemmas: the map is the forcing function; bijectivity, zero, one, add, mul, and uniqueness are exactly forcingFn_bijective, forcingFn_zero, forcingFn_one, forcingFn_add, forcingFn_mul, and forcingFn_unique. No new reasoning occurs here; it is a packaging def that witnesses the certificate type.
why it matters
In the Recognition foundation stack this is the explicit claim that distinction forces the arithmetic semiring $(\mathbb{N},0,1,+,\times)$, not only a successor tower. That upgrades the Peano/initial-object layer (ArithmeticOf, canonical arithmetic) to ring-level structure needed before cost, measures, and calibration can sit on a forced number system.
The honest module note matters for auditors: on the strict path the forcing map is the identity because every strict realization shares the free orbit carrier. The theory is not thereby trivial; the general zero/step preservation lemmas still apply to arbitrary such maps, and cross-carrier uniqueness lives in CanonicalForcing.ArithmeticOf.forcing_map_unique. No downstream consumers are wired yet (used_by is empty), so this is presently a terminal certificate in the ForcedSemiring module, ready for later Universal Forcing or ArithmeticFromLogic clients that need a single named witness that the forced object is the ordinary semiring of naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.