arith_universal_initial
plain-language theorem explainer
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
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.