lineageCost_decidable
plain-language theorem explainer
Lineage states pair a lineage label with a generation depth in the biology domain. This definition supplies a decision procedure for equality between any two such states, enabling the excluded-middle law for the corresponding domain cost. It is cited in arguments that the strict realization carries non-trivial logical content beyond placeholders. The implementation is a one-line wrapper invoking the derived DecidableEq instance on the structure.
Claim. For any lineage states $a$ and $b$, the proposition $a = b$ is decidable.
background
LineageState is the structure carrying a lineage label (Nat) and generation depth (Nat), with DecidableEq derived by construction. The module supplies concrete decidability, zero-cost equivalence, associativity, and invariance statements for each of the five domain costs, replacing the True placeholders that appear in the source Music, Biology, Narrative, Ethics, and Metaphysical modules. The upstream result is the LineageState definition whose automatic DecidableEq derivation is used here.
proof idea
The definition is a one-line wrapper that applies inferInstance to the DecidableEq instance derived for LineageState.
why it matters
It supplies the excluded-middle content required for the biology domain cost inside the Rich Domain Cost Theorems. The module documentation states that these statements are the first-class versions anyone should cite when claiming the strict realization is non-trivially law-bearing. It therefore supports the composition, invariance, and triangle-inequality properties that close the forcing chain for domain costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.