strictCategoricalRealization
plain-language theorem explainer
The definition constructs a StrictLogicRealization by taking the LogicNat inductive type as carrier, equipping it with a Nat-valued cost function and addition as composition. Researchers tracing the categorical foundations of the forcing chain cite it as the canonical strict hook. The construction is a direct field assignment whose only nontrivial proof obligation reduces by simplification against the Peano fact that the identity element differs from every successor.
Claim. The strict categorical realization is the structure whose carrier is the inductive type generated by an identity element and a successor operation, whose cost map sends each element to a natural number via the comparison function, whose composition operation is addition on costs, whose unit is the identity element, whose generator is the successor of the identity, and whose laws hold with the nontriviality condition following from the fact that the identity is not equal to any successor.
background
The Strict/Categorical module supplies a Lawvere-style realization hook whose carrier is the canonical LogicNat NNO surface. LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one further application of the generator), mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. This rests on the Peano axioms derived as theorems from the inductive structure, in particular the result that the identity is distinguishable from any iterate of the generator. Upstream results include the additive compose operation on VirtueEffect, the LogicNat inductive definition itself, the successor function, and the zero-not-successor theorem.
proof idea
The definition populates the StrictLogicRealization structure by setting Carrier to LogicNat, Cost to Nat, compare to logicNatCost, compose to addition, one to LogicNat.zero, generator to LogicNat.succ LogicNat.zero, identity_law to logicNatCost_self, non_contradiction_law to logicNatCost_symm, and the remaining laws to True. The single tactic obligation for nontrivial_law is discharged by simp using logicNatCost together with the zero_ne_succ theorem.
why it matters
This definition supplies the strict categorical realization consumed by the AxiomAudit module's _categorical_ok check and by the sibling equivalence strictCategorical_arith_equiv_logicNat. It occupies the strict domain realization slot inside UniversalForcing.Strict.Categorical, providing the Peano/NNO hook required by the forcing chain. Within Recognition Science it realizes the categorical logic surface that underpins the arithmetic layer of the T0–T8 chain and the subsequent phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.