MaxwellsDemon

Difficulty: hard — 3 definitions, 0 abbreviations, 1 lemmas, 7 theorems, 0 examples.

definition lemma theorem
legend
information-systems
def InformationSystem.gatedFlow {StateA StateB : Type} [Nonempty StateA] [Nonempty StateB] [Norm StateA]
  [Norm StateB] (transferAB : StateA → StateB → StateA × StateB)
  (hAB : ∀ (a : StateA) (b : StateB), ‖transferAB a b‖ = ‖a‖ + ‖b‖)
  (transferBA : StateA → StateB → StateA × StateB)
  (hBA : ∀ (a : StateA) (b : StateB), ‖transferBA a b‖ = ‖a‖ + ‖b‖) :
  InformationSystem (StateA × StateB) Bool Bool
Show details 
| InformationSystem.gatedFlow transferAB hAB transferBA hBA =
  {
    step := fun p dir =>
      if dir = true then
        if ‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖ then
          (transferAB p.1 p.2, true)
        else (p, false)
      else
        if ‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖ then
          (transferBA p.1 p.2, true)
        else (p, false),
    conserves := ⋯ }

Complexity: 967 (size of the value term)

Outer dependencies: InformationSystem, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Decidable, Eq, Eq.mpr, Eq.symm, Eq.trans, GT.gt, Nonempty, Not, Prod, True, congr, congrArg, eq_self, id, if_neg, if_pos, ite, of_eq_true, rfl

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

theorem InformationSystem.gatedFlow_success_AB {StateA StateB : Type} [Nonempty StateA] [Nonempty StateB]
  [Norm StateA] [Norm StateB] (transferAB : StateA → StateB → StateA × StateB)
  (hAB : ∀ (a : StateA) (b : StateB), ‖transferAB a b‖ = ‖a‖ + ‖b‖)
  (transferBA : StateA → StateB → StateA × StateB)
  (hBA : ∀ (a : StateA) (b : StateB), ‖transferBA a b‖ = ‖a‖ + ‖b‖) (p : StateA × StateB) :
  ((InformationSystem.gatedFlow transferAB hAB transferBA hBA).step p true).2 = true ↔
    ‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖
Show details 
fun {StateA StateB} [Nonempty StateA] [Nonempty StateB] [Norm StateA] [Norm StateB] transferAB hAB
    transferBA hBA p =>
  id
    (Decidable.casesOn instDecidableAnd
      (fun h =>
        Eq.mpr
          (id
            (congrFun' (congrArg Iff (congrFun' (congrArg Eq (congrArg Prod.snd (if_neg h))) true))
              (‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖)))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congr (congrArg Iff Bool.false_eq_true)
                  (congrFun' (congrArg And gt_iff_lt._simp_1) (‖(transferAB p.1 p.2).1‖ < ‖p.1‖)))
                (false_iff (‖p.2‖ < ‖(transferAB p.1 p.2).2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖)))
              (Eq.trans not_and._simp_1
                (Eq.trans
                  (implies_congr_ctx (Eq.refl (‖p.2‖ < ‖(transferAB p.1 p.2).2‖)) fun a =>
                    Eq.trans not_lt._simp_1
                      ((fun a =>
                          eq_true
                            (id
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg Not
                                      (congrFun' (congrArg And gt_iff_lt._simp_1)
                                        (‖(transferAB p.1 p.2).1‖ < ‖p.1‖)))
                                    not_and._simp_1)
                                  (implies_congr_ctx (Eq.refl (‖p.2‖ < ‖(transferAB p.1 p.2).2‖))
                                    fun a => not_lt._simp_1))
                                h)
                              a))
                        a))
                  (implies_true (‖p.2‖ < ‖(transferAB p.1 p.2).2‖)))))))
      fun h =>
      Eq.mpr
        (id
          (congrFun' (congrArg Iff (congrFun' (congrArg Eq (congrArg Prod.snd (if_pos h))) true))
            (‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖)))
        (of_eq_true
          (Eq.trans
            (congr (congrArg Iff (eq_self true))
              (Eq.trans
                (congr
                  (congrArg And
                    (Eq.trans gt_iff_lt._simp_1
                      (eq_true
                        (id
                            (Eq.mp
                              (congrFun' (congrArg And gt_iff_lt._simp_1)
                                (‖(transferAB p.1 p.2).1‖ < ‖p.1‖))
                              h)).1)))
                  (eq_true
                    (id
                        (Eq.mp
                          (congrFun' (congrArg And gt_iff_lt._simp_1)
                            (‖(transferAB p.1 p.2).1‖ < ‖p.1‖))
                          h)).2))
                (and_self True)))
            (iff_self True))))

