natCost_symm
plain-language theorem explainer
Symmetry of the natural-number equality cost is established for the ordered realization of universal forcing. Researchers constructing concrete models for forcing logic cite this to guarantee the compare operation is invariant under argument swap. The proof splits on whether the inputs coincide, substitutes in the equal case, and simplifies both branches with the cost definition.
Claim. For all natural numbers $m,n$, the equality cost of $m$ and $n$ equals the equality cost of $n$ and $m$, where the cost equals zero precisely when the numbers are identical and equals one otherwise.
background
The module supplies an ordered faithful realization for universal forcing. Its central definition is the equality cost on natural numbers: zero when the arguments coincide and one otherwise. This cost serves as the compare field inside the LogicRealization record whose carrier is Nat.
proof idea
The tactic proof opens with by_cases on m = n. The equal branch substitutes and reduces both sides to zero via the cost definition. The unequal branch records the symmetric inequality and again simplifies both sides to one.
why it matters
The result feeds the definition of the ordered natural-number realization, which supplies a concrete carrier and cost for the forcing framework. It confirms the symmetry property required for the realization to be faithful under the ordered logic setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.