UniversalForcingIsoCert
plain-language theorem explainer
Packages the claim that any two Law-of-Logic realizations have a unique structure-preserving isomorphism between their forced Peano arithmetics. Anyone citing the Universal Forcing arithmetic-extraction layer uses this certificate as the packaged invariant. It is a two-field definition bundling existence of the canonical Peano equivalence with uniqueness of the underlying carrier map; no proof body, only the certificate shape.
Claim. A Universal Forcing isomorphism certificate consists of two data: (i) for every pair of Law-of-Logic realizations $R,S$, a Peano-algebra isomorphism between the forced arithmetic of $R$ and that of $S$ (an equivalence of carriers sending zero to zero and commuting with successor); (ii) uniqueness: any two such Peano-algebra isomorphisms between the same pair induce the same underlying function on carriers.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator action, together with the structural laws the Universal Forcing program needs. The invariant target is not the ambient carrier; it is the arithmetic object extracted from the identity/step data. The canonical arithmetic of a realization is the initial Peano object (zero and successor only at this layer).
The parent Universal Forcing spine already yields a bare carrier bijection between the forced arithmetics of any two realizations. A bare bijection need not respect zero or successor. This module upgrades that bijection to a Peano-algebra isomorphism: a bundled equivalence of carriers that sends zero to zero and commutes with the step map.
The local setting is universe-monomorphic at {0,0}, so all Peano carriers live in Type 0. The certificate structure records both existence of such an isomorphism for every pair of realizations and uniqueness of the underlying carrier function among all structure-preserving isomorphisms.
proof idea
Definition only: a two-field certificate structure with empty proof body. The first field is a universally quantified Peano-algebra isomorphism between forced arithmetics of any two realizations. The second field asserts that any two such isomorphisms induce equal underlying carrier maps. Inhabitation is separate: the companion definition fills the fields with the canonical forcing Peano equivalence and the uniqueness lemma for structure-preserving maps between forced arithmetics.
why it matters
This is the packaged crown of Universal Forcing Part II at the Peano-algebra layer. The module doc states the upgrade explicitly: from bare carrier equivalence to unique Peano-algebra isomorphism ("the isomorphism is not merely some isomorphism, it is the unique one"). Downstream, the inhabited certificate supplies the canonical iso used by the order-preservation theorem in the ordered-semiring layer (the forced order is preserved and reflected along the canonical map). The next open step, flagged in the module doc, is preservation of ring operations $+$ and $\times$ and the order $\le$; PeanoObject carries only zero and step, so the richer ordered-semiring iso remains future work toward the full Part II crown. Framework-wise this sits in the arithmetic-extraction half of Universal Forcing, not in the T0–T8 forcing chain itself, but it is the uniqueness spine that makes forced arithmetic realization-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.