finCost
plain-language theorem explainer
Equality cost on a finite carrier returns zero precisely when its two arguments coincide and one otherwise. Researchers constructing periodic realizations of the universal forcing chain cite this function when defining the compare operation on Fin m. The definition proceeds by direct case distinction on equality.
Claim. For natural number $m$ and elements $x,y$ in the finite set Fin $m$, the cost is $c(x,y)=0$ if $x=y$ and $c(x,y)=1$ otherwise.
background
The ModularLogicRealization module constructs periodic finite-cyclic realizations for Universal Forcing. The internal orbit remains free (LogicNat) while the carrier interpretation is periodic. This demonstrates that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.
proof idea
The definition is a direct conditional that returns 0 on equality of the two Fin arguments and 1 otherwise.
why it matters
The definition supplies the compare field for modularRealization, the finite cyclic Law-of-Logic realization with periodic interpretation. It supports the claim that realizations of the forcing chain can use periodic carriers without faithful arithmetic embedding, consistent with the flexibility required by J-uniqueness and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.