arith_universal_initial
Any Law-of-Logic realization R induces a canonical equivalence between its extracted Peano arithmetic carrier and the reference LogicNat object. This serves as the base case for the Universal Forcing theorem, showing that forced arithmetic is initial and independent of the concrete realization. Researchers formalizing the Recognition Science foundation would cite it when establishing that all realizations yield isomorphic arithmetic structures. The definition is a direct one-line wrapper exposing the orbit equivalence already present in the Log
claimFor any Law-of-Logic realization $R$, the Peano carrier extracted from the arithmetic structure of $R$ is canonically equivalent to the reference natural numbers $LogicNat$ forced by the Law of Logic: $(arithmeticOf R).peano.carrier ≃ LogicNat$.
background
LogicRealization is a structure supplying a carrier set, a comparison cost, zero-cost element, identity, and step action, along with the structural laws required for forcing arithmetic. The reference LogicNat is the inductive type generated by an identity element and a successor step, representing the orbit under multiplication by the generator in the positive reals. The module states the first formal version of the Universal Forcing theorem, asserting that any two such realizations produce canonically equivalent forced arithmetic objects because they are initial Peano algebras. Upstream, the ArithmeticFromLogic module defines LogicNat as the smallest subset closed under the generator action.
proof idea
The definition is a one-line wrapper that directly returns the orbit equivalence supplied by the realization R.
why it matters in Recognition Science
This definition provides the simplest form of the Universal Forcing theorem, establishing that the forced arithmetic is independent of the specific realization. It supports the meta-theorem that any two Law-of-Logic realizations have canonically equivalent arithmetic objects, as they are both initial Peano algebras. In the Recognition Science framework, this aligns with the forcing chain where the arithmetic structure emerges canonically from the Law of Logic.
scope and limits
- Does not establish the equivalence for structures outside the LogicRealization interface.
- Does not provide explicit constructions of the equivalence beyond the orbit map.
- Does not address computational aspects or decidability of the equivalence.
formal statement (Lean)
36noncomputable def arith_universal_initial (R : LogicRealization) :
37 (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
proof body
Definition body.
38 R.orbitEquivLogicNat
39
40/-- **Universal Forcing Meta-Theorem, abstract spine.**
41
42Any two Law-of-Logic realizations have canonically equivalent forced
43arithmetic objects. -/