strictBiologyRealization
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim LineageState models all biological processes.
- Does not derive the phi-ladder or mass formula from this carrier.
- Does not establish equivalence to non-strict biological models.
- Does not address spatial dimensions or continuous time.
Lean usage
noncomputable def biology_adm : AdmissibleRealization strictBiologyRealization := biology_admissibleformal statement (Lean)
43def strictBiologyRealization : StrictLogicRealization where
44 Carrier := LineageState
proof body
Definition body.
45 Cost := Nat
46 zeroCost := inferInstance
47 compare := lineageCost
48 compose := reproduce
49 one := lineageZero
50 generator := reproductiveStep
51 identity_law := lineageCost_self
52 non_contradiction_law := lineageCost_symm
53 excluded_middle_law := True
54 composition_law := True
55 invariance_law := True
56 nontrivial_law := by
57 simp [lineageCost, reproductiveStep, lineageZero]
58