_categorical_ok
plain-language theorem explainer
The definition shows that arithmetic extracted from the strict categorical realization has carrier equivalent to the inductive LogicNat type. Foundation researchers in Recognition Science cite it when confirming that domain-specific strict realizations recover the forced natural numbers. It is realized as a direct one-line application of the orbit equivalence from the lightweight conversion of the realization.
Claim. Let $R$ be the strict categorical realization with carrier the inductive type generated by an identity element and successor. The Peano arithmetic structure derived from the lightweight form of $R$ has carrier type equivalent to this inductive type.
background
The module supplies an audit surface for strict, domain-rich realizations completing the Universal Forcing pass. A StrictLogicRealization is a structure consisting of a carrier type, a cost type equipped with zero, a comparison map, and a composition operation, all required to use only native law data. The strictCategoricalRealization specializes this structure by setting the carrier to LogicNat, the inductive type whose constructors identity and step mirror the orbit of positive reals closed under multiplication by the generator and containing the unit element.
proof idea
The definition is a one-line wrapper that applies the orbit equivalence to LogicNat obtained from the toLightweight conversion of the strict categorical realization.
why it matters
This definition completes the categorical audit entry in the strict Universal Forcing pass, confirming that the extracted arithmetic matches the Law-of-Logic natural numbers. It directly supports the canonical equivalence stated in the arith documentation for every strict realization. The result sits inside the foundation layer that feeds the forcing chain from T0 through the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.