reproduce_left_id
plain-language theorem explainer
The reproduce_left_id theorem shows that applying the reproduce operation with lineageZero on the left to an arbitrary lineage state a produces a state whose lineage label is zero while its generation depth equals that of a. Researchers verifying the composition axioms for the Biology domain in the strict logic realizations would cite this result. The proof is a short tactic sequence that unfolds the two definitions, applies congruence on the structure, and simplifies the field equations.
Claim. For any lineage state $a$, reproduce(lineageZero, $a$) equals the state whose lineage component is lineageZero.lineage and whose generationDepth component is $a$.generationDepth.
background
LineageState is a structure pairing a lineage label (Nat) with a generation depth (Nat); the label prevents reduction to a bare depth counter, so that arithmetic arises only from iterated reproduction steps. lineageZero is the base element with both fields zero. The reproduce operation on states $a$ and $b$ returns a state whose lineage is taken from $a$ and whose depth is the sum of the two depths.
proof idea
The proof unfolds reproduce and lineageZero, then uses congr 1 to match the structure constructor and simp to discharge the resulting field equalities. It is a direct one-line wrapper around the definitions with no additional lemmas.
why it matters
This theorem supplies the left-identity law for the reproduce operation inside the Biology domain, one of the five concrete realizations that replace the True placeholders in StrictLogicRealization. It contributes to the module's suite of decidability, zero-cost, associativity, and invariance results that make the domain costs law-bearing rather than vacuous. The surrounding Rich Domain Cost Theorems section states that these are the statements to cite when claiming non-trivial composition and invariance for each domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.