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 on their Peano carriers. Meta-theorists working on Recognition Science invariance results cite this when establishing that arithmetic is independent of the concrete realization. The definition is a one-line wrapper that applies the equivalence of initial Peano objects.
Claim. For any two realizations $R,S$ of the Law of Logic, the carrier of the forced initial Peano algebra extracted from $R$ is canonically equivalent to the carrier extracted from $S$.
background
A LogicRealization supplies a carrier type, a cost type equipped with zero, a comparison map, a zero element, and the structural propositions required by the forcing program. ArithmeticOf extracts from any such realization a PeanoObject together with a proof that the object is initial. The module presents the first formal statement of the Universal Forcing theorem: any two realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. The upstream lemma equivOfInitial constructs the natural equivalence between any two initial Peano objects by composing their universal lifting maps.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the two realizations.
why it matters
This definition supplies the abstract spine of the Universal Forcing Meta-Theorem. It is invoked directly by the reflexive-closure theorem framework_is_reflexively_closed and the meta-meta-theorem in UniversalForcingSelfReference, and it appears in the admissible-class constructions and the strict-realization variant. The result anchors the claim that forced arithmetic is identical for every Law-of-Logic realization, independent of domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.