Corollary.lean

View source on GitHub

competitive_core_removes (Corollary 1)

Bounded storage forces selection. Selection on a set produces a proper subset. After k cycles, at least k items are removed. This is the competitive core: winners persist, losers are discarded.

theorem competitive_core_removes
    (input_count output_count k : Nat)
    (hsel : output_count < input_count)
    : k * (input_count - output_count) ≥ k

policy_evicted_in_shared_pool (Corollary 2)

If policy and data share a bounded pool, and data arrives faster than free capacity allows, data overflows and evicts policy. This is not tautological — it derives eviction from bounded capacity, unequal arrival rates, and first-in eviction under pressure.

shared_pool_kills_policy

After enough cycles, all policy slots can be overwritten by data. This forces type separation: policy and data must live in different stores. That is why Attend (read policy) and Consolidate (write policy) are separate interfaces.

theorem shared_pool_kills_policy
    (capacity data_rate policy_slots : Nat)
    (hoverflow : data_rate > capacity - policy_slots)
    : policy_slots * (data_rate + policy_slots - capacity) ≥ policy_slots

SeparatePolicyStore (Corollary 3)

A separate policy store needs both interfaces: read (apply policy to data — Attend) and write (update policy from outcomes — Consolidate). Without read, policy exists but is never applied. Without write, policy is static and cannot adapt.

static_policy_fails

A static policy in a non-stationary environment eventually mismatches the required behavior. If the optimal policy changes over time and different policies produce different outputs, the fixed policy fails on some input at some time.

Connections

• Axioms.lean — imported; capacity_bound and rate_mismatch drive the corollaries
• Boundary.lean — the boundary arguments that these corollaries extend
• Removal.lean — the full removal table includes the shared-pool test