pith. machine review for the scientific record. sign in
def definition def or abbrev high

biologyRealization

show as:
view Lean formalization →

The definition supplies a concrete LogicRealization for biology by taking the carrier to be the natural numbers that count generations. Researchers tracing the universal forcing chain from logic through arithmetic to biology would cite it when they need an explicit model of reproductive steps. The construction is a direct record that wires Nat operations to the required fields and inherits the orbit axioms from LogicNat.

claimThe biological realization is the structure whose carrier is the set of natural numbers (generation counts), whose cost is the standard comparison on those numbers, whose zero is 0, whose step is the successor, and whose orbit is identified with the logic-forced naturals via the identity equivalence.

background

The module presents a lightweight biological realization whose carrier is generation count and whose generator is the reproductive step. Generation is the type alias for the natural numbers. LogicNat is the inductive type with constructors identity and step that encodes the orbit closed under multiplication by the generator; its successor is defined as the step constructor and its toNat map reads off the iteration count. The definition imports LogicRealization and relies on the upstream theorems succ_injective (Peano P2) and the induction principle of LogicNat.

proof idea

The definition populates the LogicRealization record by assigning Carrier to Generation (i.e., Nat), Cost to biologyCost, Orbit to LogicNat, and the equivalence to the reflexive map. Commutation of interpret with successor is obtained by reflexivity; orbit_no_confusion and orbit_step_injective are delegated to the corresponding theorems on LogicNat; induction is obtained by applying LogicNat.induction; nontriviality is witnessed by the element 1 together with the cost property.

why it matters in Recognition Science

This definition realizes the biological layer inside UniversalForcing and is used directly by biology_arith_equiv_nat to identify the arithmetic carrier with LogicNat. It supplies the concrete generation-count model required to embed biology into the forcing chain that runs from the Law of Logic through the eight-tick octave to three spatial dimensions. No open scaffolding questions are closed by this declaration.

scope and limits

Lean usage

noncomputable def equiv : (arithmeticOf biologyRealization).peano.carrier ≃ LogicNat := biology_arith_equiv_nat

formal statement (Lean)

  36def biologyRealization : LogicRealization where
  37  Carrier := Generation

proof body

Definition body.

  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
  49    intro n
  50    show LogicNat.toNat (LogicNat.succ n) = Nat.succ (LogicNat.toNat n)
  51    rfl
  52  orbit_no_confusion := by intro n h; exact LogicNat.zero_ne_succ n h
  53  orbit_step_injective := LogicNat.succ_injective
  54  orbit_induction := by
  55    intro P h0 hs n
  56    exact LogicNat.induction (motive := P) h0 hs n
  57  orbitEquivLogicNat := Equiv.refl LogicNat
  58  orbitEquiv_zero := rfl
  59  orbitEquiv_step := by intro n; rfl
  60  identity := biologyCost_self
  61  nonContradiction := biologyCost_symm
  62  excludedMiddle := True
  63  composition := True
  64  actionInvariant := True
  65  nontrivial := by
  66    refine ⟨1, ?_⟩
  67    simp [biologyCost]
  68

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.