finCost_symm
plain-language theorem explainer
Symmetry of the finite equality cost is established for any modulus. Researchers building modular realizations of Universal Forcing cite this to confirm that the compare operation on cyclic carriers is undirected. The proof proceeds by case analysis on whether the two Fin elements coincide, reducing both sides via the definition of finCost.
Claim. Let $m$ be a natural number and let $x,y$ belong to the finite set $Fin(m)$. Define the cost $c(x,y)$ to be $0$ if $x=y$ and $1$ otherwise. Then $c(x,y)=c(y,x)$.
background
The module constructs periodic finite-cyclic realizations for Universal Forcing. The carrier is the finite set $Fin(m)$ and the cost operation is the equality indicator that returns zero on the diagonal and one elsewhere. This demonstrates that the forcing axioms can be realized on strictly periodic carriers without faithful arithmetic embedding into the carrier itself.
proof idea
Case analysis on whether $x$ equals $y$. The equal case substitutes and simplifies directly to zero. The unequal case introduces the symmetric inequality and simplifies both sides to one using the definition of the cost.
why it matters
The lemma is required inside the construction of modularRealization, which packages a finite cyclic carrier together with this cost into a LogicRealization instance. It supports the broader claim that Universal Forcing admits realizations whose carriers are strictly periodic. Within the framework it contributes to showing that the forcing axioms hold on finite cyclic groups without additional arithmetic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.