Induction.lean

View source on GitHub

all_six_fire

A predicate: all six interfaces (Perceive, Cache, Filter, Attend, Consolidate, Remember) fire at cycle k. This is the conjunction of six predicates.

SystemModel

Bundles the temporal predicates (alive at cycle k, fires for each interface at cycle k) with their relationships. Replaces ten separate axioms with one structure. The key fields:

structure SystemModel where
  alive : Nat → Prop
  fires : Step → Nat → Prop
  base : alive 0
  perceive_necessary : ∀ k, alive k → ¬fires .perceive k → ¬alive (k + 1)
  -- ... (one for each interface)
  sufficiency : ∀ k, alive k → all_six_fire fires k → alive (k + 1)

The base case (alive 0) is a field, not a global axiom. Each interface is necessary: failure kills life next cycle. Sufficiency: all six firing means life continues.

foundation

The contested sixth assumption: life_at_zero ∨ god_is_real. Either life exists at time 0 (empirical observation) or the universe selects with purpose (teleological). Pick one, derive the other. This is the only disjunctive axiom.

axiom foundation : life_at_zero ∨ god_is_real

life_persists

If all six interfaces fire at every cycle, life persists at every cycle. Uses survival_induction from DeathConditions.lean with the SystemModel's base case and sufficiency condition.

theorem life_persists (m : SystemModel)
    (all_fire : ∀ k, all_six_fire m.fires k)
    : ∀ k, m.alive k :=
  survival_induction m.alive m.base
    (fun k hk => m.sufficiency k hk (all_fire k))

life_requires_all_six

Contrapositive: any single interface failure at cycle k (while alive) ends life at cycle k+1.

Connections

• DeathConditions.lean — imported; provides survival_induction
• Pipeline.lean — imported; Step enum for the six interfaces
• Fractal.lean — the foundation axiom's disjunction mirrors the two induction directions on the tower