Implementation

Difficulty: moderate — 4 definitions, 10 abbreviations, 10 lemmas, 2 theorems, 0 examples.

definition abbreviation lemma theorem

legend

ImportantinstNonemptyForallFin_computerNetworks

instance instNonemptyForallFin_computerNetworks.{u_1} {α : Sort u_1} [Nonempty α] {n : ℕ} :
  Nonempty (Fin n → α)

Show details

fun {α} [inst : Nonempty α] {n} => Nonempty.intro fun x => Classical.choice inst

Complexity: 25 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Fin, Nat, Nonempty

Used by: Channel, Component, Component.Arrow, Component.Arrow.Equiv, Component.Arrow.setoid, Component.Hom.tensor, Component.Hom.tensor_id_id, Component.Simplex.toInformationSystem, Component.empty, Component.empty_parallel, Component.equivalent_of_stationary, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast, Component.recast_congr, Component.sequential, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, InformationSystem.parallel_delta, InformationSystem.sequential_delta, InformationSystem.toSimplex

NoteComponent

abbrev Component (State Input Output : Type) [Nonempty State] [Norm State] [Nonempty Input] [Norm Input]
  [Nonempty Output] [Norm Output] (n m : ℕ) : Type

Show details

| Component State Input Output n m = InformationSystem State (Fin n → Input) (Fin m → Output)

Complexity: 85 (size of the value term)

Outer dependencies: (none)

Inner dependencies: InformationSystem, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: Component.Arrow, Component.Demultiplex, Component.Hom.recast_recast, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.Multiplex, Component.Simplex, Component.empty, Component.empty_parallel, Component.equivalent_of_stationary, Component.id, Component.id_sequential, Component.interchange, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast, Component.recast_congr, Component.recast_parallel_left, Component.recast_parallel_right, Component.recast_recast, Component.sequential, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry, InformationSystem.parallel

NoteComponent.Simplex

abbrev Component.Simplex (State Input Output : Type) [Nonempty State] [Norm State] [Nonempty Input]
  [Norm Input] [Nonempty Output] [Norm Output] : Type

Show details

| Component.Simplex State Input Output = Component State Input Output 1 1

Complexity: 69 (size of the value term)

Outer dependencies: (none)

Inner dependencies: Component

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: Channel, Component.Simplex.toInformationSystem, InformationSystem.toSimplex

NoteComponent.Multiplex

abbrev Component.Multiplex (State Input Output : Type) [Nonempty State] [Norm State] [Nonempty Input]
  [Norm Input] [Nonempty Output] [Norm Output] (n : ℕ) : Type

Show details

| Component.Multiplex State Input Output n = Component State Input Output n 1

Complexity: 63 (size of the value term)

Outer dependencies: (none)

Inner dependencies: Component

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: (none)

NoteComponent.Demultiplex

abbrev Component.Demultiplex (State Input Output : Type) [Nonempty State] [Norm State] [Nonempty Input]
  [Norm Input] [Nonempty Output] [Norm Output] (n : ℕ) : Type

Show details

| Component.Demultiplex State Input Output n = Component State Input Output 1 n

Complexity: 63 (size of the value term)

Outer dependencies: (none)

Inner dependencies: Component

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: (none)

NoteComponent.sequential

def Component.sequential {State1 State2 Mid Input Output : Type} [Nonempty State1] [Norm State1]
  [Nonempty State2] [Norm State2] [Nonempty Mid] [Norm Mid] [Nonempty Input] [Norm Input]
  [Nonempty Output] [Norm Output] {n m p : ℕ} (c1 : Component State1 Input Mid n m)
  (c2 : Component State2 Mid Output m p) : Component (State1 × State2) Input Output n p

Show details

| c1.sequential c2 =
  {
    step := fun p_1 i =>
      match c1.step p_1.1 i with
      | (s1', mv) =>
        match c2.step p_1.2 mv with
        | (s2', ov) => ((s1', s2'), ov),
    conserves := ⋯ }

Complexity: 463 (size of the value term)

Outer dependencies: Component, instNormProd_computerNetworks

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq

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

Used by: Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id_sequential, Component.interchange, Component.parallel_comm, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry_symmetry, InformationSystem.sequential, InformationSystem.sequential_delta

NoteComponent.parallel

def Component.parallel {State1 State2 Input Output : Type} [Nonempty State1] [Norm State1]
  [Nonempty State2] [Norm State2] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output]
  {n1 m1 n2 m2 : ℕ} (c1 : Component State1 Input Output n1 m1)
  (c2 : Component State2 Input Output n2 m2) :
  Component (State1 × State2) Input Output (n1 + n2) (m1 + m2)

Show details

| c1.parallel c2 =
  {
    step := fun p iv =>
      match c1.step p.1 fun k => iv (Fin.castAdd n2 k) with
      | (s1', o1) =>
        match c2.step p.2 fun k => iv (Fin.natAdd n1 k) with
        | (s2', o2) => ((s1', s2'), Fin.append o1 o2),
    conserves := ⋯ }

Complexity: 617 (size of the value term)

Outer dependencies: Component, instNormProd_computerNetworks

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right, Fin.sum_univ_add, Finset, Finset.sum, Finset.sum_congr, Finset.univ, Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, Int, Int.negOfNat, Nat, Nonempty, Not.intro, Prod, True, congr, congrArg, congrFun', eq_self, id, inferInstance, of_eq_true, rfl

Used by: Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.tensor, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.interchange, Component.monoidalCategory, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast_parallel_left, Component.recast_parallel_right, InformationSystem.parallel, InformationSystem.parallel_delta

NoteComponent.id

def Component.id (Input : Type) [Nonempty Input] [Norm Input] (n : ℕ) : Component Unit Input Input n n

Show details

| Component.id Input n = { step := fun x iv => ((), iv), conserves := ⋯ }

Complexity: 97 (size of the value term)

Outer dependencies: Component, instNormUnit_computerNetworks

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Finset, Finset.sum, Finset.sum_congr, Finset.univ, Norm, Real, zero_add

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

Used by: Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id_sequential, Component.monoidalCategory, Component.sequential_id, Component.symmetry_symmetry

NoteComponent.symmetry

def Component.symmetry (Input : Type) [Nonempty Input] [Norm Input] (n m : ℕ) :
  Component Unit Input Input (n + m) (m + n)

Show details

| Component.symmetry Input n m =
  {
    step := fun x iv =>
      ((), Fin.append (fun k => iv (Fin.natAdd n k)) fun k => iv (Fin.castAdd m k)),
    conserves := ⋯ }

Complexity: 235 (size of the value term)

Outer dependencies: Component, instNormUnit_computerNetworks

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right, Fin.sum_univ_add, Finset, Finset.sum, Finset.sum_congr, Finset.univ, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Fin.castAdd, Fin.natAdd, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, id, rfl

Used by: Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor_comm, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_comm, Component.symmetry_symmetry

TipComponent.id_sequential

theorem Component.id_sequential {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State : Type} [Nonempty State] [Norm State] {n m : ℕ}
  (c : Component State Input Output n m) (s : State) :
  InformationSystem.equivalent ((Component.id Input n).sequential c) c ((), s) s

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State}
    [Nonempty State] [Norm State] {n m} c s =>
  have hstep := fun x x_1 => rfl;
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s : State),
      (InformationSystem.eval ((Component.id Input n).sequential c) ((), s) is).2 =
        (InformationSystem.eval c s is).2)
    (fun s => Eq.refl (InformationSystem.eval ((Component.id Input n).sequential c) ((), s) []).2)
    (fun i is ih s =>
      Eq.mpr
        (id
          (congrFun'
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg (InformationSystem.eval ((Component.id Input n).sequential c))
                          (congrArg Prod.fst ((fun s i => hstep s i) s i)))
                        is)))
                  (congr (congrArg List.cons (congrArg Prod.snd ((fun s i => hstep s i) s i)))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg (InformationSystem.eval ((Component.id Input n).sequential c))
                          (congrArg Prod.fst ((fun s i => hstep s i) s i)))
                        is))))))
            ((c.1 s i).2 :: (InformationSystem.eval c (c.1 s i).1 is).2)))
        (congrArg (List.cons (c.step s i).2) (ih (c.step s i).1)))
    is s

Complexity: 10663 (size of the value term)

Dependencies: Component, Component.id, Component.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, congrFun', id, rfl

Used by: Component.Hom.id_comp

TipComponent.sequential_id

