biologyCost_self
plain-language theorem explainer
The biology cost function returns zero on identical generations. Researchers constructing the biological realization of the universal forcing would cite this to confirm the zero element in the LogicRealization structure. The proof is a one-line simplification that unfolds the definition of biologyCost.
Claim. For any generation $a$, the cost function satisfies $c(a,a)=0$, where $c(a,b)=0$ if $a=b$ and $c(a,b)=1$ otherwise.
background
In the BiologyRealization module the carrier is the type of generations realized as natural numbers, with the reproductive step serving as generator. The cost is defined directly as the indicator of inequality: biologyCost(a,b) equals 0 precisely when a equals b and 1 otherwise. This supplies the compare operation and zero element for the subsequent LogicRealization construction. Upstream, the Generation abbreviation appears in SpectralEmergence as Fin 3, consistent with the three-generation structure used in CKM and ThreeGenerations.
proof idea
One-line wrapper that applies the simp tactic to the definition of biologyCost, which reduces the equality by case analysis on the if-condition.
why it matters
The lemma supplies the zero-cost axiom required by biologyRealization, which builds the LogicRealization instance with Carrier := Generation, Cost := Nat, compare := biologyCost and zero := 0. It therefore closes the zero element for the biological realization inside the UniversalForcing layer, linking the generation-count carrier to the broader forcing-chain construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.