forcingFn
plain-language theorem explainer
The universal-forcing map between any two strict Law-of-Logic realizations, written as a self-map of the forced naturals. Downstream work on the forced-semiring certificate and uniqueness of arithmetic structure cites this map. The body is a one-line extraction of the underlying function of the strict universal-forcing equivalence.
Claim. For any two strict Law-of-Logic realizations $R$ and $S$, write $f_{R,S}:\mathbb{N}_{\mathrm{Logic}}\to\mathbb{N}_{\mathrm{Logic}}$ for the underlying function of the canonical equivalence between their forced Peano carriers (both carriers are definitionally the forced naturals).
background
A strict Law-of-Logic realization packages only native law data: a carrier, a cost type with zero, a comparison map, and a composition operation. No orbit is supplied up front. From that data one derives free-orbit arithmetic and a Peano surface.
The forced naturals are the two-constructor inductive type with an identity (zero-cost multiplicative unit of the orbit) and a step (one more iteration of the generator). That structure mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-real subset closed under multiplication by $\gamma$ and containing $1$.
Universal forcing for strict realizations states that any two such realizations have canonically equivalent forced arithmetic objects: the Peano carriers are related by ArithmeticOf.equivOfInitial. Because those carriers are definitionally the forced naturals, the equivalence is a self-map of that type.
proof idea
One-line definition. Apply the strict universal-forcing equivalence to the pair $(R,S)$ and take its underlying function on the forced naturals. No further rewriting or induction is performed at this site.
why it matters
This map is the spine of the ForcedSemiring development. Homomorphism lemmas (preservation of zero, successor, addition, multiplication, and one), bijectivity, and uniqueness as a zero-and-step-preserving map are all stated for it. The forced-semiring certificate assembles those facts into a single package whose map field is exactly this function.
In the broader Recognition foundation, universal forcing is the meta-theorem that every Law-of-Logic realization yields the same forced arithmetic. Presenting the equivalence as an explicit self-map of the forced naturals lets the framework treat Lean's natural numbers as the unique forced semiring, independent of which strict realization one started from. That uniqueness is the arithmetic half of the forcing chain that later pins $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.