universal_forcing
plain-language theorem explainer
Universal forcing supplies the canonical equivalence between the Peano carriers forced by any two strict logic realizations. Researchers working on the Recognition Science meta-theorem cite it when restricting to realizations that carry only native comparison, composition, and invariance data. The definition is a one-line wrapper that applies the equivalence of initial Peano objects constructed by ArithmeticOf.
Claim. Let $R$ and $S$ be strict logic realizations. Then the carrier of the Peano object derived from the arithmetic object of $R$ is canonically equivalent to the carrier of the Peano object derived from the arithmetic object of $S$.
background
StrictLogicRealization is a structure that supplies only native law data: a carrier type, a cost type with zero, a comparison map, a composition operation, distinguished elements one and generator, plus the identity law (compare x x = 0) and non-contradiction law (compare x y = compare y x). The module derives the free orbit uniformly as LogicNat rather than allowing an internal orbit field. This setting contrasts with the earlier LogicRealization interface, which permitted an explicit orbit. Upstream, ArithmeticOf builds the forced Peano object from any realization and equivOfInitial supplies the natural equivalence between two initial Peano objects.
proof idea
This is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of R and S.
why it matters
The definition realizes the universal forcing meta-theorem in the strict case and is invoked by the main universal_forcing theorem, the four canonical domains admissibility result, and the reflexive-closure theorems framework_is_reflexively_closed and meta_meta_theorem. It closes the loop in which the meta-theorem itself satisfies the Law-of-Logic shape, confirming that the framework is its own input under the meta-realization. The construction supports the T0-T8 forcing chain by guaranteeing arithmetic invariance across all realizations without supplied orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.