lineageCost_decidable
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not define or compute the lineage cost function.
- Does not establish zero-cost equivalence or triangle inequality.
- Applies only to the biology domain, not the other four domains.
- Does not address invariance under relabeling of the carrier.
formal statement (Lean)
83def lineageCost_decidable (a b : LineageState) : Decidable (a = b) :=
proof body
Definition body.
84 inferInstance
85