logicNatCost
plain-language theorem explainer
The definition equips pairs of LogicNat elements with a natural-number cost that is zero precisely when the elements coincide. Categorical logicians constructing Lawvere-style realizations of logic cite it as the compare map inside the StrictLogicRealization record. It is introduced by a direct conditional that branches on equality.
Claim. Let $N$ be the inductive type generated by an identity element and a successor constructor. Define the cost $c:N×N→ℕ$ by $c(x,y)=0$ if $x=y$ and $c(x,y)=1$ otherwise.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator). Its two-constructor structure mirrors the orbit {1, γ, γ², …} inside the positive reals, the smallest subset closed under multiplication by γ and containing 1. The present definition sits inside the module that supplies a strict categorical/Lawvere-style realization hook whose carrier is exactly this LogicNat NNO surface.
proof idea
The definition is introduced by a direct conditional expression that returns 0 on the equality case and 1 on the inequality case.
why it matters
It supplies the compare field of strictCategoricalRealization, which in turn feeds the self and symmetry lemmas for the cost function. The construction advances the strict categorical realization of logic inside the UniversalForcing chain, providing the discrete cost layer required before the eight-tick octave and three-dimensional forcing steps are recovered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.