strictBiologyRealization
plain-language theorem explainer
The definition assembles a StrictLogicRealization whose carrier is the set of lineage states, cost is the indicator function returning zero only on identical states, and generator is the reproductive step. Workers verifying the four canonical domains in the admissible class would cite it to confirm biology satisfies the strict axioms. The record is populated directly from sibling lemmas on lineageCost and reproductiveStep, with the nontrivial law reduced by a single simp.
Claim. The strict biological realization is the StrictLogicRealization with carrier the set of pairs $(l,g)$ where $l,g$ are natural numbers (lineage label and generation depth), cost function $c(a,b)=0$ if $a=b$ and $1$ otherwise, generator the reproductive step on states, identity the zero lineage state, and all required laws witnessed by the pre-established identities $c(a,a)=0$, $c(a,b)=c(b,a)$, and the trivial laws.
background
In the Strict/Biology module a lineage state is a pair of natural numbers consisting of a lineage label and a generation depth; the label prevents the carrier from being a bare Nat alias so that arithmetic must be generated by repeated reproductive steps. The cost between states is the indicator that vanishes exactly on equality, and the generator is the reproductive step that advances generation depth while preserving lineage. The module doc states this supplies a domain-rich biological realization over the simple lineage-state structure. Upstream, the compose operation from VirtueComposition supplies the pattern for combining generators, while one from IntegersFromLogic and RationalsFromLogic provide the neutral elements referenced in the realization laws.
proof idea
The definition is a direct record that sets Carrier to LineageState, Cost to Nat, zeroCost to the Nat instance, compare to lineageCost, compose to reproduce, one to lineageZero, and generator to reproductiveStep. The identity, non-contradiction, and excluded-middle laws are filled by the theorems lineageCost_self, lineageCost_symm, and True. The nontrivial law is discharged by the tactic simp [lineageCost, reproductiveStep, lineageZero].
why it matters
This definition supplies the biology_admissible witness inside AdmissibleClassCert, which records that all four canonical domains admit the universal forcing equivalence. It therefore closes the biology slot in the strict chain and feeds the axiom audit that equates the arithmetic carrier of the realization to LogicNat. The construction directly instantiates the Recognition Composition Law at the level of reproduction and confirms compatibility with the eight-tick octave structure without introducing extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.