InformationSystems

Difficulty: moderate — 5 definitions, 8 abbreviations, 9 lemmas, 2 theorems.

definition abbreviation lemma theorem

legend

We model information systems by means of an abstract mechanism, with a boundary between that what is outside and inside. At any moment, the mechanism has a particular internal state. Given an input, the mechanism ‘takes a step’ and produces an output and moves to the next state. These kinds of mechanisms are also called “Mealy machines”. In InformationSystem we add one thing on top of Mealy machines: we measure information. As a metaphor, one may think of an information system as a balloon where its volume represents its ‘information contents’. Over time it can inflate and deflate.

For every step, the information already contained in the current state plus the amount of input information must be equal to the amount of information output plus the amount of information left in its final state. The total amount of information must be ‘conserved’. This means that, overall, information is neither created nor destroyed and only moved between states, input and output. We nickname this conservation principle the “first law”, echoing how thermodynamics (the physics of heat and energy dynamics) has a first law saying energy is never created or destroyed, only moved around. Later on, we also formalize ‘natural’ information systems that obey a “second law”, where we have the eventual decrease in information similar to how a balloon slowly deflates over time.

This file develops the basic theory of information systems on its own. Component.Impl builds components out of them.

For further (optional) reading: - Weber, Transforming a single-valued transducer into a Mealy machine, Journal of Computer and System Sciences 56(1):46-59, 1998. - Chapin, A deeper look at data in Proceedings of the 1968 23rd ACM national conference, pp. 631–638, 1968.

instNormUnit_computerNetworks

Technical — you can skip this.

Unit carries no information: its one value always has measure zero.

instance : Norm Unit where
  norm _ := 0

Outer dependencies: (none)

Mathlib dependencies: Norm, Real

Lean core dependencies: Unit

instNormNonnegUnit

Technical — you can skip this.

instance : NormNonneg Unit := ⟨fun _ => le_refl 0⟩

Outer dependencies: NormNonneg, instNormUnit_computerNetworks

Mathlib dependencies: Real, le_refl

Lean core dependencies: Unit

Used by: (none)

instNormProd_computerNetworks

Technical — you can skip this.

A pair’s measure is the sum of its components’ measures.

instance [Norm α] [Norm β] : Norm (α × β) where
  norm p := ‖p.1‖ + ‖p.2‖

Outer dependencies: (none)

Mathlib dependencies: Norm, Real

Lean core dependencies: Prod

instNormNonnegProd

Technical — you can skip this.

instance [Norm α] [Norm β] [NormNonneg α] [NormNonneg β] : NormNonneg (α × β) :=

Outer dependencies: NormNonneg, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real, add_nonneg

Lean core dependencies: Prod

Used by: (none)

instNormBool_computerNetworks

Technical — you can skip this.

A bare Bool carries no information of its own, the same way Unit doesn’t: see Information for why (Bit is Bool’s information-carrying counterpart).

instance : Norm Bool where
  norm _ := 0

Outer dependencies: (none)

Mathlib dependencies: Norm, Real

Lean core dependencies: Bool

Used by: InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Receiver.step, Receiver.step_correct, Sender.step, discrete_Bool, instNormNonnegBool

instNormNonnegBool

Technical — you can skip this.

instance : NormNonneg Bool := ⟨fun _ => le_refl 0⟩

Outer dependencies: NormNonneg, instNormBool_computerNetworks

Mathlib dependencies: Real, le_refl

Lean core dependencies: Bool

Used by: (none)

discrete_Unit

Technical — you can skip this.

Unit, Bool, and any pair of discrete types are themselves discrete: none of this plumbing introduces any fractional measure.

theorem discrete_Unit : Discrete Unit := fun _ => ⟨0, by change (0:ℝ) = ((0:Nat):ℝ); norm_num⟩

Dependencies: Discrete, instNormUnit_computerNetworks

Mathlib dependencies: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real

Lean core dependencies: Eq, Nat, Nat.cast, Unit, id

Used by: (none)

discrete_Bool

Technical — you can skip this.

