Perpetuity

Difficulty: hard — 7 definitions, 1 abbreviations, 4 lemmas, 7 theorems.

definition abbreviation lemma theorem

legend

A system is spontaneous in a state s when, left alone (fed only zero-size, “free” inputs — no energy or information supplied from outside), it necessarily runs down: either it’s already at rock bottom (‖s‖ = 0, nothing left to lose), or every free input available strictly decreases it, landing somewhere that is again spontaneous.

No state is both spontaneous and perpetuous (InformationSystem.perpetuous, below): a spontaneous state can’t recover for free, and perpetuity is exactly the promise of a free way back. This is “no perpetual motion” made precise — decay-when-left-alone and free recovery can’t coexist.

A system never sits by itself, though: whatever it loses has to go somewhere. Pairing a system with an environment — another system that receives whatever crosses the boundary — closes the loop into a universe: nothing is left to exchange with anything outside that pair at all. A system is natural when it has some environment that genuinely absorbs whatever it loses, rather than that loss vanishing into nothing.

Separately, we also look at what a system’s own history can and cannot tell you: whether a step can always be undone, and why a system with only finitely many states must eventually revisit one of them.

InformationSystem.perpetuous

A system is perpetuous in a state s when, no matter what inputs you’ve already fed it, you can always choose to feed it more that bring it back to exactly s — using only zero-size inputs, i.e. without needing any energy or information supplied from outside to do the resetting. (Without that restriction, “recovery” could always be bought by simply feeding in enough new information — not a fact about the system driving itself back, just about what a large enough external push can always achieve.)

