strict_peanoEquiv_unique
plain-language theorem explainer
Any two Peano-algebra isomorphisms between the forced arithmetics of strict Law-of-Logic realizations induce the same carrier map. Researchers citing uniqueness of the strict universal-forcing isomorphism use this. The proof is a one-line reduction to the lightweight uniqueness lemma via the strict-to-lightweight forgetful map.
Claim. Let $R$ and $S$ be strict Law-of-Logic realizations, and let $e_1,e_2$ be structure-preserving isomorphisms of Peano algebras between the forced arithmetics of $R$ and $S$. Then the underlying functions $e_1$ and $e_2$ on carriers coincide: $e_1 = e_2$ as maps of sets.
background
A strict logic realization supplies only native comparison, composition, identity, invariance, and non-triviality data. Its arithmetic is not handed in by the caller; it is the forced initial Peano object derived from that law data. The sibling module already builds a bijection between forced arithmetics of any two such realizations.
This module upgrades that bijection to a structure-preserving Peano isomorphism and proves it is unique. The upgrade reuses the non-strict (lightweight) universal-forcing Peano equivalence and its uniqueness theorem, transported along the forgetful map from strict realizations to lightweight ones.
Upstream, the canonical arithmetic object for a realization is the initial Peano algebra (realization-independent at the surface; the realization only interprets). Uniqueness of Peano equivalences in the lightweight setting is the lemma this statement reduces to.
proof idea
One-line term wrapper. Apply the lightweight uniqueness lemma peanoEquiv_unique to the images of $R$ and $S$ under the strict-to-lightweight forgetful map, with the same two Peano equivalences $e_1$ and $e_2$. No new algebraic work is done on the strict surface; uniqueness is inherited from the lightweight theory.
why it matters
Closes the uniqueness half of the strict universal-forcing isomorphism certificate. Downstream, strictUniversalForcingIsoCert packages the canonical Peano iso together with this uniqueness fact: the certificate is inhabited exactly by the strict canonical iso and the statement that any two such isos agree on carriers.
In the Recognition foundation, this is the "no escape hatch" surface: arithmetic content is forced by native law data alone, and the structure-preserving comparison between any two strict realizations is not only existent but unique. That uniqueness is what makes the forced arithmetic genuinely canonical rather than one orbit among many. It sits under the broader universal-forcing chain that later feeds dimension, octave, and cost uniqueness (T5–T8 landmarks), though this lemma itself is purely about Peano-algebra uniqueness on the strict surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.