← back to lean navigator

Boundary.lean

ghView source on GitHub

Proves that removing any pipeline stage leads to a measurable bad outcome — each stage is forced by the axioms, not optional. Each proof here is a formal instance of why jktheory is load-bearing: the stages exist because the math demands them.

perceive_forced

The environment has strictly more distinguishable configurations than the system can represent internally. A lossy encoding step (Perceive) is forced to bridge the gap.

theorem perceive_forced (energy env_dim : Nat)
    (henv : env_dim > energy)
    : ∀ N : Nat, N ≤ energy → env_dim > N

Derived from capacity_bound. If internal state could be as large as the environment, no lossy encoding would be needed.

no_cache_cumulative_loss

Without a buffer, rate mismatch causes cumulative loss. If input arrives faster than drain, at least one item is lost per cycle, and the loss compounds over time.

theorem no_cache_cumulative_loss
    (input_rate drain_rate k : Nat)
    (hmismatch : input_rate > drain_rate)
    : k * (input_rate - drain_rate) ≥ k

Derived from rate_mismatch. If input never exceeds drain rate, no buffer is needed.

cache_from_rate_mismatch

Cache existence follows directly from the rate_mismatch axiom: the axiom guarantees a scenario where input outpaces drain, and without a buffer, loss is cumulative.

no_filter_fills_store

Without selection, a store of finite capacity fills after enough insertions. Once full, the system halts or drops items implicitly. Explicit selection (Filter) prevents this.

theorem no_filter_fills_store
    (capacity items_per_cycle : Nat) (hitems : items_per_cycle > 0)
    : &exists; t : Nat, t * items_per_cycle ≥ capacity

no_persistence_no_memory

Without persistence, a system with fixed state is a pure function of current input. Same input always produces same output regardless of history. This makes the system unable to handle history-dependent tasks.

Connections

← Handshake.lean · 6 of 25 by june.kim Uniqueness.lean · 8 of 25 →