def InformationSystem.perpetuous (sys : InformationSystem State Input Output) (s : State) : Prop :=
  ∀ is : List Input, ∃ is' : List Input, (∀ i ∈ is', ‖i‖ = 0) ∧
    (sys.eval s (is ++ is')).1 = s

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.eval

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Eq, Exists, List, Nonempty

Used by: InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.spontaneous_not_perpetuous

InformationSystem.roundtrip_neutral

Any run that returns to where it started is information-neutral overall: whatever detour the state took along the way, the total size of what went in exactly matches the total size of what came out, once the state is back where it began.

theorem InformationSystem.roundtrip_neutral (sys : InformationSystem State Input Output)
    (s : State) (is : List Input) (hreturn : (sys.eval s is).1 = s) :
    totalSize is = totalSize ((sys.eval s is).2) := by

Dependencies: InformationSystem, InformationSystem.eval, NormNonneg, totalSize

Proof dependencies: InformationSystem.eval_delta

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

Used by: InformationSystem.perpetuous_coherent

InformationSystem.perpetuous_coherent

Coherence: a perpetuous state can never permanently hoard information. Feed it any inputs you like; a perpetuous state guarantees some way to keep going that brings it back to exactly where it started, and by roundtrip_neutral, that whole round trip must be information-neutral. So whatever the state seemed to be holding onto partway through always has a way of being accounted for again in full, in what’s actually observed as output.

theorem InformationSystem.perpetuous_coherent (sys : InformationSystem State Input Output)
    (s : State) (hp : sys.perpetuous s) (is : List Input) :
    ∃ is', totalSize (is ++ is') = totalSize ((sys.eval s (is ++ is')).2) := by

Dependencies: InformationSystem, InformationSystem.eval, InformationSystem.perpetuous, NormNonneg, totalSize

Proof dependencies: InformationSystem.roundtrip_neutral

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Eq, Exists, List, Nonempty

Used by: (none)

InformationSystem.Spontaneous

A state is spontaneous when one of three things holds: it’s already at the bottom (‖s‖ = 0), or every free input strictly decreases it (decay), or every free input lands on a state that’s again spontaneous (next) — with no promise, on its own, that this particular input decreased anything. A state can coast on next for a while (a free input that only shuffles it sideways), as long as it’s always heading, eventually, towards bottom or a decay step; next alone, forever, in a loop back to where it started, is not a valid way to satisfy this (see spontaneous_no_self_return below for why).

inductive InformationSystem.Spontaneous (sys : InformationSystem State Input Output) : State → Prop
  | bottom {s : State} (h : ‖s‖ = 0) : sys.Spontaneous s
  | decay {s : State} (hlt : ∀ i, ‖i‖ = 0 → ‖(sys.step s i).1‖ < ‖s‖) : sys.Spontaneous s
  | next {s : State} (hnext : ∀ i, ‖i‖ = 0 → sys.Spontaneous ((sys.step s i).1)) :
      sys.Spontaneous s

Outer dependencies: InformationSystem

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, Nonempty

Used by: InformationSystem.natural, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous

InformationSystem.spontaneous

A whole system is spontaneous when every one of its states is: no matter where it currently sits, left alone it’s fated to eventually run down to nothing.

def InformationSystem.spontaneous (sys : InformationSystem State Input Output) : Prop :=
  ∀ s, sys.Spontaneous s

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.Spontaneous

Mathlib dependencies: Norm

Lean core dependencies: Nonempty

Used by: InformationSystem.spontaneous_not_perpetuous

InformationSystem.zero_run_le

Free inputs never increase size: conservation leaves nothing else it could do, since a zero-size input can only be balanced by the state losing exactly what the output picks up. This holds for any state, spontaneous or not.

theorem InformationSystem.zero_run_le (sys : InformationSystem State Input Output) (s : State)
    (is : List Input) (hzero : ∀ i ∈ is, ‖i‖ = 0) :
    ‖(sys.eval s is).1‖ ≤ ‖s‖ := by

Dependencies: InformationSystem, InformationSystem.eval, NormNonneg

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Int, Int.negOfNat, List, List.mem_cons_of_mem, List.mem_cons_self, Nat, Nonempty, congrArg, id, inferInstance, of_eq_true, rfl

Used by: InformationSystem.spontaneous_no_self_return

InformationSystem.spontaneous_no_self_return

A spontaneous state with something left to lose has no way back to exactly itself using only free inputs. The bottom and decay cases are immediate (rock bottom contradicts having something left to lose; a strict decrease can’t be undone by a run that only ever loses further ground, via zero_run_le). The next case is the interesting one: a free input might not decrease anything by itself, only promise that wherever it lands is again spontaneous. Name the state i moves s to s1. If the whole run i :: is' returns to s exactly, take is' and i in the opposite order instead, both starting from s1 this time: first is' (which, starting from s1, lands back on s, exactly by hypothesis), then i again (which, starting from s, lands on s1, by how s1 was defined in the first place). That’s another free run, is' ++ [i], this time starting and ending at s1 itself — a return-to-self one layer down in next’s own promise. Chasing this down as far as the proof of spontaneity goes has to end somewhere (bottom or decay), since a proof is a finite object — so this can’t go on forever, and no such run exists at any layer.

theorem InformationSystem.spontaneous_no_self_return (sys : InformationSystem State Input Output)
    (s : State) (hspon : sys.Spontaneous s) :
    0 < ‖s‖ → ∀ is : List Input, is ≠ [] → (∀ i ∈ is, ‖i‖ = 0) →
      (sys.eval s is).1 ≠ s := by

Dependencies: InformationSystem, InformationSystem.Spontaneous, InformationSystem.eval, NormNonneg

Proof dependencies: InformationSystem.eval_append, InformationSystem.zero_run_le

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, False.elim, Int, Int.negOfNat, List, List.mem_append, List.mem_cons_of_mem, List.mem_cons_self, List.mem_singleton, Nat, Ne, Nonempty, Not, Or, True, absurd, and_false, congrArg, forall_congr, id, implies_congr, inferInstance, not_false_eq_true, of_eq_true, or_false, rfl

Used by: InformationSystem.not_spontaneous_and_perpetuous

InformationSystem.not_spontaneous_and_perpetuous

No state is both spontaneous and perpetuous. Left alone, a spontaneous state (with something left to lose) has no free way back to exactly where it started (spontaneous_no_self_return); perpetuity promises exactly that. Applying the one to perpetuity’s own free recovery run is immediately contradictory.

(A zero-size state is excluded: sitting at rock bottom and staying there forever is not a contradiction, just a state with nothing left to lose in the first place. A “free” input — one that costs nothing — also has to actually exist for this to say anything: an input alphabet with no free option at all makes the whole question vacuous.)

theorem InformationSystem.not_spontaneous_and_perpetuous
    (sys : InformationSystem State Input Output) (s : State) (hpos : 0 < ‖s‖)
    (i0 : Input) (hi0 : ‖i0‖ = 0) :
    ¬ (sys.Spontaneous s ∧ sys.perpetuous s) := by

Dependencies: InformationSystem, InformationSystem.Spontaneous, InformationSystem.perpetuous, NormNonneg

Proof dependencies: InformationSystem.eval, InformationSystem.spontaneous_no_self_return

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Eq, Eq.trans, Exists, False, False.elim, List, List.eq_or_mem_of_mem_cons, Nonempty, Not, Or, True, congrArg, eq_false', noConfusion_of_Nat, not_false_eq_true, of_eq_true

Used by: InformationSystem.spontaneous_not_perpetuous

InformationSystem.spontaneous_not_perpetuous

A spontaneous system (every state runs down when left alone) can’t have any perpetuous state with something left to lose: sys.spontaneous already hands us spontaneity at that very state, so this is immediate from not_spontaneous_and_perpetuous.

theorem InformationSystem.spontaneous_not_perpetuous
    (sys : InformationSystem State Input Output) (hspon : sys.spontaneous)
    (s : State) (hpos : 0 < ‖s‖) (i0 : Input) (hi0 : ‖i0‖ = 0) :
    ¬ sys.perpetuous s :=

Dependencies: InformationSystem, InformationSystem.perpetuous, InformationSystem.spontaneous, NormNonneg

Proof dependencies: InformationSystem.Spontaneous, InformationSystem.not_spontaneous_and_perpetuous

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, Nonempty, Not

Used by: (none)

Environments, universes, and natural systems

A system’s Input/Output are the only two things that can ever cross its boundary. An environment for a system is simply another system, sitting on the other side of that boundary: it receives whatever the first system produces, and produces whatever the first system receives.

InformationSystem.Environment

An environment for sys: another information system that sits on the other side of sys’s boundary, receiving whatever sys produces and producing whatever sys receives.

structure InformationSystem.Environment (sys : InformationSystem State Input Output) where
  EnvState : Type
  nonempty : Nonempty EnvState
  size : Norm EnvState
  system : InformationSystem EnvState Output Input

Outer dependencies: InformationSystem

Mathlib dependencies: Norm

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

Used by: InformationSystem.Environment.ownState, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, InformationSystem.natural

InformationSystem.Environment.universe

Plugging sys into one of its own environments closes the loop into a universe: a system with nothing left to exchange with anything outside that pair at all. One step of delay (each side reacting to what the other one produced last time, rather than this very moment) is what lets each side’s own step stay an ordinary function of its own state and input, instead of two sides each waiting on the other’s answer to the same question.

def InformationSystem.Environment.universe {sys : InformationSystem State Input Output}
    (env : Environment sys) :
    letI := env.nonempty; letI := env.size
    InformationSystem (((State × env.EnvState) × Input) × Output) Unit Unit :=
  letI := env.nonempty; letI := env.size
  { step := fun (((s, e), i), o) _ =>
      let (s', o') := sys.step s i
      let (e', i') := env.system.step e o
      ((((s', e'), i'), o'), ())
    conserves := fun (((s, e), i), o) _ => by
      have h1 : ‖s‖ + ‖i‖ = ‖(sys.step s i).1‖ + ‖(sys.step s i).2‖ := sys.conserves s i
      have h2 : ‖e‖ + ‖o‖ = ‖(env.system.step e o).1‖ + ‖(env.system.step e o).2‖ :=
        env.system.conserves e o
      have hu : ‖(() : Unit)‖ = 0 := rfl
      show ‖s‖ + ‖e‖ + ‖i‖ + ‖o‖ + ‖(() : Unit)‖ =
        ‖(sys.step s i).1‖ + ‖(env.system.step e o).1‖ + ‖(env.system.step e o).2‖ +
          ‖(sys.step s i).2‖ + ‖(() : Unit)‖
      linarith }

Outer dependencies: InformationSystem, InformationSystem.Environment, instNormProd_computerNetworks, instNormUnit_computerNetworks

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

Used by: InformationSystem.Environment.universe_isolated

InformationSystem.isolated

A system has no environment interaction at all when nothing genuinely crosses its boundary, ever: whatever input it’s given carries no information, and whatever it produces carries none either.

def InformationSystem.isolated (sys : InformationSystem State Input Output) : Prop :=
  ∀ s i, ‖i‖ = 0 ∧ ‖(sys.step s i).2‖ = 0

Outer dependencies: InformationSystem

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Eq, Nonempty

Used by: InformationSystem.Environment.universe_isolated

InformationSystem.Environment.universe_isolated

A universe is always isolated: its own input and output are both Unit, which never carries any information at all (see Information) — there is nothing left outside it to exchange with.

theorem InformationSystem.Environment.universe_isolated
    {sys : InformationSystem State Input Output} (env : Environment sys) :
    letI := env.nonempty; letI := env.size
    env.universe.isolated :=

Dependencies: InformationSystem, InformationSystem.Environment, InformationSystem.Environment.universe, InformationSystem.isolated, NormNonneg, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, Nonempty, Prod, Unit, rfl

Used by: (none)

InformationSystem.Environment.ownState

sys’s own state, recovered from its universe’s combined state: this is the sense in which sys is part of env.universe — its own state is simply one piece of the universe’s.

abbrev InformationSystem.Environment.ownState {sys : InformationSystem State Input Output}
    (env : Environment sys) (w : ((State × env.EnvState) × Input) × Output) : State :=
  w.1.1.1

Outer dependencies: InformationSystem, InformationSystem.Environment

Mathlib dependencies: Norm

Lean core dependencies: Nonempty, Prod

Used by: (none)

InformationSystem.natural

A system is natural in a state s when it is spontaneous there (see Spontaneous) and has some environment that genuinely absorbs whatever it loses: an environment whose own state grows by exactly as much as the system’s state shrinks, at every free (zero-size) input. Nothing a natural system loses ever vanishes into nothing — it always leaks into its own surroundings instead, the way a real, physical system does.

def InformationSystem.natural (sys : InformationSystem State Input Output) (s : State) : Prop :=
  sys.Spontaneous s ∧ ∃ env : Environment sys,
    letI := env.nonempty; letI := env.size
    ∀ (e : env.EnvState) (i : Input), ‖i‖ = 0 →
      ‖(env.system.step e (sys.step s i).2).1‖ - ‖e‖ = ‖s‖ - ‖(sys.step s i).1‖

Outer dependencies: InformationSystem

Inner dependencies: InformationSystem.Environment, InformationSystem.Spontaneous

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Eq, Exists, Nonempty

Used by: (none)

Reversibility and recurrence

Two facts about information systems seen over time, in the spirit of thermodynamics’ “second law” — some things just can’t be undone.

If a step ever collides two distinct (state, input) pairs onto the same result, no function can recover which one actually happened: that distinguishing information is genuinely gone, not just hidden. The flip side: when step never collides anything (it’s injective), a recovery function does exist. This pins reversibility down exactly to injectivity.

Separately: a system with only finitely many states can’t keep every state it ever visits distinct forever — run it for longer than it has states, and some state must repeat. Once that happens, the two visits are the same state, so everything about what happens from then on is identical: the two histories become permanently indistinguishable from the outside.

InformationSystem.irreversible

If step collides two distinct (state, input) pairs onto the same result, no function can recover which one actually led to the result — a system that ever loses this kind of distinguishing information can never fully undo that loss. This is the sense in which information systems obey a “second law”, echoing thermodynamics’ second law: some processes just can’t be run backwards.

theorem InformationSystem.irreversible (sys : InformationSystem State Input Output)
    (s1 s2 : State) (i1 i2 : Input) (hne : (s1, i1) ≠ (s2, i2))
    (hcol : sys.step s1 i1 = sys.step s2 i2)
    (recover : State × Output → State × Input) (hrecover : ∀ s i, recover (sys.step s i) = (s, i)) :
    False := by

Dependencies: InformationSystem, NormNonneg

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Eq.symm, False, Ne, Nonempty, Prod, congrArg, id

Used by: (none)

InformationSystem.reversible

However, when no two distinct (state, input) pairs are ever collapsed onto the same result (this is what “injective” means for step), the system is reversible: a recovery function exists. Together with irreversible above, this pins reversibility down exactly to that property.

theorem InformationSystem.reversible (sys : InformationSystem State Input Output)
    (hinj : Function.Injective (fun p : State × Input => sys.step p.1 p.2)) :
    ∃ recover : State × Output → State × Input, ∀ s i, recover (sys.step s i) = (s, i) := by

Dependencies: InformationSystem, NormNonneg

Mathlib dependencies: Function.invFun, Function.leftInverse_invFun, Norm

Lean core dependencies: Eq, Exists, Function.Injective, Nonempty, Prod

Used by: (none)

InformationSystem.exists_repeat_state

A system with only finitely many states can’t keep every state it ever visits distinct: run it for longer than it has states, and some state along the way must repeat.

theorem InformationSystem.exists_repeat_state [Fintype State]
    (sys : InformationSystem State Input Output) (s : State) (is : List Input)
    (hlen : Fintype.card State < is.length) :
    ∃ i j, i < j ∧ j ≤ is.length ∧
      (sys.eval s (is.take i)).1 =
      (sys.eval s (is.take j)).1 := by

Dependencies: InformationSystem, InformationSystem.eval, NormNonneg

Mathlib dependencies: Fintype, Fintype.card, Fintype.card_fin, Fintype.exists_ne_map_eq_of_card_lt, Norm, lt_or_gt_of_ne

Used by: InformationSystem.exists_repeat_equivalent

InformationSystem.exists_repeat_equivalent

A Fintype-State system run long enough must revisit a state (exists_repeat_state), and from that point on its observable behaviour no longer depends on which of the two visits it came from (the two visits are the same state, so they have the same future behaviour outright) — the two histories become permanently indistinguishable.

theorem InformationSystem.exists_repeat_equivalent [Fintype State]
    (sys : InformationSystem State Input Output) (s : State) (is : List Input)
    (hlen : Fintype.card State < is.length) :
    ∃ i j, i < j ∧ j ≤ is.length ∧
      InformationSystem.equivalent sys sys
        ((sys.eval s (is.take i)).1)
        ((sys.eval s (is.take j)).1) := by

Dependencies: InformationSystem, InformationSystem.equivalent, InformationSystem.eval, NormNonneg

Proof dependencies: InformationSystem.exists_repeat_state

Mathlib dependencies: Fintype, Fintype.card, Norm

Lean core dependencies: And, Eq, Eq.mpr, Exists, List, List.length, List.take, Nat, Nonempty, congrArg, id

Used by: (none)

Dependency diagram

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

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend