Removal.lean
View source on GitHubThe falsifiability test: for each postcondition in the pipeline, removing it leads to system death. Ten conjuncts, each derived from the declared axioms. This is the machine-checked version of the claim that 
theory is load-bearing — remove any piece and the structure collapses.
survives / theorem healthy_survives
A system survives if injection exceeds loss at every cycle. When injected bits per cycle exceed lost bits, the system stays alive indefinitely.
no_perceive_death (P1)
Zero injection with any positive loss kills the system. Without Perceive injecting new bits, the closed loop bleeds out.
no_cache_death (C1)
Rate mismatch without a buffer means cumulative loss — one item lost per cycle minimum, compounding forever.
cache_must_evict (C2)
A bounded store with positive input rate fills eventually. The cache must evict or the system halts.
no_attend_death (A1)
Input-only selection (ignoring policy) fails on history-dependent tasks. Same input, different required response — at least one must be wrong.
theorem no_attend_death
{I O : Type} (select : I → O)
(env : Nat → I) (required : Nat → O)
(t₁ t₂ : Nat)
(hsame : env t₁ = env t₂)
(hdiff : required t₁ ≠ required t₂)
: select (env t₁) ≠ required t₁ ∨
select (env t₂) ≠ required t₂attend_must_rank (A2)
A binary gate with two output bins cannot distinguish three or more classes. Pigeonhole: 3 items into 2 bins means at least two collide and get the same treatment, causing an error when they need different treatment.
attend_must_be_stochastic (A3)
A deterministic transducer with a state+input collision and different requirements must err at one of the colliding times.
no_consolidate_death (Co1)
A fixed (non-adapting) transducer with a collision must eventually produce wrong output. Same mechanism as A3.
no_remember_death (R1)
A transducer with frozen state (resets each cycle) fails on history-dependent tasks. It has state machinery but cannot persist state across cycles, so same input always gives same output.
removal_tests
All ten postcondition removals assembled into one theorem. Eight derive conclusions directly from the axioms. A3 and Co1 take a state collision as hypothesis (the collision itself is guaranteed by capacity_bound + pigeonhole, proved separately).
Connections
- Axioms.lean — imported; each removal test cites specific axioms
- Pigeonhole.lean — provides the state collision that A3 and Co1 assume
- Stochasticity.lean — the full deterministic limitation argument
- Boundary.lean — the boundary arguments that these removal tests formalize