equivOfInitial
plain-language theorem explainer
The definition constructs the canonical isomorphism between the carriers of initial Peano objects from any two Law-of-Logic realizations. Researchers establishing universal forcing or arithmetic invariance across realizations cite this equivalence. Construction defines forward and inverse maps via lifting each initial object into the other and invokes uniqueness of initial morphisms to confirm mutual inverses.
Claim. Let $R$ and $S$ be Law-of-Logic realizations. Let $A$ be the arithmetic object forced by $R$ and $B$ the arithmetic object forced by $S$. Then the carriers of their initial Peano objects are canonically equivalent.
background
ArithmeticOf is the structure that packages a PeanoObject together with a proof that it is initial in the category of Peano objects. The module extracts arithmetic from an abstract Law-of-Logic realization by taking the initial Peano algebra generated by the realization's identity and step data. Initial objects are unique up to unique isomorphism; this supplies the invariant arithmetic content across realizations.
proof idea
The definition supplies the forward map as the lift of the initial morphism from the first Peano object into the second. The inverse map is the symmetric lift in the opposite direction. Left and right inverses are established by composing the two lifts and applying the uniqueness property of initial morphisms to recover the identity on each Peano object.
why it matters
This definition supplies the equivalence used by the arithmetic_invariant theorem in UniversalForcing, which states that the forced arithmetic of every realization is canonically equivalent. It also feeds the specific invariants for categorical, boolean, modular, ordered, and physics realizations. The construction realizes the initiality mechanism behind Universal Forcing, ensuring that arithmetic content is independent of the particular Law-of-Logic realization chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.