arith_equiv_logicNat
Every strict realization of the law of logic yields forced arithmetic whose Peano carrier is canonically equivalent to the natural numbers forced by the law of logic. Workers on the universal forcing theorem cite this equivalence when extracting concrete arithmetic from abstract realizations that carry no internal orbit. The definition is a one-line wrapper delegating to the orbit equivalence already proved for the lightweight realization derived from the strict data.
claimFor any strict logic realization $R$, the Peano carrier of the arithmetic extracted from $R$ is equivalent to the natural numbers forced by the law of logic.
background
StrictLogicRealization is a structure that supplies only native comparison, composition, identity, and non-contradiction data on a carrier type together with a cost type, without an internal orbit field. LogicNat is the inductive type with constructors identity (the zero-cost element) and step (iteration of the generator), representing the smallest subset of positive reals closed under multiplication by the generator and containing the identity. The module StrictRealization derives the free orbit uniformly as LogicNat once the lightweight realization is obtained via toLightweight, in contrast to the earlier LogicRealization interface that permitted an internal orbit as a field. Upstream, arith extracts the arithmetic structure from that lightweight realization.
proof idea
The definition is a one-line wrapper that applies the orbit equivalence already established for the lightweight realization of R.
why it matters in Recognition Science
This equivalence closes the strict realization path inside the universal forcing construction, guaranteeing that arithmetic is forced to coincide with the natural numbers generated by the law of logic without any supplied orbit. It supports the derivation of Peano arithmetic in the foundation layer and aligns with the forcing chain steps that produce the self-similar fixed point and the eight-tick octave structure. The result removes the escape hatch noted in the module documentation and thereby strengthens the claim that every strict realization yields the same forced arithmetic.
scope and limits
- Does not construct the equivalence map explicitly.
- Does not verify that the equivalence preserves addition or multiplication.
- Does not apply to realizations that supply an internal orbit.
- Does not address non-strict or meta-realizations.
formal statement (Lean)
100def arith_equiv_logicNat (R : StrictLogicRealization) :
101 (arith R).peano.carrier ≃ LogicNat :=
proof body
Definition body.
102 (toLightweight R).orbitEquivLogicNat
103
104/-- Universal forcing for strict realizations. -/