reproduce_assoc
plain-language theorem explainer
Reproduction on lineage states is associative. Researchers verifying admissible realizations for the biology domain in the strict logic framework cite this when confirming the composition law. The proof is a one-line reduction that unfolds the definition of reproduction and applies associativity of natural-number addition.
Claim. For lineage states $a, b, c$, where reproduction preserves the lineage label of the first argument and adds the generation depths, one has $reproduce(reproduce(a,b),c) = reproduce(a, reproduce(b,c))$.
background
The Rich Domain Costs module supplies the actual composition, decidability, and invariance theorems for the five domain realizations (Music, Biology, Narrative, Ethics, Metaphysical) that were only placeholder laws in the source modules. A LineageState is a pair consisting of a lineage label and a generation depth, both natural numbers; the reproduce operation on two states retains the lineage label from the first argument and sums the generation depths. This theorem relies on the associativity of addition already established in ArithmeticFromLogic.add_assoc.
proof idea
The term proof unfolds the definition of reproduce on both sides, reducing the equality to an identity on the shared lineage label together with an equality of summed generation depths. The congr tactic then isolates the depth-sum equality, which is discharged directly by the upstream add_assoc lemma on natural numbers.
why it matters
The result is invoked inside biology_admissible to witness the composition law for the strict biology realization and is collected inside richDomainCostsCert_holds. It supplies the required associativity content for the biology domain in the Rich Domain Cost Theorems, thereby supporting the overall claim that the strict realizations are non-trivially law-bearing. In the Recognition framework this step closes one of the composition-law obligations needed for the forcing chain to reach admissible realizations without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.