finCost
plain-language theorem explainer
finCost assigns cost 0 to identical elements of Fin m and cost 1 otherwise. Workers on finite cyclic realizations of logic cite it when constructing periodic carriers that satisfy the Law of Logic without faithful arithmetic embedding. The definition proceeds by a direct case distinction on equality of the two Fin arguments.
Claim. For any natural number $m$ and elements $x,y$ in the finite set with $m$ elements, the cost function returns $0$ when $x=y$ and $1$ otherwise.
background
The module constructs periodic finite-cyclic realizations of Universal Forcing. The carrier is the finite cyclic group Fin (modulus k) while the internal orbit remains the free LogicNat. This shows that not every realization needs to embed arithmetic faithfully into its carrier. finCost supplies the compare operation inside the LogicRealization record.
proof idea
Direct definition by case distinction: return 0 on equality of the Fin arguments and 1 otherwise.
why it matters
finCost is the compare field of modularRealization, the finite cyclic Law-of-Logic realization with periodic interpretation. It therefore participates in the demonstration that Universal Forcing admits carriers that are strictly periodic rather than arithmetically faithful. The construction sits inside the Foundation layer that supports the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.