theorem discrete_Bool : Discrete Bool := fun _ => ⟨0, by change (0:ℝ) = ((0:Nat):ℝ); norm_num⟩

Dependencies: Discrete, instNormBool_computerNetworks

Mathlib dependencies: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real

Lean core dependencies: Bool, Eq, Nat, Nat.cast, id

Used by: (none)

Discrete.prod

Technical — you can skip this.

theorem Discrete.prod {α β : Type} [Norm α] [Norm β] (hα : Discrete α) (hβ : Discrete β) :
    Discrete (α × β) :=

Dependencies: Discrete, instNormProd_computerNetworks

Proof dependencies: Discrete.size, Discrete.size_eq

Mathlib dependencies: Nat.cast_add, Norm, Real

Lean core dependencies: Eq, Eq.mpr, Nat, Nat.cast, Prod, congrArg, id

Used by: (none)

InformationSystem

A minimal formalization of an information system: it has a state, and given an input, it produces an output and a new state. ‖x‖ is the real-valued measure of x (defined in Information) — how much information x carries. Every information system needs a measure for its own state, inputs, and outputs. We require the “first law” to hold always: the measure of any given state plus any input equals the measure of the next state plus the output. Further, we do not allow ‘empty’ states, inputs, or outputs (where there are zero possible values).

Note that the ‘state space’ of an information system can be very simple (incapable of holding any information at all) or very complex (e.g. the brain of a human). For simplicity, we asumme information systems are ‘deterministic’: for every state and input, the next state and output are fully determined. However, in reality, no state can be perfectly known, by which one recovers the appearance of ‘non-deterministic’ systems.

information-systems

structure InformationSystem (State Input Output : Type)
    [Norm State] [Norm Input] [Norm Output]
    [Nonempty State] [Nonempty Input] [Nonempty Output] where
  step : State → Input → State × Output
  conserves : ∀ s i, ‖s‖ + ‖i‖ = ‖step s i‖

Outer dependencies: (none)

Inner dependencies: instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, HEq, Nat, Nonempty, Prod, SizeOf, eq_of_heq

InformationSystem.Step

A witness that one step really took place: starting in current, given input, the system moves to next and produces output — and holds is the proof that this is genuinely what the system’s own rule does, not just any four values glued together.

structure InformationSystem.Step (sys : InformationSystem State Input Output) where
  current : State
  input : Input
  next : State
  output : Output
  holds : sys.step current input = (next, output)

Outer dependencies: InformationSystem

Mathlib dependencies: Norm

Lean core dependencies: Eq, HEq, Nat, Nonempty, Prod, SizeOf, eq_of_heq

Used by: InformationSystem.Run, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.trajectory, InformationSystem.Step.bottom, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.stepAt

InformationSystem.stepAt

The witness for the one step sys actually takes from s, given i.

abbrev InformationSystem.stepAt (sys : InformationSystem State Input Output) (s : State) (i : Input) :
    Step sys where
  current := s
  input := i
  next := (sys.step s i).1
  output := (sys.step s i).2
  holds := rfl

Outer dependencies: InformationSystem, InformationSystem.Step

Mathlib dependencies: Norm

Lean core dependencies: Nonempty, Prod, rfl

Used by: InformationSystem.delta, InformationSystem.parallel_delta, InformationSystem.sequential_delta

InformationSystem.Step.delta

The information delta of a step: input measure minus output measure. Positive means the system gains information (it consumed more than it revealed), negative means it loses information (it revealed more than it consumed), and zero means neither.

abbrev InformationSystem.Step.delta {sys : InformationSystem State Input Output} (st : Step sys) :
    ℝ :=
  ‖st.input‖ - ‖st.output‖

Outer dependencies: InformationSystem, InformationSystem.Step

Mathlib dependencies: Norm, Real

Lean core dependencies: Nonempty

Used by: InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.delta, InformationSystem.parallel_delta, InformationSystem.sequential_delta

InformationSystem.delta

The information delta of the step sys takes from s, given i: shorthand for the delta of its own witness.

abbrev InformationSystem.delta (sys : InformationSystem State Input Output)
    (s : State) (i : Input) : ℝ :=
  (sys.stepAt s i).delta

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.Step.delta, InformationSystem.stepAt

Mathlib dependencies: Norm, Real

Lean core dependencies: Nonempty

Used by: Channel.loss, InformationSystem.eval_delta, InformationSystem.parallel_delta, InformationSystem.sequential_delta

InformationSystem.Step.delta_trichotomy

Trivial: on every step, an information system either gains, loses, or neither.

theorem InformationSystem.Step.delta_trichotomy {sys : InformationSystem State Input Output}
    (st : Step sys) : st.delta < 0 ∨ st.delta = 0 ∨ st.delta > 0 :=

Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta

Mathlib dependencies: Norm, Real, lt_trichotomy

Lean core dependencies: Eq, GT.gt, Nonempty, Or

Used by: (none)

InformationSystem.Step.delta_alt

The delta of a step is exactly how much more information the system has in its next state compared to its current state: a system gains information when the next state is larger, it loses information when the next state is smaller than the current one.

theorem InformationSystem.Step.delta_alt {sys : InformationSystem State Input Output}
    (st : Step sys) : st.delta = ‖st.next‖ - ‖st.current‖ := by

Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta

Proof dependencies: instNormProd_computerNetworks

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Int, Int.negOfNat, Nat, Nonempty, Not.intro, Prod, congrArg, id, inferInstance, rfl

Used by: InformationSystem.Step.gains, InformationSystem.Step.loses

InformationSystem.Step.loses

When a system loses information (more output than input), the excess must come from the state: the next state shrinks compared to the current one.

theorem InformationSystem.Step.loses {sys : InformationSystem State Input Output} (st : Step sys) :
    st.delta < 0 ↔ ‖st.next‖ < ‖st.current‖ := by

Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta

Proof dependencies: InformationSystem.Step.delta_alt

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Iff, Int, Int.negOfNat, Nat, Nonempty, congrArg, id, inferInstance, rfl

Used by: (none)

InformationSystem.Step.gains

When a system gains information (less output than input), the difference must end up somewhere: the next state grows compared to the current one.

theorem InformationSystem.Step.gains {sys : InformationSystem State Input Output} (st : Step sys) :
    st.delta > 0 ↔ ‖st.next‖ > ‖st.current‖ := by

Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta

Proof dependencies: InformationSystem.Step.delta_alt

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, GT.gt, Iff, Int, Int.negOfNat, Nat, Nonempty, congrArg, id, inferInstance, rfl

Used by: (none)

InformationSystem.Step.bottom

When an information system is fully squeezed out (the state carries no information at all), it can never produce more output than it receives as input.

theorem InformationSystem.Step.bottom {sys : InformationSystem State Input Output}
    [NormNonneg State] (st : Step sys) : ‖st.current‖ = 0 → ‖st.output‖ ≤ ‖st.input‖ := by

Dependencies: InformationSystem, InformationSystem.Step, NormNonneg

Proof dependencies: instNormProd_computerNetworks

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Int, Int.negOfNat, Nat, Nonempty, Prod, congrArg, id, inferInstance, rfl

Used by: (none)

InformationSystem.eval

Evaluate a system over a list of inputs, fed into step one at a time, in order: each input moves the system to the state reached after the previous input (or the initial state, for the first one). What comes out is the state reached at the end, together with the list of outputs produced along the way.

