DeathConditions.lean

View source on GitHub

Budget

An information budget tracks bits through the pipeline. Input bits come from Perceive; loss bits leave through the competitive core (Filter + Attend + Consolidate). The budget must balance: input must cover loss.

broken_step_death

Death condition 1: a broken step leaks extra bits. If a morphism's contract fails and leaks extra_leak bits per cycle, the cumulative leak eventually exceeds any finite budget.

theorem broken_step_death
    (budget extra_leak : Nat) (hleak : extra_leak > 0)
    : &exists; n : Nat, n * extra_leak > budget

The proof picks n = budget + 1. At that point, (budget + 1) * extra_leak ≥ budget + 1 > budget.

closed_loop_zero_input

Death condition 2: a closed loop has zero input. With any positive loss per cycle, state bits deplete to zero. At cycle state: state * loss ≥ state.

decaying_input_death

Death condition 3: decaying input. If input decays by some amount each cycle, cumulative decay eventually exceeds the initial input.

survival_induction

Standard induction on natural numbers, named for use by the life_persists theorem in Induction.lean. Given a base case and an inductive step, the property holds for all n.

theorem survival_induction
    (contract_holds : Nat → Prop)
    (base : contract_holds 0)
    (step : ∀ n, contract_holds n → contract_holds (n + 1))
    : ∀ n, contract_holds n

Connections

• Induction.lean — imports survival_induction; uses it to prove life persists when all six fire
• Handshake.lean — the information budget constraints (InformationBudget, closed_loop_budget_negative)
• Removal.lean — each removal test is one of these death conditions instantiated