categorical_arith_equiv_logicNat
plain-language theorem explainer
The categorical realization of universal forcing supplies an equivalence between the carrier of its extracted Peano arithmetic and the natural numbers constructed from the law of logic. Foundation researchers cite this equivalence when confirming that the categorical model reproduces the arithmetic forced by the law of logic. The definition is a direct one-line alias to the orbit equivalence already present in the realization object.
Claim. Let $C$ be the categorical realization. The carrier of the Peano structure inside the arithmetic object extracted from $C$ is equivalent to the inductive type of natural numbers forced by the law of logic.
background
The module re-exports the canonical categorical realization under the universal forcing tree. Logic-forced natural numbers form an inductive type with constructors for the zero-cost identity element and successive generator iterations; this mirrors the multiplicative orbit starting at one and closed under the generator. The arithmetic extraction function produces the arithmetic object from any logic realization, while the categorical instance is the canonical one built on the Peano structure of these natural numbers.
proof idea
This is a one-line wrapper that delegates directly to the orbit equivalence constructed inside the categorical realization.
why it matters
This definition shows that the categorical realization carries the universal forced arithmetic. It supplies a basic consistency link between categorical and logic-based models inside the UniversalForcing layer of the Recognition Science framework. No downstream uses are recorded, so the declaration functions as a foundational bridge rather than a step toward a specific parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.