def InformationSystem.eval (sys : InformationSystem State Input Output) :
    State → List Input → State × List Output
  | s, [] => (s, [])
  | s, i :: is =>
    let (s', o) := sys.step s i
    let (s'', os) := sys.eval s' is
    (s'', o :: os)

Outer dependencies: InformationSystem

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Eq.symm, List, Nonempty, PProd, PUnit, Prod, congrArg, id

InformationSystem.eval_append

Evaluating a system over two input lists back to back lands on the same final state as evaluating it over the first list, then continuing from wherever that left off over the second.

theorem InformationSystem.eval_append (sys : InformationSystem State Input Output) (s : State)
    (is1 is2 : List Input) :
    (sys.eval s (is1 ++ is2)).1 = (sys.eval (sys.eval s is1).1 is2).1 := by

Dependencies: InformationSystem, InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.trans, List, Nonempty, Prod, True, congrArg, congrFun', eq_self, of_eq_true

Used by: InformationSystem.spontaneous_no_self_return

totalSize

The total measure of a list of values, under their canonical real-valued measure.

abbrev totalSize [Norm α] (l : List α) : ℝ :=
  (l.map (‖·‖)).sum

Outer dependencies: (none)

Mathlib dependencies: Norm, Real

Lean core dependencies: List, List.map, List.sum

Used by: Channel.lossy_loses_overall, Channel.overall_loss, InformationSystem.eval_delta, InformationSystem.eval_trichotomy, InformationSystem.perpetuous_coherent, InformationSystem.roundtrip_neutral

InformationSystem.eval_trichotomy

Over any evaluated input list, an information system either gains, loses, or neither overall (again trivial).

theorem InformationSystem.eval_trichotomy (sys : InformationSystem State Input Output)
    (s : State) (is : List Input) :
    totalSize (sys.eval s is).2 < totalSize is ∨
    totalSize is < totalSize (sys.eval s is).2 ∨
    totalSize is = totalSize (sys.eval s is).2 := by

Dependencies: InformationSystem, InformationSystem.eval, totalSize

Mathlib dependencies: Norm, Real, lt_trichotomy

Lean core dependencies: Eq, Eq.symm, List, Nonempty, Or

Used by: (none)

InformationSystem.eval_delta

Two ways to look at an information system over time, agreeing exactly: - step by step starting in an initial state, where we plus all the inputs minus all the outputs (no need to look at any intermediary state) - by looking only at the initial and final state, their information difference is that very same quantity.

theorem InformationSystem.eval_delta (sys : InformationSystem State Input Output)
    (s : State) (is : List Input) :
    ‖(sys.eval s is).1‖ - ‖s‖ = totalSize is - totalSize (sys.eval s is).2 := by

Dependencies: InformationSystem, InformationSystem.eval, totalSize

Proof dependencies: InformationSystem.delta

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Int, Int.negOfNat, List, Nat, Nonempty, Not.intro, True, congr, congrArg, eq_self, id, inferInstance, of_eq_true, rfl

Used by: Channel.overall_loss, InformationSystem.roundtrip_neutral

InformationSystem.Run

A run: a chain of witnessed steps, each one landing exactly where the next one starts. At least one step is required — a run always actually goes somewhere.

structure InformationSystem.Run (sys : InformationSystem State Input Output) where
  steps : List (Step sys)
  nonempty : steps ≠ []
  chained : steps.IsChain (fun a b => a.next = b.current)

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.Step

Mathlib dependencies: Norm

Lean core dependencies: Eq, HEq, List, Nat, Ne, Nonempty, SizeOf, eq_of_heq

Used by: InformationSystem.Run.cycle, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.trajectory, InformationSystem.Run.trajectory_head

InformationSystem.Run.initial

The state a run starts in: its first step’s own starting state.

abbrev InformationSystem.Run.initial {sys : InformationSystem State Input Output} (r : Run sys) :
    State :=
  (r.steps.head r.nonempty).current

Outer dependencies: InformationSystem, InformationSystem.Run

Inner dependencies: InformationSystem.Step

Mathlib dependencies: Norm

Lean core dependencies: List.head, Nonempty

Used by: InformationSystem.Run.cycle, InformationSystem.Run.trajectory, InformationSystem.Run.trajectory_head

InformationSystem.Run.final

The state a run ends in: its last step’s own resulting state.

abbrev InformationSystem.Run.final {sys : InformationSystem State Input Output} (r : Run sys) :
    State :=
  (r.steps.getLast r.nonempty).next

Outer dependencies: InformationSystem, InformationSystem.Run

Inner dependencies: InformationSystem.Step

Mathlib dependencies: Norm

Lean core dependencies: List.getLast, Nonempty

Used by: InformationSystem.Run.cycle

InformationSystem.Run.trajectory

The sequence of states a run visits, forgetting every input and output along the way: the initial state, followed by the state reached after each step.

abbrev InformationSystem.Run.trajectory {sys : InformationSystem State Input Output} (r : Run sys) :
    List State :=
  r.initial :: r.steps.map (·.next)

Outer dependencies: InformationSystem, InformationSystem.Run

Inner dependencies: InformationSystem.Run.initial, InformationSystem.Step

Mathlib dependencies: Norm

Lean core dependencies: List, List.map, Nonempty

Used by: InformationSystem.Run.trajectory_head

InformationSystem.Run.trajectory_head

A run’s trajectory always starts with the run’s own initial state.

theorem InformationSystem.Run.trajectory_head {sys : InformationSystem State Input Output}
    (r : Run sys) : r.trajectory.head? = some r.initial := rfl

Dependencies: InformationSystem, InformationSystem.Run, InformationSystem.Run.initial, InformationSystem.Run.trajectory

Mathlib dependencies: Norm

Lean core dependencies: Eq, List.head?, Nonempty, Option, rfl

Used by: (none)

InformationSystem.Run.cycle

A cycle: a run that starts and ends in the same state.

abbrev InformationSystem.Run.cycle {sys : InformationSystem State Input Output} (r : Run sys) :
    Prop :=
  r.initial = r.final

Outer dependencies: InformationSystem, InformationSystem.Run

Inner dependencies: InformationSystem.Run.final, InformationSystem.Run.initial

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nonempty

Used by: (none)

InformationSystem.equivalent

Two information systems (possibly with different states, even different state types) are equivalent from a chosen initial state each when they’re indistinguishable from the outside: feeding the very same sequence of inputs to both, both yield exactly the same sequence of outputs, no matter how long those input sequences are or what input values were chosen. This is what we call a state’s observable behaviour: everything about the outputs evaluating produces from that state onward, with the state itself left out of the picture. In particular, since step is a plain function of state and input, two literally equal states always produce the same outputs from then on, so they always have the same observable behaviour too.

def InformationSystem.equivalent {State1 State2 : Type}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    (sys1 : InformationSystem State1 Input Output) (sys2 : InformationSystem State2 Input Output)
    (s1 : State1) (s2 : State2) : Prop :=
  ∀ is : List Input, (sys1.eval s1 is).2 = (sys2.eval s2 is).2

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, List, Nonempty

InformationSystem.equivalent_output

Equivalent systems agree on the very next output, for any single input.

theorem InformationSystem.equivalent_output {State1 State2 : Type}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    {sys1 : InformationSystem State1 Input Output} {sys2 : InformationSystem State2 Input Output}
    {s1 : State1} {s2 : State2} (h : InformationSystem.equivalent sys1 sys2 s1 s2) (i : Input) :
    (sys1.step s1 i).2 = (sys2.step s2 i).2 := by

Dependencies: InformationSystem, InformationSystem.equivalent

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, HEq, List, Nonempty, eq_of_heq

Used by: Component.Impl.Hom.toSpec, Component.Impl.parallel_congr, Component.Impl.recast_congr, Component.Impl.sequential_congr

InformationSystem.equivalent_step

Equivalent systems remain equivalent after taking the very same single step.

theorem InformationSystem.equivalent_step {State1 State2 : Type}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    {sys1 : InformationSystem State1 Input Output} {sys2 : InformationSystem State2 Input Output}
    {s1 : State1} {s2 : State2} (h : InformationSystem.equivalent sys1 sys2 s1 s2) (i : Input) :
    InformationSystem.equivalent sys1 sys2 (sys1.step s1 i).1 (sys2.step s2 i).1 := by

Dependencies: InformationSystem, InformationSystem.equivalent

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, HEq, List, Nonempty, eq_of_heq

Used by: Component.Impl.parallel_congr, Component.Impl.recast_congr, Component.Impl.sequential_congr

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend