forcingFn_bijective
plain-language theorem explainer
Between any two strict logic realizations, the canonical forcing map is a bijection. Cite this when packaging the forced-semiring certificate or arguing that arithmetic structure is uniquely determined rather than chosen. The proof is a one-line extraction of bijectivity from the universal-forcing equivalence.
Claim. For any two strict logic realizations $R$ and $S$, the forcing map $f_{R,S}\colon R\to S$ is bijective (it is the underlying function of the universal-forcing equivalence between $R$ and $S$).
background
In the Universal Forcing layer, a strict logic realization is a concrete carrier that interprets the Law-of-Logic arithmetic: zero-cost identity and a generator step, matching the inductive presentation LogicNat (identity and step, the orbit ${1,\gamma,\gamma^2,\ldots}$).
The forcing map is the unique structure-preserving transport from one such realization to another. Sibling lemmas already record that it preserves zero, successor, addition, multiplication, and one. The present claim isolates the set-theoretic half of that transport: the map is bijective, so the two realizations are equivalent as sets under the forced arithmetic.
Upstream, this rests on the universal-forcing equivalence for strict realizations: that equivalence supplies both the map and the proof that it is bijective, injective and surjective as a package.
proof idea
One-line term proof. Apply the universal-forcing equivalence between the two strict logic realizations and project its bijectivity field. No separate injectivity or surjectivity argument is rebuilt here; both come from that equivalence.
why it matters
This is the bijectivity slot in the forced-semiring certificate. Downstream, forcedSemiringCert_holds assembles map, bijection, zero, one, and add into a single certificate that the arithmetic forced by logic is a semiring uniquely determined up to unique isomorphism.
In the Recognition foundation, that uniqueness is the point: natural-number structure is not an extra axiom but the orbit forced by identity and step. Bijectivity of the forcing map means any two realizations are canonically identified, so later mass-ladder and eight-tick constructions sit on one arithmetic backbone rather than a choice of model. It pairs with the uniqueness-as-semiring-map sibling (any zero-and-step-preserving function equals the forcing map).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.