theorem Component.sequential_id {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State : Type} [Nonempty State] [Norm State] {n m : ℕ}
  (c : Component State Input Output n m) (s : State) :
  InformationSystem.equivalent (c.sequential (Component.id Output m)) c (s, ()) s

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State}
    [Nonempty State] [Norm State] {n m} c s =>
  have hstep := fun x x_1 => rfl;
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s : State),
      (InformationSystem.eval (c.sequential (Component.id Output m)) (s, ()) is).2 =
        (InformationSystem.eval c s is).2)
    (fun s => Eq.refl (InformationSystem.eval (c.sequential (Component.id Output m)) (s, ()) []).2)
    (fun i is ih s =>
      Eq.mpr
        (id
          (congrFun'
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg (InformationSystem.eval (c.sequential (Component.id Output m)))
                          (congrArg Prod.fst ((fun s i => hstep s i) s i)))
                        is)))
                  (congr (congrArg List.cons (congrArg Prod.snd ((fun s i => hstep s i) s i)))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg (InformationSystem.eval (c.sequential (Component.id Output m)))
                          (congrArg Prod.fst ((fun s i => hstep s i) s i)))
                        is))))))
            ((c.1 s i).2 :: (InformationSystem.eval c (c.1 s i).1 is).2)))
        (congrArg (List.cons (c.step s i).2) (ih (c.step s i).1)))
    is s

Complexity: 10663 (size of the value term)

Dependencies: Component, Component.id, Component.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, congrFun', id, rfl

Used by: Component.Hom.comp_id

TipComponent.sequential_assoc

theorem Component.sequential_assoc {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 State2 State3 Mid1 Mid2 : Type} [Nonempty State1]
  [Norm State1] [Nonempty State2] [Norm State2] [Nonempty State3] [Norm State3] [Nonempty Mid1]
  [Norm Mid1] [Nonempty Mid2] [Norm Mid2] {n m p q : ℕ} (c1 : Component State1 Input Mid1 n m)
  (c2 : Component State2 Mid1 Mid2 m p) (c3 : Component State3 Mid2 Output p q) (s1 : State1)
  (s2 : State2) (s3 : State3) :
  InformationSystem.equivalent ((c1.sequential c2).sequential c3) (c1.sequential (c2.sequential c3))
    ((s1, s2), s3) (s1, s2, s3)

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output]
    {State1 State2 State3 Mid1 Mid2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    [Nonempty State3] [Norm State3] [Nonempty Mid1] [Norm Mid1] [Nonempty Mid2] [Norm Mid2]
    {n m p q} c1 c2 c3 s1 s2 s3 =>
  have hstep := fun x x_1 x_2 x_3 => rfl;
  have hstep' := fun x x_1 x_2 x_3 => rfl;
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s1 : State1) (s2 : State2) (s3 : State3),
      (InformationSystem.eval ((c1.sequential c2).sequential c3) ((s1, s2), s3) is).2 =
        (InformationSystem.eval (c1.sequential (c2.sequential c3)) (s1, s2, s3) is).2)
    (fun s1 s2 s3 =>
      Eq.refl (InformationSystem.eval ((c1.sequential c2).sequential c3) ((s1, s2), s3) []).2)
    (fun i is ih s1 s2 s3 =>
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg (InformationSystem.eval ((c1.sequential c2).sequential c3))
                          (congrArg Prod.fst ((fun s1 s2 s3 i => hstep s1 s2 s3 i) s1 s2 s3 i)))
                        is)))
                  (congr
                    (congrArg List.cons
                      (congrArg Prod.snd ((fun s1 s2 s3 i => hstep s1 s2 s3 i) s1 s2 s3 i)))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg (InformationSystem.eval ((c1.sequential c2).sequential c3))
                          (congrArg Prod.fst ((fun s1 s2 s3 i => hstep s1 s2 s3 i) s1 s2 s3 i)))
                        is))))))
            (congrArg Prod.snd
              (congr
                (congrArg Prod.mk
                  (congrArg Prod.fst
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1.sequential (c2.sequential c3)))
                        (congrArg Prod.fst ((fun s1 s2 s3 i => hstep' s1 s2 s3 i) s1 s2 s3 i)))
                      is)))
                (congr
                  (congrArg List.cons
                    (congrArg Prod.snd ((fun s1 s2 s3 i => hstep' s1 s2 s3 i) s1 s2 s3 i)))
                  (congrArg Prod.snd
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1.sequential (c2.sequential c3)))
                        (congrArg Prod.fst ((fun s1 s2 s3 i => hstep' s1 s2 s3 i) s1 s2 s3 i)))
                      is)))))))
        (congrArg (List.cons (c3.step s3 (c2.step s2 (c1.step s1 i).2).2).2)
          (ih (c1.step s1 i).1 (c2.step s2 (c1.step s1 i).2).1
            (c3.step s3 (c2.step s2 (c1.step s1 i).2).2).1)))
    is s1 s2 s3

Complexity: 44079 (size of the value term)

Dependencies: Component, Component.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, Prod, congr, congrArg, congrFun', id, rfl

Used by: Component.Hom.comp_assoc

TipComponent.sequential_congr

theorem Component.sequential_congr {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 State2 State1' State2' Mid : Type} [Nonempty State1]
  [Norm State1] [Nonempty State2] [Norm State2] [Nonempty State1'] [Norm State1'] [Nonempty State2']
  [Norm State2'] [Nonempty Mid] [Norm Mid] {n m p : ℕ} {c1 : Component State1 Input Mid n m}
  {c1' : Component State1' Input Mid n m} {c2 : Component State2 Mid Output m p}
  {c2' : Component State2' Mid Output m p} {s1 : State1} {s1' : State1'} {s2 : State2}
  {s2' : State2'} (h1 : InformationSystem.equivalent c1 c1' s1 s1')
  (h2 : InformationSystem.equivalent c2 c2' s2 s2') :
  InformationSystem.equivalent (c1.sequential c2) (c1'.sequential c2') (s1, s2) (s1', s2')

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output]
    {State1 State2 State1' State2' Mid} [Nonempty State1] [Norm State1] [Nonempty State2]
    [Norm State2] [Nonempty State1'] [Norm State1'] [Nonempty State2'] [Norm State2'] [Nonempty Mid]
    [Norm Mid] {n m p} {c1} {c1'} {c2} {c2'} {s1} {s1'} {s2} {s2'} h1 h2 is =>
  List.rec (motive := fun is =>
    ∀ {s1 : State1} {s1' : State1'} {s2 : State2} {s2' : State2'},
      InformationSystem.equivalent c1 c1' s1 s1' →
        InformationSystem.equivalent c2 c2' s2 s2' →
          (InformationSystem.eval (c1.sequential c2) (s1, s2) is).2 =
            (InformationSystem.eval (c1'.sequential c2') (s1', s2') is).2)
    (fun {s1} {s1'} {s2} {s2'} h1 h2 =>
      Eq.refl (InformationSystem.eval (c1.sequential c2) (s1, s2) []).2)
    (fun i is ih {s1} {s1'} {s2} {s2'} h1 h2 =>
      have e1 := InformationSystem.equivalent_output h1 i;
      have hstep1 := rfl;
      have hstep2 := rfl;
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg (InformationSystem.eval (c1.sequential c2))
                          (congrArg Prod.fst hstep1))
                        is)))
                  (congr (congrArg List.cons (congrArg Prod.snd hstep1))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg (InformationSystem.eval (c1.sequential c2))
                          (congrArg Prod.fst hstep1))
                        is))))))
            (congrArg Prod.snd
              (congr
                (congrArg Prod.mk
                  (congrArg Prod.fst
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1'.sequential c2'))
                        (congrArg Prod.fst hstep2))
                      is)))
                (congr (congrArg List.cons (congrArg Prod.snd hstep2))
                  (congrArg Prod.snd
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1'.sequential c2'))
                        (congrArg Prod.fst hstep2))
                      is)))))))
        (have hhead :=
          Eq.mpr
            (id (congrArg (fun _a => (c2.step s2 _a).2 = (c2'.step s2' (c1'.step s1' i).2).2) e1))
            (InformationSystem.equivalent_output h2 (c1'.step s1' i).2);
        have hnext2 :=
          Eq.mpr
            (id
              (congrArg
                (fun _a =>
                  InformationSystem.equivalent c2 c2' (c2.step s2 _a).1
                    (c2'.step s2' (c1'.step s1' i).2).1)
                e1))
            (InformationSystem.equivalent_step h2 (c1'.step s1' i).2);
        id
          (Eq.mpr
            (id
              (congrArg
                (fun _a =>
                  _a ::
                      (InformationSystem.eval (c1.sequential c2)
                          ((c1.step s1 i).1, (c2.step s2 (c1.step s1 i).2).1) is).2 =
                    (c2'.step s2' (c1'.step s1' i).2).2 ::
                      (InformationSystem.eval (c1'.sequential c2')
                          ((c1'.step s1' i).1, (c2'.step s2' (c1'.step s1' i).2).1) is).2)
                hhead))
            (congrArg (List.cons (c2'.step s2' (c1'.step s1' i).2).2)
              (ih (InformationSystem.equivalent_step h1 i) hnext2)))))
    is h1 h2