Complexity: 15823 (size of the value term)

Dependencies: InformationSystem.gatedFlow, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Bool.false_eq_true, Decidable, Eq, Eq.mp, Eq.mpr, Eq.trans, False, GT.gt, Iff, Nonempty, Not, Prod, True, and_self, congr, congrArg, congrFun', eq_self, eq_true, false_iff, id, if_neg, if_pos, iff_self, implies_congr_ctx, implies_true, ite, of_eq_true

Used by: (none)

theorem InformationSystem.gatedFlow_success_BA {StateA StateB : Type} [Nonempty StateA] [Nonempty StateB]
  [Norm StateA] [Norm StateB] (transferAB : StateA → StateB → StateA × StateB)
  (hAB : ∀ (a : StateA) (b : StateB), ‖transferAB a b‖ = ‖a‖ + ‖b‖)
  (transferBA : StateA → StateB → StateA × StateB)
  (hBA : ∀ (a : StateA) (b : StateB), ‖transferBA a b‖ = ‖a‖ + ‖b‖) (p : StateA × StateB) :
  ((InformationSystem.gatedFlow transferAB hAB transferBA hBA).step p false).2 = true ↔
    ‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖
Show details 
fun {StateA StateB} [Nonempty StateA] [Nonempty StateB] [Norm StateA] [Norm StateB] transferAB hAB
    transferBA hBA p =>
  id
    (Decidable.casesOn instDecidableAnd
      (fun h =>
        Eq.mpr
          (id
            (congrFun' (congrArg Iff (congrFun' (congrArg Eq (congrArg Prod.snd (if_neg h))) true))
              (‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖)))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congr (congrArg Iff Bool.false_eq_true)
                  (congrFun' (congrArg And gt_iff_lt._simp_1) (‖(transferBA p.1 p.2).2‖ < ‖p.2‖)))
                (false_iff (‖p.1‖ < ‖(transferBA p.1 p.2).1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖)))
              (Eq.trans not_and._simp_1
                (Eq.trans
                  (implies_congr_ctx (Eq.refl (‖p.1‖ < ‖(transferBA p.1 p.2).1‖)) fun a =>
                    Eq.trans not_lt._simp_1
                      ((fun a =>
                          eq_true
                            (id
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg Not
                                      (congrFun' (congrArg And gt_iff_lt._simp_1)
                                        (‖(transferBA p.1 p.2).2‖ < ‖p.2‖)))
                                    not_and._simp_1)
                                  (implies_congr_ctx (Eq.refl (‖p.1‖ < ‖(transferBA p.1 p.2).1‖))
                                    fun a => not_lt._simp_1))
                                h)
                              a))
                        a))
                  (implies_true (‖p.1‖ < ‖(transferBA p.1 p.2).1‖)))))))
      fun h =>
      Eq.mpr
        (id
          (congrFun' (congrArg Iff (congrFun' (congrArg Eq (congrArg Prod.snd (if_pos h))) true))
            (‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖)))
        (of_eq_true
          (Eq.trans
            (congr (congrArg Iff (eq_self true))
              (Eq.trans
                (congr
                  (congrArg And
                    (Eq.trans gt_iff_lt._simp_1
                      (eq_true
                        (id
                            (Eq.mp
                              (congrFun' (congrArg And gt_iff_lt._simp_1)
                                (‖(transferBA p.1 p.2).2‖ < ‖p.2‖))
                              h)).1)))
                  (eq_true
                    (id
                        (Eq.mp
                          (congrFun' (congrArg And gt_iff_lt._simp_1)
                            (‖(transferBA p.1 p.2).2‖ < ‖p.2‖))
                          h)).2))
                (and_self True)))
            (iff_self True))))

Complexity: 15823 (size of the value term)

