canonicalCategoricalRealization
plain-language theorem explainer
The definition supplies the canonical LogicRealization whose carrier is the inductive type LogicNat, serving as the natural numbers object for categorical realizations. Researchers on the Universal Forcing program cite it to establish that arithmetic remains invariant across realizations. The body is a direct structure definition that populates every required field by referencing the constructors and theorems already established for LogicNat.
Claim. The canonical categorical realization is the structure LogicRealization with carrier the inductive type LogicNat (generated by the identity constructor and the step constructor), cost set the natural numbers, zero element the identity, successor the step constructor, interpretation the identity map on LogicNat, and all required invariants (zero-cost comparison, orbit equivalence, non-contradiction, excluded middle, composition, action invariance, nontriviality) satisfied by the inductive structure and the pre-proved Peano theorems.
background
In the Recognition Science setting the LogicRealization structure packages a carrier set together with cost, zero, step, orbit, interpretation, and logical invariants so that logical operations are realized in the style of a Lawvere natural numbers object. The module CategoricalLogicRealization supplies a direct hook for the Universal Forcing program, using the same initial Peano algebra language already developed in ArithmeticFromLogic rather than rebuilding category theory from scratch.
proof idea
The definition is a direct structure construction. Carrier, Cost, zero, step, Orbit, interpret, and the orbit equivalence are assigned by direct reference to LogicNat and its constructors. The Peano axioms are discharged by rfl for the trivial cases and by the upstream theorems zero_ne_succ, succ_injective, and LogicNat.induction for the non-trivial cases; the remaining logical invariants are filled with True or short by_cases arguments.
why it matters
This definition supplies the canonical NNO-based realization that is used by categorical_arithmetic_invariant to prove that the arithmetic extracted from any realization is equivalent to the arithmetic extracted from the canonical one via equivOfInitial. It is also the body of categoricalRealization in the UniversalForcing module. Within the framework it realizes the natural numbers object required for the forcing chain, ensuring that the Peano arithmetic forced from logic is uniform across all realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.