lineageZero
plain-language theorem explainer
The definition supplies the zero element of the LineageState structure that anchors the strict biological realization. Researchers formalizing admissible biological models cite it as the neutral base case for the reproduction generator. It is introduced by direct construction as the pair of zero coordinates.
Claim. The zero lineage state is the element of the LineageState structure whose lineage label is $0$ and whose generation depth is $0$, written $⟨0, 0⟩$.
background
The module Strict/Biology.lean develops a domain-rich biological realization over a simple lineage-state structure. A lineage state consists of a generation-depth coordinate together with a lineage label; the label ensures that arithmetic operations are induced by repeated application of the reproductive step rather than being presupposed by the type name.
proof idea
The definition is introduced by direct construction using the structure constructor applied to the pair of zeros.
why it matters
This zero element is required by strictBiologyRealization to equip the carrier with a neutral element and is invoked in the proof of reproduce_left_id together with the construction of biology_admissible. It anchors the biological sector of the universal forcing framework by supplying the base case for lineage evolution under the reproduction generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.