logicNatCost_self
plain-language theorem explainer
The theorem confirms that the cost between any element of the logic-forced naturals and itself is zero. Modelers of categorical logic realizations cite it to anchor the zero-cost identity in the orbit structure. The proof is a one-line simplification that unfolds the cost definition directly on equal arguments.
Claim. For every element $a$ of the natural numbers induced by the law of logic, the cost of $a$ with itself equals zero.
background
LogicNat is the inductive type whose identity constructor represents the multiplicative identity in the orbit and whose step constructor iterates the generator, forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. The cost function between two such elements returns zero when they are identical and one otherwise. This theorem belongs to the strict categorical realization module, which supplies a Lawvere-style natural number object hook using the canonical LogicNat surface from the categorical logic realization.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of the cost function, which immediately reduces the equal-argument case to zero.
why it matters
The zero-cost identity is required by the strict categorical realization, which constructs a StrictLogicRealization with LogicNat as carrier and natural numbers as costs. It fills the identity case in the foundation layer of the universal forcing chain, confirming the zero-cost element in the logic-forced naturals before downstream categorical constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.