universal_forcing
plain-language theorem explainer
Any two Law-of-Logic realizations induce canonically equivalent forced arithmetic objects on their Peano carriers. Researchers working within the Recognition Science framework cite this when establishing invariance of arithmetic across distinct realizations. The definition is a one-line wrapper that delegates directly to the equivalence of initial Peano objects.
Claim. Let $R$ and $S$ be Law-of-Logic realizations. The carriers of the Peano objects extracted from the arithmetic structures forced by $R$ and by $S$ are canonically equivalent.
background
A Law-of-Logic realization supplies a carrier type, a cost type equipped with a zero, a comparison map, a zero element, and the structural laws required by the Universal Forcing program. The arithmetic object forced by a realization is the structure containing a Peano object together with a proof that the object is initial. The module states the general Universal Forcing theorem: every Law-of-Logic realization carries canonically equivalent forced arithmetic.
proof idea
This definition is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the two realizations.
why it matters
This definition supplies the core invariance statement of the Universal Forcing Meta-Theorem. It is invoked by the abstract spine in UniversalForcing, by the admissibility witnesses for the four canonical domains, and by the reflexive-closure and meta-meta theorems in UniversalForcingSelfReference. It fills the meta-theorem asserting that the forced arithmetic is independent of the choice of realization and connects to the framework landmark of canonical equivalence of forced arithmetic objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.