biologyCost
plain-language theorem explainer
A cost function on generations returns zero for matching inputs and one for differing ones. Researchers in the Recognition framework cite it when constructing the biological logic realization. The implementation uses a direct conditional based on input equality.
Claim. Let $G$ be the type of generations realized as natural numbers. Define the cost function $c : G × G → ℕ$ by $c(a,b) = 0$ if $a = b$ and $c(a,b) = 1$ otherwise.
background
In this module generations act as the carrier for a lightweight biological realization, with the reproductive step serving as generator. The type is realized directly as natural numbers. Upstream, generations appear as Fin 3 in SpectralEmergence to match the cube dimension, as inductive types in CKM and ThreeGenerations that encode parity patterns across dimensions, and in RSLedger as the three fermion generations with canonical torsion from Q₃ cube geometry.
proof idea
The definition is a direct conditional that returns zero on equality of the two generation inputs and one otherwise. No external lemmas are required beyond the decidable equality on natural numbers.
why it matters
This cost function supplies the compare operation for the biological realization, which assembles a LogicRealization structure with generations as carrier and natural numbers as cost. It extends the forcing chain to a biological interpretation by treating generational mismatch as unit cost. Downstream results establish zero self-cost and symmetry of the function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.