Complexity: 35804 (size of the value term)

Dependencies: Component, Component.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, Prod, congr, congrArg, congrFun', id, rfl

Used by: Component.Hom.comp

TipComponent.parallel_congr

theorem Component.parallel_congr {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 State2 State1' State2' : Type} [Nonempty State1]
  [Norm State1] [Nonempty State2] [Norm State2] [Nonempty State1'] [Norm State1'] [Nonempty State2']
  [Norm State2'] {n1 m1 n2 m2 : ℕ} {c1 : Component State1 Input Output n1 m1}
  {c1' : Component State1' Input Output n1 m1} {c2 : Component State2 Input Output n2 m2}
  {c2' : Component State2' Input Output n2 m2} {s1 : State1} {s1' : State1'} {s2 : State2}
  {s2' : State2'} (h1 : InformationSystem.equivalent c1 c1' s1 s1')
  (h2 : InformationSystem.equivalent c2 c2' s2 s2') :
  InformationSystem.equivalent (c1.parallel c2) (c1'.parallel c2') (s1, s2) (s1', s2')

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output]
    {State1 State2 State1' State2'} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    [Nonempty State1'] [Norm State1'] [Nonempty State2'] [Norm State2'] {n1 m1 n2 m2} {c1} {c1'}
    {c2} {c2'} {s1} {s1'} {s2} {s2'} h1 h2 is =>
  List.rec (motive := fun is =>
    ∀ {s1 : State1} {s1' : State1'} {s2 : State2} {s2' : State2'},
      InformationSystem.equivalent c1 c1' s1 s1' →
        InformationSystem.equivalent c2 c2' s2 s2' →
          (InformationSystem.eval (c1.parallel c2) (s1, s2) is).2 =
            (InformationSystem.eval (c1'.parallel c2') (s1', s2') is).2)
    (fun {s1} {s1'} {s2} {s2'} h1 h2 =>
      Eq.refl (InformationSystem.eval (c1.parallel c2) (s1, s2) []).2)
    (fun iv is ih {s1} {s1'} {s2} {s2'} h1 h2 =>
      have e1 := InformationSystem.equivalent_output h1 fun k => iv (Fin.castAdd n2 k);
      have e2 := InformationSystem.equivalent_output h2 fun k => iv (Fin.natAdd n1 k);
      have hnext1 := InformationSystem.equivalent_step h1 fun k => iv (Fin.castAdd n2 k);
      have hnext2 := InformationSystem.equivalent_step h2 fun k => iv (Fin.natAdd n1 k);
      id
        (have hhead :=
          id
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    Fin.append _a (c2.step s2 fun k => iv (Fin.natAdd n1 k)).2 =
                      Fin.append (c1'.step s1' fun k => iv (Fin.castAdd n2 k)).2
                        (c2'.step s2' fun k => iv (Fin.natAdd n1 k)).2)
                  e1))
              (Eq.mpr
                (id
                  (congrArg
                    (fun _a =>
                      Fin.append (c1'.step s1' fun k => iv (Fin.castAdd n2 k)).2 _a =
                        Fin.append (c1'.step s1' fun k => iv (Fin.castAdd n2 k)).2
                          (c2'.step s2' fun k => iv (Fin.natAdd n1 k)).2)
                    e2))
                (Eq.refl
                  (Fin.append (c1'.step s1' fun k => iv (Fin.castAdd n2 k)).2
                    (c2'.step s2' fun k => iv (Fin.natAdd n1 k)).2))));
        Eq.mpr
          (id
            (congrArg
              (fun _a =>
                _a ::
                    (InformationSystem.eval (c1.parallel c2)
                        ((c1.step s1 fun k => iv (Fin.castAdd n2 k)).1,
                          (c2.step s2 fun k => iv (Fin.natAdd n1 k)).1)
                        is).2 =
                  ((c1'.parallel c2').step (s1', s2') iv).2 ::
                    (InformationSystem.eval (c1'.parallel c2')
                        ((c1'.step s1' fun k => iv (Fin.castAdd n2 k)).1,
                          (c2'.step s2' fun k => iv (Fin.natAdd n1 k)).1)
                        is).2)
              hhead))
          (congrArg (List.cons ((c1'.parallel c2').step (s1', s2') iv).2) (ih hnext1 hnext2))))
    is h1 h2

Complexity: 17756 (size of the value term)

Dependencies: Component, Component.parallel, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval

Mathlib dependencies: Fin.append, Norm

Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, congrArg, id

Used by: Component.Hom.tensor, Component.monoidalCategory

NoteComponent.recast

abbrev Component.recast {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output]
  [Norm Output] {State : Type} [Nonempty State] [Norm State] {n n' m m' : ℕ} (hn : n = n')
  (hm : m = m') (c : Component State Input Output n m) : Component State Input Output n' m'

Show details

| Component.recast hn hm c =
  {
    step := fun s iv =>
      match c.step s (iv ∘ Fin.cast hn) with
      | (s', ov) => (s', ov ∘ Fin.cast ⋯),
    conserves := ⋯ }

Complexity: 327 (size of the value term)

Outer dependencies: Component

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Prod.mk.eta, Real

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.cast, Fin.cast_refl, Function.comp, Nat, Nonempty, Prod, congr, congrArg, id

Used by: Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.recast, Component.Hom.recast_recast, Component.Hom.tensor_assoc, Component.Hom.tensor_empty, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Component.recast_congr, Component.recast_parallel_left, Component.recast_parallel_right, Component.recast_recast

TipComponent.recast_congr

theorem Component.recast_congr {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 State2 : Type} [Nonempty State1] [Norm State1]
  [Nonempty State2] [Norm State2] {n n' m m' : ℕ} (hn : n = n') (hm : m = m')
  {c1 : Component State1 Input Output n m} {c2 : Component State2 Input Output n m} {s1 : State1}
  {s2 : State2} (h : InformationSystem.equivalent c1 c2 s1 s2) :
  InformationSystem.equivalent (Component.recast hn hm c1) (Component.recast hn hm c2) s1 s2

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1 State2}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n n' m m'} hn hm {c1} {c2} {s1}
    {s2} h =>
  hn ▸
    hm ▸ fun is =>
      List.rec (motive := fun is =>
        ∀ {s1 : State1} {s2 : State2},
          InformationSystem.equivalent c1 c2 s1 s2 →
            (InformationSystem.eval (Component.recast (Eq.refl n) (Eq.refl m) c1) s1 is).2 =
              (InformationSystem.eval (Component.recast (Eq.refl n) (Eq.refl m) c2) s2 is).2)
        (fun {s1} {s2} h =>
          Eq.refl (InformationSystem.eval (Component.recast (Eq.refl n) (Eq.refl m) c1) s1 []).2)
        (fun i is ih {s1} {s2} h =>
          have e1 := InformationSystem.equivalent_output h i;
          id
            (have hhead := id e1;
            Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    _a ::
                        (InformationSystem.eval (Component.recast rfl rfl c1)
                            ((Component.recast rfl rfl c1).step s1 i).1 is).2 =
                      ((Component.recast rfl rfl c2).step s2 i).2 ::
                        (InformationSystem.eval (Component.recast rfl rfl c2)
                            ((Component.recast rfl rfl c2).step s2 i).1 is).2)
                  hhead))
              (congrArg (List.cons ((Component.recast rfl rfl c2).step s2 i).2)
                (ih (InformationSystem.equivalent_step h i)))))
        is h

Complexity: 6677 (size of the value term)

Dependencies: Component, Component.recast, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Proof dependencies: InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, congrArg, id, rfl

Used by: Component.Hom.recast

TipComponent.parallel_assoc

