strictUniversalForcingIsoCert
plain-language theorem explainer
Packages the strict canonical Peano isomorphism and its uniqueness into one inhabited certificate. Cite it when asserting that any two strict Law-of-Logic realizations have a unique structure-preserving arithmetic isomorphism forced by native law data alone. The body simply wires the existing iso constructor and uniqueness theorem into the certificate fields.
Claim. There is an inhabited certificate asserting: for any two strict Law-of-Logic realizations $R$ and $S$, there exists a canonical Peano-algebra isomorphism between their forced arithmetics, and any two structure-preserving isomorphisms between those arithmetics agree as functions on the carrier.
background
A strict Law-of-Logic realization supplies only native comparison, composition, identity, invariance, and non-triviality data. Its arithmetic is derived, not handed in by the caller. The forced arithmetic carries a Peano algebra structure (zero and successor on a carrier).
Strict/Invariance already gives a bijection between the forced arithmetics of any two strict realizations. This module upgrades that bijection, via the strict-to-lightweight functor, to a structure-preserving Peano isomorphism: zero maps to zero and the map commutes with successor. Uniqueness says any two such Peano equivalences have the same underlying function.
The certificate structure bundles those two facts: a family of canonical isomorphisms indexed by pairs of strict realizations, plus a uniqueness clause for structure-preserving maps between their forced Peano algebras.
proof idea
Definitional inhabitant of the certificate structure. The iso field is filled by the strict structure-preserving Peano equivalence (itself a thin wrapper that applies the lightweight universal-forcing Peano equivalence after the strict-to-lightweight forgetful map). The unique field is filled by the strict canonicality theorem, which equates the underlying functions of any two Peano equivalences between the same pair of forced arithmetics. No extra proof work beyond wiring those two results.
why it matters
Closes the strict "no escape hatch" surface of Universal Forcing: arithmetic is not an input orbit but a derived object, and the comparison map between any two such derived arithmetics is a unique Peano isomorphism. That is the structure-preserving form of the claim that the Law of Logic forces a single arithmetic up to unique isomorphism once only native law data is allowed.
Downstream consumers of exclusivity or framework-equivalence arguments can treat this certificate as the packaged witness that strict realizations cannot disagree on arithmetic structure. It sits under the broader Universal Forcing chain that feeds the Recognition Science forcing ladder (unique cost, self-similar scale, discrete octave), by locking the arithmetic substrate before physical constants are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.