universal_forcing
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish admissibility of any concrete realization.
- Does not supply explicit carriers or numerical spectra.
- Does not address the continuous positive-ratio arithmetic invariant separately.
- Does not prove uniqueness of the equivalence beyond the initiality property.
formal statement (Lean)
44noncomputable def universal_forcing (R S : LogicRealization) :
45 (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
proof body
Definition body.
46 ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
47
48/-- The continuous positive-ratio realization has the same forced arithmetic
49as every other realization. -/