strictCategoricalRealization
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not implement the full Mathlib category-theory NNO API.
- Does not derive arithmetic operations beyond the basic Peano structure and cost comparison.
- Does not address non-strict or probabilistic realizations.
- Does not compute explicit costs for concrete LogicNat elements beyond the identity and symmetry laws.
Lean usage
def audit_check : (StrictLogicRealization.arith strictCategoricalRealization).peano.carrier ≃ LogicNat := strictCategorical_arith_equiv_logicNatformal statement (Lean)
34def strictCategoricalRealization : StrictLogicRealization where
35 Carrier := LogicNat
proof body
Definition body.
36 Cost := Nat
37 zeroCost := inferInstance
38 compare := logicNatCost
39 compose := fun a b => a + b
40 one := LogicNat.zero
41 generator := LogicNat.succ LogicNat.zero
42 identity_law := logicNatCost_self
43 non_contradiction_law := logicNatCost_symm
44 excluded_middle_law := True
45 composition_law := True
46 invariance_law := True
47 nontrivial_law := by
48 simp [logicNatCost, LogicNat.zero_ne_succ]
49