natCost_self
plain-language theorem explainer
The equality cost on natural numbers returns zero for any element compared to itself. Researchers building ordered realizations of universal forcing cite this identity to confirm baseline zero costs in the carrier set. The proof is a direct simplification that unfolds the cost definition.
Claim. For every natural number $n$, the equality cost of $n$ with itself equals zero, where the cost is defined to be zero on equal arguments and one otherwise.
background
The module constructs an ordered faithful realization for universal forcing, using natural numbers as the carrier. The equality cost function on naturals is defined to return zero precisely when its two arguments coincide and one otherwise; this serves as the compare operation inside the LogicRealization structure. The upstream definition supplies the concrete cost that the present identity specializes to the diagonal case.
proof idea
The proof is a one-line wrapper that applies the simplifier tactic using the definition of the equality cost function.
why it matters
This identity is invoked inside the definition of the ordered natural-number realization, which supplies a concrete model for the ordered faithful realization. It guarantees that identical elements incur zero cost, satisfying a basic requirement for any cost function used in the forcing-chain constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.