forcingFn_unique
plain-language theorem explainer
Any map on the logic-forced naturals that fixes zero and commutes with successor equals the canonical forcing map between two strict logic realizations. Semiring-homomorphism uniqueness for forced arithmetic cites this. The proof is a one-line appeal to universal forcing uniqueness on strict realizations.
Claim. Let $R$ and $S$ be strict logic realizations. If $f$ is a function on the logic-forced naturals with $f(0)=0$ and $f(n+1)=f(n)+1$ for all $n$, then $f$ equals the canonical forcing map associated to $R$ and $S$.
background
Logic-forced naturals (LogicNat) are the inductive type with constructors identity (zero-cost element) and step (one more generator iteration). Successor is one application of the generator; Peano structure is theorem, not axiom. The orbit picture is ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-reals subset closed under multiplication by $\gamma$ and containing $1$.
This module sits in universal forcing: strict logic realizations carry enough structure that distinction forces arithmetic, not merely a tower. The canonical forcing map between two such realizations is the unique candidate for a zero/step-preserving transport of that arithmetic.
Upstream, canonicity for the LogicNat presentation already supplies uniqueness of zero/step-preserving maps; the present statement restates that uniqueness in the forced-semiring surface language.
proof idea
One-line term wrapper. It applies universal_forcing_unique on the two strict realizations to the given $f$ and the zero/successor hypotheses, yielding equality with the canonical forcing map. No local induction or algebraic expansion is performed here.
why it matters
Closes the uniqueness half of the forced-semiring certificate: distinction forces the arithmetic object $(\mathbb{N},0,1,+,\times)$ canonically, not by choice of map. Downstream, forcedSemiringCert_holds packages bijectivity plus preservation of $0,1,+,\times$ together with this uniqueness; forcingFn_eq_id specializes to $f=\mathrm{id}$ and concludes the forcing map is the identity on logic-forced naturals.
In the Recognition chain this is foundation-level canonicity for arithmetic before constants and geometry (T5–T8). It underwrites the claim that the forced object is Lean's $\mathbb{N}$ as a semiring, so later mass-ladder and calibration work inherit a determined, not selected, carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.