universalForcingIsoCert
plain-language theorem explainer
Inhabits the universal forcing isomorphism certificate: any two Law-of-Logic realizations have a unique structure-preserving Peano isomorphism between their forced arithmetics. Citation target for the arithmetic-extraction layer of Universal Forcing Part II. The definition wires the canonical Peano equivalence and the uniqueness theorem into the two certificate fields.
Claim. There is a certificate asserting that for every pair of Law-of-Logic realizations $R$ and $S$, the forced Peano algebras of $R$ and $S$ admit a structure-preserving isomorphism (sending zero to zero and commuting with successor), and that any two such isomorphisms agree as functions on the underlying carriers.
background
Universal Forcing extracts a Peano algebra from each Law-of-Logic realization. The earlier spine already yields a bare carrier bijection between the forced arithmetics of any two realizations. A set bijection need not respect zero or successor, so it is weaker than an isomorphism of number systems.
This module upgrades that bijection at the Peano-algebra layer. A Peano equivalence packages an underlying equivalence of carriers together with proofs that it maps zero to zero and commutes with the step map. Canonicality says any two such structure-preserving maps between the same pair of forced arithmetics have identical underlying functions, via uniqueness of the mediating arrow out of an initial object.
The certificate structure records both ingredients, quantified over all realizations in the monomorphic {0,0} universe used throughout the program. The richer ordered-semiring isomorphism (addition, multiplication, order) is explicitly left for later work, since the Peano object here carries only zero and step.
proof idea
Structure inhabitant, not a tactic proof. The iso field is filled by the already-constructed canonical Peano equivalence, which packages the universal-forcing carrier bijection with the zero- and step-preservation lemmas. The unique field is filled by the canonicality theorem, which reduces uniqueness of structure-preserving maps to uniqueness of the mediating homomorphism out of the initial Peano object of the source forced arithmetic. Both fields are lambda-abstracted over pairs of realizations.
why it matters
Closes item 4 of the CanonicalIso module program: the packaged, universally quantified certificate that forced arithmetics are uniquely Peano-isomorphic. That upgrades the Universal Forcing invariant from a bare carrier equivalence to a unique Peano-algebra isomorphism, the arithmetic-extraction layer of Part II.
No downstream consumers are wired yet in the graph; the certificate is the export surface for later exclusivity and framework-comparison arguments that need a single named witness rather than separate iso and uniqueness lemmas. Honest residual gap, stated in the module doc: preservation of ring operations and order is not included, because the underlying Peano object only exposes zero and step. The ordered-semiring iso remains the remaining work toward the full Part II crown. Not itself a T0–T8 forcing step; it sits under the logical-arithmetic spine that feeds those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.