`Generation`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization
domain: Foundation
line: 18 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  15open ArithmeticFromLogic
  16open Invariance.Universal
  17
  18abbrev Generation := Nat
  19
  20def biologyCost (a b : Generation) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem biologyCost_self (a : Generation) : biologyCost a a = 0 := by
  24  simp [biologyCost]
  25
  26theorem biologyCost_symm (a b : Generation) : biologyCost a b = biologyCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [biologyCost]
  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [biologyCost, h, h']
  31
  32def biologyInterpret (n : LogicNat) : Generation :=
  33  LogicNat.toNat n
  34
  35/-- Biological realization as generation-count comparison. -/
  36def biologyRealization : LogicRealization where
  37  Carrier := Generation
  38  Cost := Nat
  39  zeroCost := inferInstance
  40  compare := biologyCost
  41  zero := 0
  42  step := Nat.succ
  43  Orbit := LogicNat
  44  orbitZero := LogicNat.zero
  45  orbitStep := LogicNat.succ
  46  interpret := biologyInterpret
  47  interpret_zero := by rfl
  48  interpret_step := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.