def
definition
reproductiveStep
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.Biology on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
37 { lineage := a.lineage, generationDepth := a.generationDepth + b.generationDepth }
38
39def lineageZero : LineageState := ⟨0, 0⟩
40def reproductiveStep : LineageState := ⟨0, 1⟩
41
42/-- Strict biological realization using reproduction as the generator. -/
43def strictBiologyRealization : StrictLogicRealization where
44 Carrier := LineageState
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
59def biology_arith_equiv_logicNat :
60 (StrictLogicRealization.arith strictBiologyRealization).peano.carrier
61 ≃ ArithmeticFromLogic.LogicNat :=
62 (StrictLogicRealization.toLightweight strictBiologyRealization).orbitEquivLogicNat
63
64end Biology
65end Strict
66end UniversalForcing
67end Foundation
68end IndisputableMonolith