reproduce
plain-language theorem explainer
The reproduce definition constructs a combined lineage state by retaining the lineage label from the first input and summing the generation depths of both inputs. Researchers modeling admissible biological realizations within the Universal Forcing framework cite it as the explicit composition operation on LineageState. The definition proceeds by direct field construction that encodes addition on depths without additional lemmas.
Claim. Define the reproduction of two lineage states $a$ and $b$ by the state whose lineage label equals that of $a$ and whose generation depth equals the sum of the generation depths of $a$ and $b$.
background
The Strict Biology module supplies a domain-rich realization of biology inside the Universal Forcing framework. Its carrier is the structure LineageState, which consists of a natural-number lineage label together with a natural-number generation depth; the label prevents the type from collapsing to a bare Nat alias, so that arithmetic must be introduced explicitly via reproductive steps.
proof idea
The definition is a direct structural constructor: it copies the lineage field from the first argument and replaces the generation-depth field by the Nat sum of the two input depths.
why it matters
This definition supplies the compose operation inside strictBiologyRealization, which is then shown admissible in biology_admissible and used to witness the bilinear family forced by multiplicative consistency in DAlembert.Inevitability. It thereby anchors the biological model that feeds into RichDomainCostsCert, phi-ladder verification, and the reduction of simulation hypotheses to tautologies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.