StrictUniversalForcingIsoCert
plain-language theorem explainer
Packages the strict universal-forcing claim: any two strict Law-of-Logic realizations have a unique structure-preserving Peano-algebra isomorphism between their forced arithmetics. Foundation workers cite it when they need the certificate type rather than the inhabited instance. It is a pure structure definition; the fields are filled by the sibling strict Peano equivalence and uniqueness lemmas.
Claim. A strict universal-forcing isomorphism certificate consists of (i) for every pair of strict Law-of-Logic realizations $R,S$, a Peano-algebra equivalence between the forced arithmetic of $R$ and that of $S$, and (ii) uniqueness: any two such Peano equivalences induce the same underlying carrier map.
background
In the strict Universal Forcing layer, a StrictLogicRealization supplies only native comparison, composition, identity, invariance, and non-triviality data. Its arithmetic is not an input; it is the forced Peano surface derived from that law data. The sibling module Strict/Invariance already gives a bijection between forced arithmetics of any two such realizations.
This module upgrades that bijection to a structure-preserving Peano equivalence, routed through the strict-to-lightweight functor into the ordinary Universal Forcing results (universalForcingPeanoEquiv, peanoEquiv_unique). The canonical arithmetic object for a realization is the initial Peano object: realization-independent content fixed by initiality, with the realization only interpreting it.
The certificate structure records both existence of the canonical Peano iso and uniqueness of the underlying carrier map, so downstream code can demand a single packaged witness rather than two separate lemmas.
proof idea
No proof body: this is a structure declaration. Field iso has type “for all strict realizations $R,S$, a PeanoEquiv between their forced Peano algebras.” Field unique asserts that any two such equivalences agree as functions on carriers.
Inhabitation is deferred to strictUniversalForcingIsoCert, which sets iso to strict_universal_forcing_peanoEquiv and unique to strict_peanoEquiv_unique. Those siblings are the one-line bridges that reuse the non-strict Universal Forcing Peano equivalence and uniqueness via the strict surface.
why it matters
Closes the strict “no escape hatch” story: forced arithmetic is not only bijective across realizations but canonically and uniquely isomorphic as Peano algebras, forced by native law data alone. Downstream, strictUniversalForcingIsoCert is the inhabited instance that packages those two facts for callers.
In the Recognition forcing chain this sits under the foundation layer that makes arithmetic content realization-invariant before constants and geometry (T5–T8) are read off. It is the strict-surface analogue of the ordinary Universal Forcing Peano certificate: same uniqueness-of-structure claim, restricted to realizations that cannot smuggle in an external orbit. Referees checking that “arithmetic is forced, not chosen” point here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.