Axioms.lean

View source on GitHub

capacity_bound

Bounded energy means bounded distinguishable states. A system with finite energy can only maintain finitely many internal states. This gives the finite state space (Fin N) that downstream proofs need.

axiom capacity_bound (energy : Nat) (he : energy > 0) :
  &exists; N : Nat, 0 < N ∧ N ≤ energy

If you reject this (allow infinite states), the pigeonhole principle fails and there is no forced state collision.

rate_mismatch

Input can arrive faster than the system processes it. Environments are richer than processors.

axiom rate_mismatch :
  &exists; (input_rate drain_rate : Nat),
    input_rate > drain_rate ∧ drain_rate > 0

Without this, no buffer is ever needed — Cache becomes optional.

NonStationary

Environments change. At some period p, the required response at time t differs from time t + p. This is a property of specific environments, not a universal law.

def NonStationary {O : Type} (required : Nat → O) (p : Nat) : Prop :=
  &exists; t, required t ≠ required (t + p)

positive_loss

Bounded systems lose information each cycle. At least some bits are irreversibly lost per processing step.

axiom positive_loss : &exists; (loss : Nat), loss > 0

Without this, lossless computation is possible and a closed loop can survive indefinitely.

history_matters

History-dependent tasks exist: the correct response to the same input can depend on what happened before.

axiom history_matters :
  &exists; (env : Nat → Nat) (required : Nat → Nat),
    HistoryDependent env required

Without this, all tasks are memoryless stimulus-response and persistence is unnecessary.

BoundedTransducer

The unified formal model: a finite-state machine with Fin N states, processing an input stream and producing output. Its step function is deterministic: given a state and an input, it produces exactly one next state and one output.

structure BoundedTransducer (N : Nat) (I O : Type) where
  step : Fin N → I → Fin N × O

This is the machine that Stochasticity.lean shows is limited: determinism + finite states means it cannot distinguish arbitrarily many histories.

Connections

• Boundary.lean — derives that each pipeline stage is forced from these axioms
• Removal.lean — removes each postcondition and shows the system dies, citing these axioms
• Stochasticity.lean — uses capacity_bound + BoundedTransducer to show deterministic limits
• Pigeonhole.lean — the collision that capacity_bound enables