strictBoolean_arith_equiv_logicNat
The strict discrete Boolean realization forces arithmetic canonically equivalent to LogicNat, the free iteration object generated by an identity element and successor steps. Researchers tracing invariance across realizations in the universal forcing framework would cite this result. The definition is a one-line wrapper that applies the orbit equivalence extracted from the lightweight version of the realization.
claimLet $R$ be the strict discrete Boolean realization with carrier type Bool, cost type Nat, comparison given by boolCost, and composition given by xorBool. The Peano carrier of the arithmetic extracted from $R$ is equivalent to LogicNat, the inductive type with constructors for the identity element and a successor operation.
background
A StrictLogicRealization consists of a carrier type, a cost type equipped with zero, a comparison map from pairs of carriers to costs, and a binary composition operation on carriers. The strictBooleanRealization instantiates this structure with Bool as carrier, Nat as cost, boolCost for comparison, and xorBool for composition. LogicNat is the inductive type whose constructors identity and step generate the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity. The arith operation extracts forced arithmetic from the lightweight realization obtained by toLightweight. The module setting notes that while the Boolean carrier orbit is periodic, the forced arithmetic is the free iteration object derived from the native generator.
proof idea
This is a one-line wrapper that applies the orbitEquivLogicNat equivalence from the lightweight realization of strictBooleanRealization.
why it matters in Recognition Science
This definition supplies the first strict cross-realization invariance theorem, confirming that positive-ratio and Boolean realizations force identical arithmetic. It supports the forcing chain by establishing that the arithmetic structure is independent of the choice of strict realization. The result sits between the definition of StrictLogicRealization and the extraction of arith, reinforcing that the logic-forced natural numbers arise uniformly before the transition to spatial dimensions and constants in the Recognition Science framework.
scope and limits
- Does not claim that the Boolean carrier itself coincides with LogicNat.
- Does not address non-strict or continuous realizations.
- Does not compute explicit mappings or cost values under the equivalence.
- Does not extend the invariance statement beyond the strict Boolean case.
formal statement (Lean)
53def strictBoolean_arith_equiv_logicNat :
54 (StrictLogicRealization.arith strictBooleanRealization).peano.carrier
55 ≃ ArithmeticFromLogic.LogicNat :=
proof body
Definition body.
56 (StrictLogicRealization.toLightweight strictBooleanRealization).orbitEquivLogicNat
57
58/-- First strict cross-realization invariance theorem:
59positive ratios and Boolean propositions force the same arithmetic. -/