universal_forcing
Logic forces one canonical arithmetic across all admissible settings.
plain-language theorem explainer
Any two Law-of-Logic realizations induce canonically equivalent forced arithmetic objects because their extracted Peano algebras are initial. Researchers in Recognition Science cite this to guarantee arithmetic invariance across realizations. The definition is a one-line wrapper that invokes the equivalence of initial Peano objects supplied by the ArithmeticOf construction.
Claim. Let $R$ and $S$ be Law-of-Logic realizations. Then the carrier of the Peano object forced by $R$ is canonically equivalent to the carrier of the Peano object forced by $S$.
background
The module states the first formal version of the Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. A LogicRealization supplies a carrier type, a cost type equipped with zero, a comparison map, and a zero element together with the structural laws required for the forcing program. An ArithmeticOf R is the structure consisting of a PeanoObject together with a proof that it is initial in the category of Peano objects. The upstream lemma equivOfInitial constructs the canonical equivalence between any two initial Peano objects by lifting each through the universal property of the other.
proof idea
The definition is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects extracted from the two realizations.
why it matters
This supplies the abstract spine of the Universal Forcing Meta-Theorem. It is invoked by the admissible-class witnesses for the four canonical domains and by the self-reference theorems that establish reflexive closure of the framework. The meta-meta-theorem records that the equivalence is recovered when the meta-theorem is applied inside the meta-realization. It completes the step in the forcing chain where arithmetic invariance follows from initiality of the forced Peano objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.