lineageCost_self
plain-language theorem explainer
The identity establishes that the cost between any lineage state and itself is zero. Researchers constructing strict biological realizations in the Universal Forcing framework cite it to confirm the zero element of the cost monoid on LineageState. The proof is a one-line wrapper that applies the simplifier directly to the conditional definition of lineageCost.
Claim. For every lineage state $a$ (a pair of natural-number lineage label and generation depth), the cost of $a$ relative to itself equals zero.
background
The Strict Biology module supplies a domain-rich realization of biological processes over a simple carrier. A lineage state is a structure with a natural-number lineage label and a generation depth; the label prevents the type from collapsing to a bare natural number, so that arithmetic is generated by repeated reproductive steps rather than by the carrier name itself.
proof idea
The proof is a one-line wrapper that invokes simp on the definition of lineageCost. The simplifier immediately matches the equality case in the conditional definition and discharges the goal.
why it matters
The identity is invoked inside the definition of strictBiologyRealization, which equips LineageState with the Nat cost and the reproduce composition to produce a StrictLogicRealization. It thereby supplies the required zero-cost element for the biology domain inside the Universal Forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.