natCost
plain-language theorem explainer
natCost supplies the equality cost on natural numbers, returning zero exactly when the inputs coincide and one otherwise. It is cited by constructions of ordered logic realizations that require a discrete carrier with a simple defect measure. The definition is a direct conditional that distinguishes the equality case from all others.
Claim. The cost function on natural numbers is defined by $c(m,n)=0$ if $m=n$ and $c(m,n)=1$ otherwise.
background
The module OrderedLogicRealization provides an ordered faithful realization for Universal Forcing. Within it, natCost serves as the compare operation for the natural-number carrier in the LogicRealization structure. The cost measures equality defects and is used to instantiate zeroCost, compare, and zero for the realization. No upstream lemmas are required.
proof idea
The definition is given directly by a conditional expression that returns 0 on the equality case and 1 otherwise. It is a one-line wrapper that implements the intended cost without further reduction.
why it matters
natCost is invoked by natOrderedRealization to build the ordered natural-number realization and by the self-cost and symmetry theorems that follow. It supplies the discrete ordered structure needed for the foundation of Universal Forcing, consistent with the forcing chain that begins from ordered logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.