theorem Component.parallel_assoc {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 State2 State3 : Type} [Nonempty State1] [Norm State1]
  [Nonempty State2] [Norm State2] [Nonempty State3] [Norm State3] {n1 m1 n2 m2 n3 m3 : ℕ}
  (c1 : Component State1 Input Output n1 m1) (c2 : Component State2 Input Output n2 m2)
  (c3 : Component State3 Input Output n3 m3) (s1 : State1) (s2 : State2) (s3 : State3) :
  InformationSystem.equivalent (Component.recast ⋯ ⋯ ((c1.parallel c2).parallel c3))
    (c1.parallel (c2.parallel c3)) ((s1, s2), s3) (s1, s2, s3)

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output]
    {State1 State2 State3} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    [Nonempty State3] [Norm State3] {n1 m1 n2 m2 n3 m3} c1 c2 c3 s1 s2 s3 =>
  have he := fun iv =>
    ⟨funext fun k =>
        (fun a a_1 e_a => e_a ▸ Eq.refl (iv a))
          (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.castAdd n3 (Fin.castAdd n2 k)))
          (Fin.castAdd (n2 + n3) k)
          (Eq.refl (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.castAdd n3 (Fin.castAdd n2 k)))),
      ⟨funext fun k =>
          (fun a a_1 e_a => e_a ▸ Eq.refl (iv a))
            (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.castAdd n3 (Fin.natAdd n1 k)))
            (Fin.natAdd n1 (Fin.castAdd n3 k))
            (Eq.refl (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.castAdd n3 (Fin.natAdd n1 k)))),
        funext fun k =>
          (fun a a_1 e_a => e_a ▸ Eq.refl (iv a))
            (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.natAdd (n1 + n2) k))
            (Fin.natAdd n1 (Fin.natAdd n2 k))
            (Fin.ext
              (id (Decidable.byContradiction fun a => Component.parallel_assoc._proof_1_1 k a)))⟩⟩;
  have hstep1 := fun s1 s2 s3 iv =>
    And.casesOn (he iv) fun e1 right =>
      And.casesOn right fun e2 e3 =>
        Eq.refl
            (Component.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
              ((c1.parallel c2).parallel c3)) ▸
          id
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    ((((c1.1 s1 _a).1,
                            (c2.1 s2 fun k =>
                                iv
                                  (Fin.cast (Nat.add_assoc n1 n2 n3)
                                    (Fin.castAdd n3 (Fin.natAdd n1 k)))).1),
                          (c3.1 s3 fun k =>
                              iv (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.natAdd (n1 + n2) k))).1),
                        Fin.append
                            (Fin.append (c1.1 s1 _a).2
                              (c2.1 s2 fun k =>
                                  iv
                                    (Fin.cast (Nat.add_assoc n1 n2 n3)
                                      (Fin.castAdd n3 (Fin.natAdd n1 k)))).2)
                            (c3.1 s3 fun k =>
                                iv (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.natAdd (n1 + n2) k))).2 ∘
                          Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3))) =
                      ((((c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                            (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                          (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1),
                        Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                          (Fin.append (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                            (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2)))
                  e1))
              (Eq.mpr
                (id
                  (congrArg
                    (fun _a =>
                      ((((c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1, (c2.1 s2 _a).1),
                            (c3.1 s3 fun k =>
                                iv (Fin.cast (Nat.add_assoc n1 n2 n3) (Fin.natAdd (n1 + n2) k))).1),
                          Fin.append
                              (Fin.append (c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                                (c2.1 s2 _a).2)
                              (c3.1 s3 fun k =>
                                  iv
                                    (Fin.cast (Nat.add_assoc n1 n2 n3)
                                      (Fin.natAdd (n1 + n2) k))).2 ∘
                            Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3))) =
                        ((((c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                              (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                            (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1),
                          Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                            (Fin.append
                              (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                              (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2)))
                    e2))
                (Eq.mpr
                  (id
                    (congrArg
                      (fun _a =>
                        ((((c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                                (c2.1 s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                              (c3.1 s3 _a).1),
                            Fin.append
                                (Fin.append (c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                                  (c2.1 s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2)
                                (c3.1 s3 _a).2 ∘
                              Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3))) =
                          ((((c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                                (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                              (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1),
                            Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                              (Fin.append
                                (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                                (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2)))
                      e3))
                  (have happend :=
                    Fin.append_assoc (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                      (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                      (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2;
                  Eq.mpr
                    (id
                      (congrArg
                        (fun _a =>
                          ((((c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                                  (c2.1 s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                                (c3.1 s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1),
                              _a ∘ Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3))) =
                            ((((c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                                  (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                                (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1),
                              Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                                (Fin.append
                                  (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                                  (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2)))
                        happend))
                    ((fun {α β} fst fst_1 e_fst =>
                        Eq.rec (motive := fun fst_2 e_fst =>
                          ∀ (snd snd_1 : β), snd = snd_1 → (fst, snd) = (fst_2, snd_1))
                          (fun snd snd_1 e_snd => e_snd ▸ Eq.refl (fst, snd)) e_fst)
                      (((c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                          (c2.1 s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                        (c3.1 s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1)
                      (((c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                          (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                        (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1)
                      (Eq.refl
                        (((c1.1 s1 fun k => iv (Fin.castAdd (n2 + n3) k)).1,
                            (c2.1 s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).1),
                          (c3.1 s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).1))
                      ((Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                            (Fin.append
                              (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                              (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2) ∘
                          Fin.cast (Nat.add_assoc m1 m2 m3)) ∘
                        Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3)))
                      (Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                        (Fin.append (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                          (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2))
                      (Eq.refl
                        ((Fin.append (c1.step s1 fun k => iv (Fin.castAdd (n2 + n3) k)).2
                              (Fin.append
                                (c2.step s2 fun k => iv (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                                (c3.step s3 fun k => iv (Fin.natAdd n1 (Fin.natAdd n2 k))).2) ∘
                            Fin.cast (Nat.add_assoc m1 m2 m3)) ∘
                          Fin.cast (Eq.symm (Nat.add_assoc m1 m2 m3)))))))));
  have hstep2 := fun s1 s2 s3 iv => Eq.refl ((c1.parallel (c2.parallel c3)).step (s1, s2, s3) iv);
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s1 : State1) (s2 : State2) (s3 : State3),
      (InformationSystem.eval
            (Component.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
              ((c1.parallel c2).parallel c3))
            ((s1, s2), s3) is).2 =
        (InformationSystem.eval (c1.parallel (c2.parallel c3)) (s1, s2, s3) is).2)
    (fun s1 s2 s3 =>
      Eq.refl
        (InformationSystem.eval
            (Component.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
              ((c1.parallel c2).parallel c3))
            ((s1, s2), s3) []).2)
    (fun i is ih s1 s2 s3 =>
      have h1 := hstep1 s1 s2 s3 i;
      have h2 := hstep2 s1 s2 s3 i;
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg
                          (InformationSystem.eval
                            (Component.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
                              ((c1.parallel c2).parallel c3)))
                          (congrArg Prod.fst h1))
                        is)))
                  (congr (congrArg List.cons (congrArg Prod.snd h1))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg
                          (InformationSystem.eval
                            (Component.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
                              ((c1.parallel c2).parallel c3)))
                          (congrArg Prod.fst h1))
                        is))))))
            (congrArg Prod.snd
              (congr
                (congrArg Prod.mk
                  (congrArg Prod.fst
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1.parallel (c2.parallel c3)))
                        (congrArg Prod.fst h2))
                      is)))
                (congr (congrArg List.cons (congrArg Prod.snd h2))
                  (congrArg Prod.snd
                    (congrFun'
                      (congrArg (InformationSystem.eval (c1.parallel (c2.parallel c3)))
                        (congrArg Prod.fst h2))
                      is)))))))
        (congrArg
          (List.cons
            (Fin.append (c1.step s1 fun k => i (Fin.castAdd (n2 + n3) k)).2
              (Fin.append (c2.step s2 fun k => i (Fin.natAdd n1 (Fin.castAdd n3 k))).2
                (c3.step s3 fun k => i (Fin.natAdd n1 (Fin.natAdd n2 k))).2)))
          (ih (c1.step s1 fun k => i (Fin.castAdd (n2 + n3) k)).1
            (c2.step s2 fun k => i (Fin.natAdd n1 (Fin.castAdd n3 k))).1
            (c3.step s3 fun k => i (Fin.natAdd n1 (Fin.natAdd n2 k))).1)))
    is s1 s2 s3

Complexity: 126702 (size of the value term)

Dependencies: Component, Component.parallel, Component.recast, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_assoc, Norm

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, False, Fin, Fin.cast, Fin.castAdd, Fin.ext, Fin.natAdd, Function.comp, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.tidy_sat, List, Nat, Nat.add_assoc, Nat.cast, Nat.lt_or_gt_of_ne, Nonempty, Not, Or.elim, Prod, congr, congrArg, congrFun', funext, id, le_of_le_of_eq, of_decide_eq_true

Used by: Component.Hom.tensor_assoc

NoteComponent.empty

abbrev Component.empty (Input Output : Type) [Nonempty Input] [Norm Input] [Nonempty Output]
  [Norm Output] : Component Unit Input Output 0 0

Show details

| Component.empty Input Output = { step := fun x x_1 => ((), Fin.elim0), conserves := ⋯ }

Complexity: 153 (size of the value term)

Outer dependencies: Component, instNormUnit_computerNetworks

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Finset, Finset.sum_congr, Finset.univ, Finset.univ_eq_empty, Norm, Real, add_zero

Lean core dependencies: Eq, Eq.trans, Fin, Fin.elim0, Nat, Nonempty, Prod, True, Unit, Unit.unit, congr, congrArg, eq_self, of_eq_true

Used by: Component.Hom.tensorUnit, Component.empty_parallel, Component.monoidalCategory, Component.parallel_empty

TipComponent.parallel_empty

theorem Component.parallel_empty {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {n m : ℕ}
  (c : Component State1 Input Output n m) (s : State1) :
  InformationSystem.equivalent (c.parallel (Component.empty Input Output)) c (s, ()) s

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1}
    [Nonempty State1] [Norm State1] {n m} c s =>
  have hstep := fun s iv =>
    id
      ((fun {α β} fst fst_1 e_fst =>
          Eq.rec (motive := fun fst_2 e_fst =>
            ∀ (snd snd_1 : β), snd = snd_1 → (fst, snd) = (fst_2, snd_1))
            (fun snd snd_1 e_snd => e_snd ▸ Eq.refl (fst, snd)) e_fst)
        ((c.1 s fun k => iv (Fin.castAdd 0 k)).1, ())
        ((c.step s fun k => iv (Fin.castAdd 0 k)).1, ())
        (Eq.refl ((c.1 s fun k => iv (Fin.castAdd 0 k)).1, ()))
        (Fin.append (c.1 s fun k => iv (Fin.castAdd 0 k)).2 Fin.elim0)
        (c.step s fun k => iv (Fin.castAdd 0 k)).2
        (of_eq_true
          (Eq.trans
            (congrFun'
              (congrArg Eq
                (Eq.trans (Fin.append_elim0 (c.1 s fun k => iv k).2)
                  (Eq.trans
                    (congrArg (Function.comp (c.1 s fun k => iv k).2)
                      (Fin.cast_refl m (Nat.add_zero m)))
                    CompTriple.comp_eq)))
              (c.step s fun k => iv k).2)
            (eq_self (c.1 s fun k => iv k).2))));
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s : State1),
      (InformationSystem.eval (c.parallel (Component.empty Input Output)) (s, ()) is).2 =
        (InformationSystem.eval c s is).2)
    (fun s =>
      Eq.refl (InformationSystem.eval (c.parallel (Component.empty Input Output)) (s, ()) []).2)
    (fun i is ih s =>
      id
        (Eq.mpr
          (id
            (congrFun'
              (congrArg Eq
                (congrArg Prod.snd
                  (congr
                    (congrArg Prod.mk
                      (congrArg Prod.fst
                        (congrFun'
                          (congrArg
                            (InformationSystem.eval (c.parallel (Component.empty Input Output)))
                            (congrArg Prod.fst ((fun s iv => hstep s iv) s i)))
                          is)))
                    (congr (congrArg List.cons (congrArg Prod.snd ((fun s iv => hstep s iv) s i)))
                      (congrArg Prod.snd
                        (congrFun'
                          (congrArg
                            (InformationSystem.eval (c.parallel (Component.empty Input Output)))
                            (congrArg Prod.fst ((fun s iv => hstep s iv) s i)))
                          is))))))
              ((c.1 s i).2 :: (InformationSystem.eval c (c.1 s i).1 is).2)))
          (congrArg (List.cons (c.step s fun k => i (Fin.castAdd 0 k)).2)
            (ih (c.step s fun k => i (Fin.castAdd 0 k)).1))))
    is s

Complexity: 23097 (size of the value term)

Dependencies: Component, Component.empty, Component.parallel, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_elim0, Norm

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Fin, Fin.cast, Fin.castAdd, Fin.cast_refl, Fin.elim0, Function.comp, List, Nat, Nat.add_zero, Nonempty, Prod, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, id, of_eq_true

Used by: Component.monoidalCategory

TipComponent.empty_parallel

theorem Component.empty_parallel {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {n m : ℕ}
  (c : Component State1 Input Output n m) (s : State1) :
  InformationSystem.equivalent (Component.recast ⋯ ⋯ ((Component.empty Input Output).parallel c)) c
    ((), s) s

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1}
    [Nonempty State1] [Norm State1] {n m} c s =>
  have hstep := fun s iv =>
    Eq.refl
        (Component.recast (Nat.zero_add n) (Nat.zero_add m)
          ((Component.empty Input Output).parallel c)) ▸
      have hin :=
        funext fun k =>
          (fun a a_1 e_a => e_a ▸ Eq.refl (iv a)) (Fin.cast (Nat.zero_add n) (Fin.natAdd 0 k)) k
            (Fin.ext
              (of_eq_true
                (Eq.trans
                  (congrFun'
                    (congrArg Eq
                      (congrArg Fin.val
                        (Fin.cast.congr_simp (Nat.zero_add n) (Fin.natAdd 0 k)
                          ⟨↑k, zero_add ↑k ▸ Fin.natAdd._proof_1 0 k⟩
                          (Fin.mk.congr_simp (0 + ↑k) (↑k) (zero_add ↑k)
                            (Fin.natAdd._proof_1 0 k)))))
                    ↑k)
                  (eq_self ↑k))));
      id
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (((), (c.1 s _a).1),
                    Fin.append Fin.elim0 (c.1 s _a).2 ∘ Fin.cast (Eq.symm (Nat.zero_add m))) =
                  (((), (c.step s iv).1), (c.step s iv).2))
              hin))
          (have happend := Fin.append_left_nil Fin.elim0 (c.step s iv).2 rfl;
          Eq.mpr
            (id
              (congrArg
                (fun _a =>
                  (((), (c.1 s iv).1), _a ∘ Fin.cast (Eq.symm (Nat.zero_add m))) =
                    (((), (c.step s iv).1), (c.step s iv).2))
                happend))
            ((fun {α β} fst fst_1 e_fst =>
                Eq.rec (motive := fun fst_2 e_fst =>
                  ∀ (snd snd_1 : β), snd = snd_1 → (fst, snd) = (fst_2, snd_1))
                  (fun snd snd_1 e_snd => e_snd ▸ Eq.refl (fst, snd)) e_fst)
              ((), (c.1 s iv).1) ((), (c.step s iv).1) (Eq.refl ((), (c.1 s iv).1))
              (((c.step s iv).2 ∘ Fin.cast (Fin.append_left_nil._proof_1 rfl)) ∘
                Fin.cast (Eq.symm (Nat.zero_add m)))
              (c.step s iv).2
              (Eq.refl
                (((c.step s iv).2 ∘ Fin.cast (Fin.append_left_nil._proof_1 rfl)) ∘
                  Fin.cast (Eq.symm (Nat.zero_add m)))))));
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s : State1),
      (InformationSystem.eval
            (Component.recast (Nat.zero_add n) (Nat.zero_add m)
              ((Component.empty Input Output).parallel c))
            ((), s) is).2 =
        (InformationSystem.eval c s is).2)
    (fun s =>
      Eq.refl
        (InformationSystem.eval
            (Component.recast (Nat.zero_add n) (Nat.zero_add m)
              ((Component.empty Input Output).parallel c))
            ((), s) []).2)
    (fun i is ih s =>
      Eq.mpr
        (id
          (congrFun'
            (congrArg Eq
              (congrArg Prod.snd
                (congr
                  (congrArg Prod.mk
                    (congrArg Prod.fst
                      (congrFun'
                        (congrArg
                          (InformationSystem.eval
                            (Component.recast (Nat.zero_add n) (Nat.zero_add m)
                              ((Component.empty Input Output).parallel c)))
                          (congrArg Prod.fst ((fun s iv => hstep s iv) s i)))
                        is)))
                  (congr (congrArg List.cons (congrArg Prod.snd ((fun s iv => hstep s iv) s i)))
                    (congrArg Prod.snd
                      (congrFun'
                        (congrArg
                          (InformationSystem.eval
                            (Component.recast (Nat.zero_add n) (Nat.zero_add m)
                              ((Component.empty Input Output).parallel c)))
                          (congrArg Prod.fst ((fun s iv => hstep s iv) s i)))
                        is))))))
            ((c.1 s i).2 :: (InformationSystem.eval c (c.1 s i).1 is).2)))
        (congrArg (List.cons (c.step s i).2) (ih (c.step s i).1)))
    is s

Complexity: 24716 (size of the value term)

Dependencies: Component, Component.empty, Component.parallel, Component.recast, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_left_nil, Norm, zero_add

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.cast, Fin.elim0, Fin.ext, Fin.natAdd, Function.comp, List, Nat, Nat.zero_add, Nonempty, Prod, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true, rfl

Used by: Component.Hom.tensor_empty

TipComponent.parallel_comm

theorem Component.parallel_comm {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {State2 : Type}
  [Nonempty State2] [Norm State2] {n1 m1 n2 m2 : ℕ} (c1 : Component State1 Input Output n1 m1)
  (c2 : Component State2 Input Output n2 m2) (s1 : State1) (s2 : State2) :
  InformationSystem.equivalent (c1.parallel c2)
    (((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).sequential
      (Component.symmetry Output m2 m1))
    (s1, s2) (((), s2, s1), ())

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1}
    [Nonempty State1] [Norm State1] {State2} [Nonempty State2] [Norm State2] {n1 m1 n2 m2} c1 c2 s1
    s2 =>
  have hstep := fun s1 s2 iv =>
    Eq.refl
        (((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).sequential
          (Component.symmetry Output m2 m1)) ▸
      of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Eq
              (congrFun'
                (congrFun'
                  (congrArg InformationSystem.step
                    (InformationSystem.mk.congr_simp
                      (fun p i =>
                        match
                          ((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).step p.1
                            i with
                        | (s1', mv) =>
                          match (Component.symmetry Output m2 m1).step p.2 mv with
                          | (s2', ov) => ((s1', s2'), ov))
                      (fun p i =>
                        ((((), (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).1,
                              (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).1),
                            ()),
                          Fin.append (fun k => (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).2 k)
                            fun k => (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).2 k))
                      (funext fun p =>
                        funext fun i =>
                          congr
                            (congrArg Prod.mk
                              (congr
                                (congrArg Prod.mk
                                  (congrArg Prod.fst
                                    (congrFun'
                                      (congrFun'
                                        (InformationSystem.mk.congr_simp
                                            (fun p i =>
                                              match (Component.symmetry Input n1 n2).step p.1 i with
                                              | (s1', mv) =>
                                                match (c2.parallel c1).step p.2 mv with
                                                | (s2', ov) => ((s1', s2'), ov))
                                            (fun p i =>
                                              (((), (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).1,
                                                  (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).1),
                                                Fin.append
                                                  (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).2
                                                  (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).2))
                                            (funext fun p =>
                                              funext fun i =>
                                                congr
                                                  (congrArg Prod.mk
                                                    (congrArg (Prod.mk ())
                                                      (congrArg Prod.fst
                                                        (congr
                                                          (congrArg Prod.mk
                                                            (congr
                                                              (congrArg Prod.mk
                                                                (congrArg Prod.fst
                                                                  (congrArg (c2.1 p.2.1)
                                                                    (funext fun k =>
                                                                      Fin.append_left
                                                                        (fun k =>
                                                                          i (Fin.natAdd n1 k))
                                                                        (fun k =>
                                                                          i (Fin.castAdd n2 k))
                                                                        k))))
                                                              (congrArg Prod.fst
                                                                (congrArg (c1.1 p.2.2)
                                                                  (funext fun k =>
                                                                    Fin.append_right
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k)))))
                                                          (congr
                                                            (congrArg Fin.append
                                                              (congrArg Prod.snd
                                                                (congrArg (c2.1 p.2.1)
                                                                  (funext fun k =>
                                                                    Fin.append_left
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k))))
                                                            (congrArg Prod.snd
                                                              (congrArg (c1.1 p.2.2)
                                                                (funext fun k =>
                                                                  Fin.append_right
                                                                    (fun k => i (Fin.natAdd n1 k))
                                                                    (fun k => i (Fin.castAdd n2 k))
                                                                    k))))))))
                                                  (congrArg Prod.snd
                                                    (congr
                                                      (congrArg Prod.mk
                                                        (congr
                                                          (congrArg Prod.mk
                                                            (congrArg Prod.fst
                                                              (congrArg (c2.1 p.2.1)
                                                                (funext fun k =>
                                                                  Fin.append_left
                                                                    (fun k => i (Fin.natAdd n1 k))
                                                                    (fun k => i (Fin.castAdd n2 k))
                                                                    k))))
                                                          (congrArg Prod.fst
                                                            (congrArg (c1.1 p.2.2)
                                                              (funext fun k =>
                                                                Fin.append_right
                                                                  (fun k => i (Fin.natAdd n1 k))
                                                                  (fun k => i (Fin.castAdd n2 k))
                                                                  k)))))
                                                      (congr
                                                        (congrArg Fin.append
                                                          (congrArg Prod.snd
                                                            (congrArg (c2.1 p.2.1)
                                                              (funext fun k =>
                                                                Fin.append_left
                                                                  (fun k => i (Fin.natAdd n1 k))
                                                                  (fun k => i (Fin.castAdd n2 k))
                                                                  k))))
                                                        (congrArg Prod.snd
                                                          (congrArg (c1.1 p.2.2)
                                                            (funext fun k =>
                                                              Fin.append_right
                                                                (fun k => i (Fin.natAdd n1 k))
                                                                (fun k => i (Fin.castAdd n2 k))
                                                                k)))))))
                                            (Component.sequential._proof_1
                                              (Component.symmetry Input n1 n2) (c2.parallel c1)) ▸
                                          Eq.refl
                                            ((Component.symmetry Input n1 n2).sequential
                                                (c2.parallel c1)).1)
                                        p.1)
                                      i)))
                                (congrArg Prod.fst
                                  (Eq.trans
                                    (congrArg
                                      ((fun x iv =>
                                          ((),
                                            Fin.append (fun k => iv (Fin.natAdd m2 k)) fun k =>
                                              iv (Fin.castAdd m1 k)))
                                        p.2)
                                      (congrArg Prod.snd
                                        (congrFun'
                                          (congrFun'
                                            (InformationSystem.mk.congr_simp
                                                (fun p i =>
                                                  match
                                                    (Component.symmetry Input n1 n2).step p.1 i with
                                                  | (s1', mv) =>
                                                    match (c2.parallel c1).step p.2 mv with
                                                    | (s2', ov) => ((s1', s2'), ov))
                                                (fun p i =>
                                                  (((), (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).1,
                                                      (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).1),
                                                    Fin.append
                                                      (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).2
                                                      (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).2))
                                                (funext fun p =>
                                                  funext fun i =>
                                                    congr
                                                      (congrArg Prod.mk
                                                        (congrArg (Prod.mk ())
                                                          (congrArg Prod.fst
                                                            (congr
                                                              (congrArg Prod.mk
                                                                (congr
                                                                  (congrArg Prod.mk
                                                                    (congrArg Prod.fst
                                                                      (congrArg (c2.1 p.2.1)
                                                                        (funext fun k =>
                                                                          Fin.append_left
                                                                            (fun k =>
                                                                              i (Fin.natAdd n1 k))
                                                                            (fun k =>
                                                                              i (Fin.castAdd n2 k))
                                                                            k))))
                                                                  (congrArg Prod.fst
                                                                    (congrArg (c1.1 p.2.2)
                                                                      (funext fun k =>
                                                                        Fin.append_right
                                                                          (fun k =>
                                                                            i (Fin.natAdd n1 k))
                                                                          (fun k =>
                                                                            i (Fin.castAdd n2 k))
                                                                          k)))))
                                                              (congr
                                                                (congrArg Fin.append
                                                                  (congrArg Prod.snd
                                                                    (congrArg (c2.1 p.2.1)
                                                                      (funext fun k =>
                                                                        Fin.append_left
                                                                          (fun k =>
                                                                            i (Fin.natAdd n1 k))
                                                                          (fun k =>
                                                                            i (Fin.castAdd n2 k))
                                                                          k))))
                                                                (congrArg Prod.snd
                                                                  (congrArg (c1.1 p.2.2)
                                                                    (funext fun k =>
                                                                      Fin.append_right
                                                                        (fun k =>
                                                                          i (Fin.natAdd n1 k))
                                                                        (fun k =>
                                                                          i (Fin.castAdd n2 k))
                                                                        k))))))))
                                                      (congrArg Prod.snd
                                                        (congr
                                                          (congrArg Prod.mk
                                                            (congr
                                                              (congrArg Prod.mk
                                                                (congrArg Prod.fst
                                                                  (congrArg (c2.1 p.2.1)
                                                                    (funext fun k =>
                                                                      Fin.append_left
                                                                        (fun k =>
                                                                          i (Fin.natAdd n1 k))
                                                                        (fun k =>
                                                                          i (Fin.castAdd n2 k))
                                                                        k))))
                                                              (congrArg Prod.fst
                                                                (congrArg (c1.1 p.2.2)
                                                                  (funext fun k =>
                                                                    Fin.append_right
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k)))))
                                                          (congr
                                                            (congrArg Fin.append
                                                              (congrArg Prod.snd
                                                                (congrArg (c2.1 p.2.1)
                                                                  (funext fun k =>
                                                                    Fin.append_left
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k))))
                                                            (congrArg Prod.snd
                                                              (congrArg (c1.1 p.2.2)
                                                                (funext fun k =>
                                                                  Fin.append_right
                                                                    (fun k => i (Fin.natAdd n1 k))
                                                                    (fun k => i (Fin.castAdd n2 k))
                                                                    k)))))))
                                                (Component.sequential._proof_1
                                                  (Component.symmetry Input n1 n2)
                                                  (c2.parallel c1)) ▸
                                              Eq.refl
                                                ((Component.symmetry Input n1 n2).sequential
                                                    (c2.parallel c1)).1)
                                            p.1)
                                          i)))
                                    (congrArg (Prod.mk ())
                                      (congr
                                        (congrArg Fin.append
                                          (funext fun k =>
                                            Fin.append_right
                                              (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).2
                                              (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).2 k))
                                        (funext fun k =>
                                          Fin.append_left
                                            (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).2
                                            (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).2 k)))))))
                            (congrArg Prod.snd
                              (Eq.trans
                                (congrArg
                                  ((fun x iv =>
                                      ((),
                                        Fin.append (fun k => iv (Fin.natAdd m2 k)) fun k =>
                                          iv (Fin.castAdd m1 k)))
                                    p.2)
                                  (congrArg Prod.snd
                                    (congrFun'
                                      (congrFun'
                                        (InformationSystem.mk.congr_simp
                                            (fun p i =>
                                              match (Component.symmetry Input n1 n2).step p.1 i with
                                              | (s1', mv) =>
                                                match (c2.parallel c1).step p.2 mv with
                                                | (s2', ov) => ((s1', s2'), ov))
                                            (fun p i =>
                                              (((), (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).1,
                                                  (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).1),
                                                Fin.append
                                                  (c2.1 p.2.1 fun k => i (Fin.natAdd n1 k)).2
                                                  (c1.1 p.2.2 fun k => i (Fin.castAdd n2 k)).2))
                                            (funext fun p =>
                                              funext fun i =>
                                                congr
                                                  (congrArg Prod.mk
                                                    (congrArg (Prod.mk ())
                                                      (congrArg Prod.fst
                                                        (congr
                                                          (congrArg Prod.mk
                                                            (congr
                                                              (congrArg Prod.mk
                                                                (congrArg Prod.fst
                                                                  (congrArg (c2.1 p.2.1)
                                                                    (funext fun k =>
                                                                      Fin.append_left
                                                                        (fun k =>
                                                                          i (Fin.natAdd n1 k))
                                                                        (fun k =>
                                                                          i (Fin.castAdd n2 k))
                                                                        k))))
                                                              (congrArg Prod.fst
                                                                (congrArg (c1.1 p.2.2)
                                                                  (funext fun k =>
                                                                    Fin.append_right
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k)))))
                                                          (congr
                                                            (congrArg Fin.append
                                                              (congrArg Prod.snd
                                                                (congrArg (c2.1 p.2.1)
                                                                  (funext fun k =>
                                                                    Fin.append_left
                                                                      (fun k => i (Fin.natAdd n1 k))
                                                                      (fun k =>
                                                                        i (Fin.castAdd n2 k))
                                                                      k))))
                                                            (congrArg Prod.snd
                                                              (congrArg (c1.1 p.2.2)
                                                                (funext fun k =>
                                                                  Fin.append_right
                                                                    (fun k => i (Fin.natAdd n1 k))
                                                                    (fun k => i (Fin.castAdd n2 k))
                                                                    k))))))))
                                                  (congrArg Prod.snd
                                                    (congr
                                                      (congrArg Prod.mk
                                                        (congr
                                                          (congrArg Prod.mk
                                                            (congrArg Prod.fst
                                                              (congrArg (c2.1 p.2.1)
                                                                (funext fun k =>
                                                                  Fin.append_left
                                                                    (fun k => i (Fin.natAdd n1 k))
                                                                    (fun k => i (Fin.castAdd n2 k))
                                                                    k))))
                                                          (congrArg Prod.fst
                                                            (congrArg (c1.1 p.2.2)
                                                              (funext fun k =>
                                                                Fin.append_right
                                                                  (fun k => i (Fin.natAdd n1 k))
                                                                  (fun k => i (Fin.castAdd n2 k))
                                                                  k)))))
                                                      (congr
                                                        (congrArg Fin.append
                                                          (congrArg Prod.snd
                                                            (congrArg (c2.1 p.2.1)
                                                              (funext fun k =>
                                                                Fin.append_left
                                                                  (fun k => i (Fin.natAdd n1 k))
                                                                  (fun k => i (Fin.castAdd n2 k))
                                                                  k))))
                                                        (congrArg Prod.snd
                                                          (congrArg (c1.1 p.2.2)
                                                            (funext fun k =>
                                                              Fin.append_right
                                                                (fun k => i (Fin.natAdd n1 k))
                                                                (fun k => i (Fin.castAdd n2 k))
                                                                k)))))))
                                            (Component.sequential._proof_1
                                              (Component.symmetry Input n1 n2) (c2.parallel c1)) ▸
                                          Eq.refl
                                            ((Component.symmetry Input n1 n2).sequential
                                                (c2.parallel c1)).1)
                                        p.1)
                                      i)))
                                (congrArg (Prod.mk ())
                                  (congr
                                    (congrArg Fin.append
                                      (funext fun k =>
                                        Fin.append_right
                                          (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).2
                                          (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).2 k))
                                    (funext fun k =>
                                      Fin.append_left (c2.1 p.1.2.1 fun k => i (Fin.natAdd n1 k)).2
                                        (c1.1 p.1.2.2 fun k => i (Fin.castAdd n2 k)).2 k))))))
                      (Component.sequential._proof_1
                        ((Component.symmetry Input n1 n2).sequential (c2.parallel c1))
                        (Component.symmetry Output m2 m1))))
                  (((), s2, s1), ()))
                iv))
            ((((), (c2.step s2 fun k => iv (Fin.natAdd n1 k)).1,
                  (c1.step s1 fun k => iv (Fin.castAdd n2 k)).1),
                ()),
              Fin.append (c1.step s1 fun k => iv (Fin.castAdd n2 k)).2
                (c2.step s2 fun k => iv (Fin.natAdd n1 k)).2))
          (eq_self
            ((((), (c2.1 s2 fun k => iv (Fin.natAdd n1 k)).1,
                  (c1.1 s1 fun k => iv (Fin.castAdd n2 k)).1),
                ()),
              Fin.append (fun k => (c1.1 s1 fun k => iv (Fin.castAdd n2 k)).2 k) fun k =>
                (c2.1 s2 fun k => iv (Fin.natAdd n1 k)).2 k)));
  fun is =>
  List.rec (motive := fun is =>
    ∀ (s1 : State1) (s2 : State2),
      (InformationSystem.eval (c1.parallel c2) (s1, s2) is).2 =
        (InformationSystem.eval
            (((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).sequential
              (Component.symmetry Output m2 m1))
            (((), s2, s1), ()) is).2)
    (fun s1 s2 => Eq.refl (InformationSystem.eval (c1.parallel c2) (s1, s2) []).2)
    (fun i is ih s1 s2 =>
      have h := hstep s1 s2 i;
      Eq.mpr
        (id
          (congrArg
            (Eq
              (((c1.parallel c2).1 (s1, s2) i).2 ::
                (InformationSystem.eval (c1.parallel c2) ((c1.parallel c2).1 (s1, s2) i).1 is).2))
            (congrArg Prod.snd
              (congr
                (congrArg Prod.mk
                  (congrArg Prod.fst
                    (congrFun'
                      (congrArg
                        (InformationSystem.eval
                          (((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).sequential
                            (Component.symmetry Output m2 m1)))
                        (congrArg Prod.fst h))
                      is)))
                (congr (congrArg List.cons (congrArg Prod.snd h))
                  (congrArg Prod.snd
                    (congrFun'
                      (congrArg
                        (InformationSystem.eval
                          (((Component.symmetry Input n1 n2).sequential (c2.parallel c1)).sequential
                            (Component.symmetry Output m2 m1)))
                        (congrArg Prod.fst h))
                      is)))))))
        (congrArg (List.cons ((c1.parallel c2).1 (s1, s2) i).2)
          (ih (c1.step s1 fun k => i (Fin.castAdd n2 k)).1
            (c2.step s2 fun k => i (Fin.natAdd n1 k)).1)))
    is s1 s2

Complexity: 432531 (size of the value term)

Dependencies: Component, Component.parallel, Component.sequential, Component.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem, InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right, Norm, Real

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true

Used by: Component.Hom.tensor_comm

NoteInformationSystem.toSimplex

abbrev InformationSystem.toSimplex {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1]
  (sys : InformationSystem State1 Input Output) : Component.Simplex State1 Input Output

Show details

| sys.toSimplex =
  {
    step := fun s iv =>
      match sys.step s (iv 0) with
      | (s', o) => (s', fun x => o),
    conserves := ⋯ }

Complexity: 293 (size of the value term)

Outer dependencies: Component.Simplex, InformationSystem

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Fin.sum_univ_one, Finset.sum, Finset.univ, Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq

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

Used by: InformationSystem.parallel, InformationSystem.parallel_delta, InformationSystem.sequential, InformationSystem.sequential_delta

NoteComponent.Simplex.toInformationSystem

abbrev Component.Simplex.toInformationSystem {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1]
  (c : Component.Simplex State1 Input Output) : InformationSystem State1 Input Output

Show details

| c.toInformationSystem =
  {
    step := fun s i =>
      match c.step s fun x => i with
      | (s', ov) => (s', ov 0),
    conserves := ⋯ }

Complexity: 281 (size of the value term)

Outer dependencies: Component.Simplex, InformationSystem

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Fin.sum_univ_one, Finset.sum, Finset.univ, Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq

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

Used by: Channel.system, InformationSystem.sequential, InformationSystem.sequential_delta

NoteInformationSystem.sequential

abbrev InformationSystem.sequential {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {State2 : Type}
  [Nonempty State2] [Norm State2] {Mid : Type} [Nonempty Mid] [Norm Mid]
  (sys1 : InformationSystem State1 Input Mid) (sys2 : InformationSystem State2 Mid Output) :
  InformationSystem (State1 × State2) Input Output

Show details

| sys1.sequential sys2 =
  Component.Simplex.toInformationSystem (Component.sequential sys1.toSimplex sys2.toSimplex)

Complexity: 235 (size of the value term)

Outer dependencies: InformationSystem, instNormProd_computerNetworks

Inner dependencies: Component.Simplex.toInformationSystem, Component.sequential, InformationSystem.toSimplex

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Prod

Used by: InformationSystem.sequential_delta

ImportantInformationSystem.sequential_delta

theorem InformationSystem.sequential_delta {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {State2 : Type}
  [Nonempty State2] [Norm State2] {Mid : Type} [Nonempty Mid] [Norm Mid]
  (sys1 : InformationSystem State1 Input Mid) (sys2 : InformationSystem State2 Mid Output)
  (s1 : State1) (s2 : State2) (i : Input) :
  ((sys1.sequential sys2).stepAt (s1, s2) i).delta =
    (sys1.stepAt s1 i).delta + (sys2.stepAt s2 (sys1.step s1 i).2).delta

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1}
    [Nonempty State1] [Norm State1] {State2} [Nonempty State2] [Norm State2] {Mid} [Nonempty Mid]
    [Norm Mid] sys1 sys2 s1 s2 i =>
  id
    (id
      (id
        (id
          (id
            (id
              (of_eq_true
                (Eq.trans
                  (congrArg (Eq (‖i‖ - ‖(sys2.1 s2 (sys1.1 s1 i).2).2‖))
                    (sub_add_sub_cancel ‖i‖ ‖(sys1.step s1 i).2‖
                      ‖(sys2.step s2 (sys1.step s1 i).2).2‖))
                  (eq_self (‖i‖ - ‖(sys2.1 s2 (sys1.1 s1 i).2).2‖)))))))))

Complexity: 34189 (size of the value term)

Dependencies: InformationSystem, InformationSystem.Step.delta, InformationSystem.sequential, InformationSystem.stepAt, instNormProd_computerNetworks

Proof dependencies: Component.Simplex.toInformationSystem, Component.sequential, InformationSystem.toSimplex, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm, Real, sub_add_sub_cancel

Lean core dependencies: Eq, Eq.trans, Fin, Nat, Nonempty, Prod, True, congrArg, eq_self, id, of_eq_true

Used by: (none)

NoteInformationSystem.parallel

abbrev InformationSystem.parallel {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {State2 : Type}
  [Nonempty State2] [Norm State2] (sys1 : InformationSystem State1 Input Output)
  (sys2 : InformationSystem State2 Input Output) : Component (State1 × State2) Input Output 2 2

Show details

| sys1.parallel sys2 = Component.parallel sys1.toSimplex sys2.toSimplex

Complexity: 189 (size of the value term)

Outer dependencies: Component, InformationSystem, instNormProd_computerNetworks

Inner dependencies: Component.parallel, InformationSystem.toSimplex

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Prod

Used by: InformationSystem.parallel_delta

ImportantInformationSystem.parallel_delta

theorem InformationSystem.parallel_delta {Input : Type} [Nonempty Input] [Norm Input] {Output : Type}
  [Nonempty Output] [Norm Output] {State1 : Type} [Nonempty State1] [Norm State1] {State2 : Type}
  [Nonempty State2] [Norm State2] (sys1 : InformationSystem State1 Input Output)
  (sys2 : InformationSystem State2 Input Output) (s1 : State1) (s2 : State2) (iv : Fin 2 → Input) :
  (InformationSystem.stepAt (sys1.parallel sys2) (s1, s2) iv).delta =
    (sys1.stepAt s1 (iv 0)).delta + (sys2.stepAt s2 (iv 1)).delta

Show details

fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1}
    [Nonempty State1] [Norm State1] {State2} [Nonempty State2] [Norm State2] sys1 sys2 s1 s2 iv =>
  id
    (id
      (id
        (id
          (id
            (id
              (have hiv := Fin.sum_univ_two fun i => ‖iv i‖;
              have hout :=
                Eq.mpr
                  (id
                    (congrArg (fun _a => _a = ‖(sys1.step s1 (iv 0)).2‖ + ‖(sys2.step s2 (iv 1)).2‖)
                      (Fin.sum_univ_two fun i =>
                        ‖Fin.append (fun x => (sys1.step s1 (iv 0)).2)
                            (fun x => (sys2.step s2 (iv 1)).2) i‖)))
                  (Eq.refl
                    (‖Fin.append (fun x => (sys1.step s1 (iv 0)).2)
                          (fun x => (sys2.step s2 (iv 1)).2) 0‖ +
                      ‖Fin.append (fun x => (sys1.step s1 (iv 0)).2)
                          (fun x => (sys2.step s2 (iv 1)).2) 1‖));
              Eq.mpr
                (id
                  (congrArg
                    (fun _a =>
                      _a -
                          ∑ i,
                            ‖Fin.append (fun x => (sys1.step s1 (iv 0)).2)
                                (fun x => (sys2.step s2 (iv 1)).2) i‖ =
                        ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                  output := (sys1.step s1 (iv 0)).2,
                                  holds :=
                                    InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.input‖ -
                            ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                  output := (sys1.step s1 (iv 0)).2,
                                  holds :=
                                    InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.output‖ +
                          (‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                  output := (sys2.step s2 (iv 1)).2,
                                  holds :=
                                    InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.input‖ -
                            ‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                  output := (sys2.step s2 (iv 1)).2,
                                  holds :=
                                    InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.output‖))
                    hiv))
                (Eq.mpr
                  (id
                    (congrArg
                      (fun _a =>
                        ‖iv 0‖ + ‖iv 1‖ - _a =
                          ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                    output := (sys1.step s1 (iv 0)).2,
                                    holds :=
                                      InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.input‖ -
                              ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                    output := (sys1.step s1 (iv 0)).2,
                                    holds :=
                                      InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.output‖ +
                            (‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                    output := (sys2.step s2 (iv 1)).2,
                                    holds :=
                                      InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.input‖ -
                              ‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                    output := (sys2.step s2 (iv 1)).2,
                                    holds :=
                                      InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.output‖))
                      hout))
                  (Mathlib.Tactic.Ring.of_eq
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖iv 0‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖iv 0‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖iv 1‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖iv 1‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys1.step s1 (iv 0)).2‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys2.step s2 (iv 1)).2‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys1.step s1 (iv 0)).2‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys2.step s2 (iv 1)).2‖
                              (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 *
                                    (Int.negOfNat 1).rawCast +
                                  0)))))))
                    (Mathlib.Tactic.Ring.Common.add_congr
                      (Mathlib.Tactic.Ring.Common.sub_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                output := (sys1.step s1 (iv 0)).2,
                                holds := InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.input‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖iv 0‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s1, input := iv 0, next := (sys1.step s1 (iv 0)).1,
                                output := (sys1.step s1 (iv 0)).2,
                                holds := InformationSystem.stepAt._proof_1 sys1 s1 (iv 0) }.output‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.sub_pf
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys1.step s1 (iv 0)).2‖
                              (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                0)))))
                      (Mathlib.Tactic.Ring.Common.sub_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                output := (sys2.step s2 (iv 1)).2,
                                holds := InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.input‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖iv 1‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s2, input := iv 1, next := (sys2.step s2 (iv 1)).1,
                                output := (sys2.step s2 (iv 1)).2,
                                holds := InformationSystem.stepAt._proof_1 sys2 s2 (iv 1) }.output‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.sub_pf
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys2.step s2 (iv 1)).2‖
                              (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                0)))))
                      (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                        (‖iv 0‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_gt
                          (‖iv 1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖(sys1.step s1 (iv 0)).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(sys2.step s2 (iv 1)).2‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                0))))))))))))))

Complexity: 112767 (size of the value term)

Dependencies: InformationSystem, InformationSystem.Step.delta, InformationSystem.parallel, InformationSystem.stepAt, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: Component.parallel, InformationSystem.toSimplex

Mathlib dependencies: Fin.append, Fin.sum_univ_two, Finset.sum, Finset.univ, Int.rawCast, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Norm, Real, Ring

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

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.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend