arithmetic_invariant
plain-language theorem explainer
Any two Law-of-Logic realizations induce canonically equivalent arithmetic structures through their Peano carriers. Researchers tracing the forcing chain from logic to number systems cite this when establishing uniqueness of arithmetic across realizations. The definition is a direct one-line wrapper invoking the canonical equivalence between initial Peano algebras.
Claim. Let $R$ and $S$ be realizations of the Law of Logic. The carrier sets of the Peano objects inside the arithmetic structures forced by $R$ and $S$ are canonically equivalent: the Peano carrier of the arithmetic object of $R$ is equivalent to the Peano carrier of the arithmetic object of $S$.
background
The module states the first formal version of the Universal Forcing theorem: any two Law-of-Logic realizations possess canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. A LogicRealization supplies the structure from which ArithmeticOf extracts a PeanoObject together with a proof that the object is initial. The upstream ArithmeticOf.equivOfInitial supplies the natural equivalence between any two such initial Peano objects, constructed by lifting each initial algebra to the other.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the two realizations.
why it matters
This supplies the simplest spine of the Universal Forcing theorem, showing arithmetic invariance before later modules enrich the interpretation map from each carrier. It closes the initial segment of the forcing chain by guaranteeing that every realization yields the same Peano algebra up to unique isomorphism, consistent with the uniqueness properties required for the subsequent introduction of the phi-ladder and physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.