forcingFn_eq_id
plain-language theorem explainer
For any two strict logic realizations, the canonical universal-forcing map on the shared free arithmetic carrier equals the identity. Anyone citing the forced-semiring certificate uses this to record that the strict presentation collapses carriers definitionally. The proof is a one-line uniqueness argument: the identity preserves zero and successor, so uniqueness forces equality with the forcing map.
Claim. For any two strict logic realizations $R$ and $S$, the canonical universal-forcing map $F_{R,S}:\mathbb{N}\to\mathbb{N}$ between their arithmetic carriers equals the identity function.
background
In Universal Forcing, a strict logic realization packages a free arithmetic orbit whose carrier is definitionally the logic-layer naturals (Peano-style $\mathbb{N}$). The universal-forcing map between two such realizations is therefore a self-map of that carrier: each source orbit element is sent to the matching target element.
The module builds a forced-semiring certificate: for any two strict realizations the forcing map is bijective, preserves $0$, $1$, $+$, and $\times$, and is the unique zero-and-successor-preserving map. The forced object is canonically the semiring $(\mathbb{N},0,1,+,\times)$. An honest module note records that on the strict path the map is literally the identity, because every realization shares the same free carrier.
Upstream, the forcing map is obtained from the strict universal-forcing construction, and a uniqueness lemma characterizes it among zero/step maps. Identity homomorphisms on Peano objects supply the comparison map used here.
proof idea
One-line term proof. Feed the identity on the free carrier into the uniqueness lemma for the forcing map, discharging zero-preservation by reflexivity and successor-preservation by the trivial pointwise identity. Uniqueness gives equality of the forcing map with the identity after taking the symmetric form of that equality.
why it matters
Closes the honesty clause of the forced-semiring story: under strict realizations the carriers coincide, so the canonical map is the identity. That fact is packaged into the forced-semiring certificate (map and uniqueness fields) without overclaiming cross-carrier content, which lives instead in the general canonicity theorem for arithmetic-of objects in CanonicalForcing.
In the Recognition Science foundation layer, distinction forces ordinary Peano arithmetic as a semiring. The identity case is the strict presentation of that forcing, not a collapse of the general theory: preservation lemmas still apply to arbitrary zero/step maps, and non-strict or multi-carrier uniqueness remains nontrivial. No downstream dependents are wired yet; the certificate is the intended consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.