lineageZero
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not define any operations on lineage states.
- Does not prove algebraic properties such as associativity of reproduction.
- Does not connect lineage states to physical constants or forcing-chain steps T5-T8.
formal statement (Lean)
39def lineageZero : LineageState := ⟨0, 0⟩