finCost_self
plain-language theorem explainer
The equality cost on a finite carrier returns zero on identical arguments. This reflexivity is invoked when building periodic cyclic realizations of the logic. It is cited in constructions that separate the internal orbit from the carrier interpretation. The proof is a direct simplification using the cost definition.
Claim. For every natural number $m$ and every $x$ in the finite set with $m$ elements, the cost function satisfies $d(x,x)=0$, where $d$ equals zero precisely when its arguments coincide.
background
The module supplies a periodic finite-cyclic realization of Universal Forcing in which the internal orbit remains free while the carrier interpretation is periodic. The cost function is defined by the rule that returns zero exactly when the two Fin m arguments are equal and one otherwise. This supplies a discrete equality metric on the cyclic carrier. The present theorem records the reflexivity of that metric and is the sole dependency of the modularRealization construction.
proof idea
One-line wrapper that applies the simp tactic to the definition of the cost function, which immediately yields zero on identical arguments.
why it matters
The lemma is used inside the definition of modularRealization, the finite cyclic Law-of-Logic realization with periodic interpretation. It thereby supports the module claim that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier. The result sits inside the foundation layer that prepares finite models for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.