lineageCost
plain-language theorem explainer
The lineage cost function on pairs of lineage states returns zero precisely when the states are identical and one otherwise. It serves as the compare map in the strict biological realization within the Recognition Science framework. Researchers verifying admissible biological realizations cite this definition to establish the zero-cost property. The implementation is a direct case distinction on equality.
Claim. Let $a$ and $b$ be lineage states. The cost function is defined by $c(a,b)=0$ if $a=b$, and $c(a,b)=1$ otherwise.
background
A lineage state pairs a lineage label with a generation depth, both natural numbers, and carries decidable equality to support direct comparison. The module develops a strict biological realization over this carrier, where reproduction generates the logic and the cost measures state identity. This setup imports the music realization to embed biology inside the universal forcing chain.
proof idea
The definition is a one-line case split: return zero when the two LineageState arguments are equal and one otherwise, relying on the decidable equality instance derived for the structure.
why it matters
This cost definition populates the compare field of strictBiologyRealization, which is used to construct biology_admissible in the AdmissibleClass module. It thereby supplies the zero-cost condition for the biological domain in the Recognition framework. The downstream theorems lineageCost_self and lineageCost_symm derive the expected metric properties, and lineageCost_zero_iff confirms the equivalence to state identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.