Dependencies: InformationSystem.gatedFlow, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Bool.false_eq_true, Decidable, Eq, Eq.mp, Eq.mpr, Eq.trans, False, GT.gt, Iff, Nonempty, Not, Prod, True, and_self, congr, congrArg, congrFun', eq_self, eq_true, false_iff, id, if_neg, if_pos, iff_self, implies_congr_ctx, implies_true, ite, of_eq_true

Used by: (none)

def Cell : Type
Show details 
| Cell = (Bool × Bool)

Complexity: 5 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Bool, Prod

Used by: Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective, instDecidableEqCell, instFintypeCell, instNonemptyCell, instNormCell, instNormNonnegCell

instance instFintypeCell : Fintype Cell
Show details 
| instFintypeCell = { elems := instFintypeCell._aux_1, complete := instFintypeCell._proof_3 }

Complexity: 7 (size of the value term)

Outer dependencies: Cell

Mathlib dependencies: Finset, Finset.univ, Fintype

Lean core dependencies: Bool, Prod

Used by: Cell.erase_not_surjective

instance instDecidableEqCell : DecidableEq Cell
Show details 
| instDecidableEqCell = instDecidableEqCell._aux_1

Complexity: 1 (size of the value term)

Outer dependencies: Cell

Lean core dependencies: Bool, DecidableEq, Prod

Used by: Cell.erase_not_injective

instance instNonemptyCell : Nonempty Cell
Show details 
Nonempty.intro (false, false)

Complexity: 13 (size of the value term)

Outer dependencies: Cell

Lean core dependencies: Bool, Nonempty

Used by: Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective

instance instNormCell : Norm Cell
Show details 
| instNormCell = { norm := fun x => 2 }

Complexity: 21 (size of the value term)

Outer dependencies: Cell

Mathlib dependencies: Norm, Real

Lean core dependencies: Nat

Used by: Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective, instNormNonnegCell

instance instNormNonnegCell : NormNonneg Cell
Show details 
{
  nonneg := fun x =>
    id
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true)) }

Complexity: 235 (size of the value term)

Outer dependencies: Cell, NormNonneg, instNormCell

Mathlib dependencies: Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real

Lean core dependencies: Bool, Nat, id

Used by: (none)

def Cell.eraseSecondBit : InformationSystem Cell Unit Unit
Show details 
| Cell.eraseSecondBit =
  { step := fun c x => ((c.1, false), ()), conserves := Cell.eraseSecondBit._proof_1 }

Complexity: 57 (size of the value term)

Outer dependencies: Cell, InformationSystem, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Inner dependencies: instNormProd_computerNetworks

Mathlib dependencies: Real, add_zero

Lean core dependencies: Bool, Eq, Eq.trans, Prod, True, Unit, Unit.unit, congr, congrArg, eq_self, of_eq_true

Used by: Cell.erase_not_injective, Cell.erase_not_surjective

theorem Cell.erase_not_injective : ¬Function.Injective fun c => (Cell.eraseSecondBit.step c ()).1
Show details 
fun hinj =>
  have this := hinj rfl;
  absurd this (of_decide_eq_true (id (Eq.refl true)))

Complexity: 344 (size of the value term)

Dependencies: Cell, Cell.eraseSecondBit, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Proof dependencies: instDecidableEqCell

Lean core dependencies: Bool, Decidable.decide, Eq, False, Function.Injective, Not, Unit, Unit.unit, absurd, id, of_decide_eq_true, rfl

Used by: Cell.erase_not_surjective

theorem Cell.erase_not_surjective : ¬Function.Surjective fun c => (Cell.eraseSecondBit.step c ()).1
Show details 
Eq.mpr (id (congrArg (fun _a => ¬_a) (Eq.symm (propext Finite.injective_iff_surjective))))
  Cell.erase_not_injective

Complexity: 567 (size of the value term)

Dependencies: Cell, Cell.eraseSecondBit, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Proof dependencies: Cell.erase_not_injective, instFintypeCell

Mathlib dependencies: Finite.injective_iff_surjective

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Function.Injective, Function.Surjective, Not, Unit, Unit.unit, congrArg, id

Used by: (none)

Dependency diagram

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

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend