lineageCost_zero_iff
plain-language theorem explainer
The equivalence establishes that lineage cost vanishes exactly when two lineage states coincide. Researchers verifying strict realizations of the Biology domain within the Recognition framework cite it to confirm that costs satisfy the zero-distance axiom. The argument unfolds the cost definition and splits cases on equality of the states.
Claim. For any lineage states $a$ and $b$, the cost function returns zero if and only if $a$ equals $b$.
background
The RichDomainCosts module supplies the concrete content for the five domain realizations (Music, Biology, Narrative, Ethics, Metaphysical) that were declared with placeholder laws. LineageState is the Biology carrier: a structure pairing a lineage label with a generation depth, both natural numbers, equipped with decidable equality. The function lineageCost is defined to return 0 on equal states and 1 otherwise, acting as a discrete indicator distance.
proof idea
Unfold the definition of lineageCost. Perform case analysis on whether the two states are equal. Simplification in the equal case yields the true statement 0 = 0; in the unequal case it yields the false statement 1 = 0, establishing both directions of the biconditional.
why it matters
The result is collected inside richDomainCostsCert_holds, which assembles the full certificate that all five domains satisfy the strict composition, decidability, and invariance laws. It supplies the zero-cost direction of the invariance law for the Biology realization, confirming that the cost structure is a proper metric component compatible with the composition law required by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.