strictCategorical_arith_equiv_logicNat
plain-language theorem explainer
The definition supplies an equivalence between the Peano carrier extracted from the arithmetic of the strict categorical realization and the LogicNat inductive type. Foundation researchers tracing how logic forces arithmetic would cite it to anchor the canonical NNO surface. The proof is a one-line wrapper that invokes the orbit equivalence produced by converting the realization to its lightweight form.
Claim. Let $R$ be the strict categorical realization with carrier type LogicNat. Then the Peano carrier of the arithmetic derived from $R$ is equivalent to the inductive type LogicNat whose constructors are the zero-cost identity element and the successor step.
background
StrictLogicRealization is the structure that packages a carrier type, a cost type with zero, a compare function, and a compose operation, all drawn only from native law data. The sibling definition strictCategoricalRealization instantiates this structure by setting the carrier to LogicNat, the cost to Nat, and the compare and compose operations to the corresponding logicNatCost and addition. LogicNat itself is the inductive type with constructors identity (the multiplicative identity in the orbit) and step, explicitly constructed to mirror the smallest subset of positive reals closed under multiplication by the generator gamma and containing 1. The module supplies a Lawvere-style categorical hook whose carrier is this canonical LogicNat NNO surface; future refinements may connect it to Mathlib's full category-theory NNO API. The upstream arith operation extracts ArithmeticOf from the lightweight realization obtained via toLightweight, and the doc-comment on arith states that every strict realization has forced arithmetic canonically equivalent to LogicNat.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat field of the lightweight realization produced by StrictLogicRealization.toLightweight on strictCategoricalRealization.
why it matters
This definition closes the loop for the strict categorical case by exhibiting the explicit equivalence between the extracted Peano carrier and LogicNat. It directly supports the upstream claim that every strict realization yields forced arithmetic canonically equivalent to LogicNat. Within the Recognition Science framework it supplies the concrete arithmetic surface required for the forcing chain from logic to natural numbers, preparing the ground for later extraction of Peano axioms and arithmetic operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.