LineageState
plain-language theorem explainer
LineageState pairs a natural-number lineage label with a generation depth to serve as the discrete carrier for strict biological descent models. Modelers of reproduction costs or lineage evolution cite it when building cost functions and reproductive operations over the Recognition framework. The declaration is a direct structure with two Nat fields and derived decidable equality.
Claim. A lineage state is a pair $(l, d) $ with $l, d $ natural numbers, where $l$ labels the descent line and $d$ records generational depth, equipped with decidable equality.
background
The Strict Biology module realizes biological processes over a minimal state structure that separates lineage identity from generational progress. LineageState supplies a lineage field to track distinct descent lines and a generationDepth field to accumulate reproductive increments. This design ensures that arithmetic on states arises only from explicit reproductive steps rather than from treating the carrier as a bare natural number.
proof idea
The declaration is a plain structure definition that introduces the two Nat fields and derives DecidableEq and Repr instances automatically.
why it matters
LineageState supplies the carrier type for every downstream biological definition in the module, including lineageCost, reproduce, and strictBiologyRealization. It grounds the biological domain in the Recognition framework by enforcing that state transitions occur only through repeated reproductive steps, consistent with the self-similar forcing chain. The structure closes the interface between the abstract lineage model and concrete cost and reproduction operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.