Implementation

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

definition abbreviation lemma theorem
legend

The way we modeled information systems was with one input and one output. We will now generalize this into multiple inputs and outputs, so we can draw block diagrams. Each such block is a ‘component’, where we will now focus on their wiring. The number of inputs (say \(n\)) and the number of outputs (say \(m\)) determine its so-called ‘arity’. An \(n\times m\)-arity component has \(n\) inputs and \(m\) outputs.

Components are fixed-arity building blocks that can be placed in sequence or placed in parallel to form bigger components. We have already seen the Component.Impl.Simplex component before: one input, one output. We also have the Component.Impl.Multiplex component: \(n\) inputs, one output. And also the Component.Impl.Demultiplex component: one input, \(m\) outputs.

Every InformationSystem is a Component.Impl.Simplex component in disguise. However, also conversely, every component can be considered as an InformationSystem.

This covers only the basics: there is more advanced mathematical structure behind components.

Component.Impl

A component has some fixed number of input wires and output wires, all sharing one common per-wire Input, respectively Output, type. Three named special cases mark out useful shapes: the Component.Impl.Simplex (one input, one output — the one actually used below, to recover a plain InformationSystem), the Component.Impl.Multiplex (n inputs feeding one output), and the Component.Impl.Demultiplex (one input fanning out to n outputs). The latter two aren’t composed with anything yet in this file; they’re named here because Component.Impl.sequential/Component.Impl.parallel below already work for any wire counts, not just small fixed ones, so nothing stops a later file from building with them. Components in general are built by linking others together in sequence, or by placing them side by side in parallel.

Technical — you can skip this.

A bundle of n wires is nonempty as soon as the wire’s own type is: just fill every wire with the same witness value. Typeclass plumbing, needed for a Component.Impl’s Fin n → Input/ Fin m → Output to qualify as valid InformationSystem input/output types below.

instance [Nonempty α] {n : Nat} : Nonempty (Fin n → α) :=

Outer dependencies: (none)

Lean core dependencies: Fin, Nat, Nonempty

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

A component with n input wires and m output wires: an information system whose input is one value per input wire (n values in total) and whose output is one value per output wire (m values in total).

abbrev Component.Impl (State Input Output : Type) [Nonempty State] [Norm State]
    [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (n m : Nat) :=
  InformationSystem State (Fin n → Input) (Fin m → Output)

Outer dependencies: (none)

Inner dependencies: InformationSystem, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

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

A component with exactly one input wire and one output wire.

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

Outer dependencies: (none)

Inner dependencies: Component.Impl

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

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

A component with n input wires feeding into a single output wire.

abbrev Component.Impl.Multiplex (State Input Output : Type) [Nonempty State] [Norm State]
    [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (n : Nat) :=
  Component.Impl State Input Output n 1

Outer dependencies: (none)

Inner dependencies: Component.Impl

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: (none)

A component with a single input wire fanning out to n output wires.

abbrev Component.Impl.Demultiplex (State Input Output : Type) [Nonempty State] [Norm State]
    [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (n : Nat) :=
  Component.Impl State Input Output 1 n

Outer dependencies: (none)

Inner dependencies: Component.Impl

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: (none)

Run two components in sequence: the first component’s m output wires feed directly into the second component’s m input wires, producing one bigger component with the first’s number of input wires and the second’s number of output wires.

def Component.Impl.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 : Nat} (c1 : Component.Impl State1 Input Mid n m) (c2 : Component.Impl State2 Mid Output m p) :
    Component.Impl (State1 × State2) Input Output n p where
  step p i :=
    let (s1', mv) := c1.step p.1 i
    let (s2', ov) := c2.step p.2 mv
    ((s1', s2'), ov)
  conserves p i := by
    change ‖p.1‖ + ‖p.2‖ + ‖i‖ =
      ‖(c1.step p.1 i).1‖ + ‖(c2.step p.2 ((c1.step p.1 i).2)).1‖ +
        ‖(c2.step p.2 ((c1.step p.1 i).2)).2‖
    have h1 : ‖p.1‖ + ‖i‖ = ‖(c1.step p.1 i).1‖ + ‖(c1.step p.1 i).2‖ := c1.conserves p.1 i
    have h2 : ‖p.2‖ + ‖(c1.step p.1 i).2‖ =
        ‖(c2.step p.2 ((c1.step p.1 i).2)).1‖ +
          ‖(c2.step p.2 ((c1.step p.1 i).2)).2‖ :=
      c2.conserves p.2 ((c1.step p.1 i).2)
    linarith

Outer dependencies: Component.Impl, 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.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id_comp, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.toSpec_comp, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.id_sequential, Component.Impl.interchange, Component.Impl.parallel_comm, Component.Impl.sequential_assoc, Component.Impl.sequential_congr, Component.Impl.sequential_id, Component.Impl.symmetry_symmetry, InformationSystem.sequential, InformationSystem.sequential_delta

Place two components side by side, independently: their wire bundles are concatenated (the first component’s n1 input wires followed by the second’s n2, likewise for the m1 + m2 output wires), with no interaction between the two components.

def Component.Impl.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 : Nat}
    (c1 : Component.Impl State1 Input Output n1 m1) (c2 : Component.Impl State2 Input Output n2 m2) :
    Component.Impl (State1 × State2) Input Output (n1 + n2) (m1 + m2) where
  step p iv :=
    let (s1', o1) := c1.step p.1 (fun k => iv (Fin.castAdd n2 k))
    let (s2', o2) := c2.step p.2 (fun k => iv (Fin.natAdd n1 k))
    ((s1', s2'), Fin.append o1 o2)
  conserves p iv := by
    have h1 : ‖p.1‖ + ‖(fun k => iv (Fin.castAdd n2 k))‖ =
        ‖(c1.step p.1 (fun k => iv (Fin.castAdd n2 k))).1‖ +
          ‖(c1.step p.1 (fun k => iv (Fin.castAdd n2 k))).2‖ :=
      c1.conserves p.1 (fun k => iv (Fin.castAdd n2 k))
    have h2 : ‖p.2‖ + ‖(fun k => iv (Fin.natAdd n1 k))‖ =
        ‖(c2.step p.2 (fun k => iv (Fin.natAdd n1 k))).1‖ +
          ‖(c2.step p.2 (fun k => iv (Fin.natAdd n1 k))).2‖ :=
      c2.conserves p.2 (fun k => iv (Fin.natAdd n1 k))
    change ‖p.1‖ + ‖p.2‖ + ‖iv‖ =
      ‖(c1.step p.1 (fun k => iv (Fin.castAdd n2 k))).1‖ +
        ‖(c2.step p.2 (fun k => iv (Fin.natAdd n1 k))).1‖ +
        ‖Fin.append ((c1.step p.1 (fun k => iv (Fin.castAdd n2 k))).2)
          ((c2.step p.2 (fun k => iv (Fin.natAdd n1 k))).2)‖
    have hiv : ‖iv‖ =
        ‖(fun k => iv (Fin.castAdd n2 k))‖ + ‖(fun k => iv (Fin.natAdd n1 k))‖ :=
      Fin.sum_univ_add (fun i => ‖iv i‖)
    have hout : ∀ (o1 : Fin m1 → Output) (o2 : Fin m2 → Output),
        ‖Fin.append o1 o2‖ = ‖o1‖ + ‖o2‖ := by
      intro o1 o2
      change (∑ i, ‖Fin.append o1 o2 i‖) = (∑ i, ‖o1 i‖) + (∑ i, ‖o2 i‖)
      rw [Fin.sum_univ_add]
      simp [Fin.append_left, Fin.append_right]
    rw [hout]
    linarith

Outer dependencies: Component.Impl, 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.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.tensor, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.interchange, Component.Impl.monoidalCategory, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.parallel_congr, Component.Impl.parallel_empty, Component.Impl.recast_parallel_left, Component.Impl.recast_parallel_right, InformationSystem.parallel, InformationSystem.parallel_delta

The identity component on n wires: every wire passes straight through unchanged. Composing any component with Component.Impl.id on either side (via Component.Impl.sequential) leaves it as it was.

def Component.Impl.id (Input : Type) [Nonempty Input] [Norm Input] (n : Nat) :
    Component.Impl Unit Input Input n n where
  step _ iv := ((), iv)
  conserves _ iv := by simp [Norm.norm]

Outer dependencies: Component.Impl, 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.Impl.Hom.comp_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id, Component.Impl.Hom.id_comp, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.id_sequential, Component.Impl.monoidalCategory, Component.Impl.sequential_id, Component.Impl.symmetry_symmetry

The symmetry (swap) component: swaps the first n wires and the next m wires as two blocks, turning an n + m-wire bundle into an m + n-wire bundle. Together with Component.Impl.id and Component.Impl.parallel, this one primitive is enough, in principle, to build any rewiring/permutation of wires — this file doesn’t demonstrate that in general, only the specific rewirings each lemma below actually needs.

def Component.Impl.symmetry (Input : Type) [Nonempty Input] [Norm Input] (n m : Nat) :
    Component.Impl Unit Input Input (n + m) (m + n) where
  step _ iv := ((), Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)))
  conserves _ iv := by
    change (0 : ℝ) + (∑ i, ‖iv i‖) =
      (0 : ℝ) + (∑ i, ‖Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) i‖)
    rw [Fin.sum_univ_add (f := fun i => ‖iv i‖), Fin.sum_univ_add
      (f := fun i => ‖Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) i‖)]
    simp only [Fin.append_left, Fin.append_right]
    ring

Outer dependencies: Component.Impl, 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.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_comm, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_comm, Component.Impl.symmetry_symmetry

Identity and associativity laws

Composing any component with Component.Impl.id, on either side, leaves it unchanged, and Component.Impl.sequential is associative — both up to InformationSystem.equivalent.

Composing Component.Impl.id in front of a component changes nothing observable.

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

Dependencies: Component.Impl, Component.Impl.id, Component.Impl.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.Impl.Hom.id_comp

Composing Component.Impl.id behind a component changes nothing observable.

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

Dependencies: Component.Impl, Component.Impl.id, Component.Impl.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.Impl.Hom.comp_id

Composing components in sequence is associative, up to re-associating their combined state.

theorem Component.Impl.sequential_assoc {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 : Nat}
    (c1 : Component.Impl State1 Input Mid1 n m) (c2 : Component.Impl State2 Mid1 Mid2 m p)
    (c3 : Component.Impl State3 Mid2 Output p q) (s1 : State1) (s2 : State2) (s3 : State3) :
    InformationSystem.equivalent (Component.Impl.sequential (Component.Impl.sequential c1 c2) c3)
      (Component.Impl.sequential c1 (Component.Impl.sequential c2 c3)) ((s1, s2), s3) (s1, (s2, s3)) := by

Dependencies: Component.Impl, Component.Impl.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.Impl.Hom.comp_assoc

Sequencing respects equivalence: if c1 ≃ c1' and c2 ≃ c2', then linking them in sequence gives equivalent results. Needed so that swapping either component for an equivalent one never changes what Component.Impl.sequential produces, up to InformationSystem.equivalent.

theorem Component.Impl.sequential_congr {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 : Nat}
    {c1 : Component.Impl State1 Input Mid n m} {c1' : Component.Impl State1' Input Mid n m}
    {c2 : Component.Impl State2 Mid Output m p} {c2' : Component.Impl 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 (Component.Impl.sequential c1 c2) (Component.Impl.sequential c1' c2')
      (s1, s2) (s1', s2') := by

Dependencies: Component.Impl, Component.Impl.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.Impl.Hom.comp

Placing side by side respects equivalence: if c1 ≃ c1' and c2 ≃ c2', then their parallel placements give equivalent results. Needed so that swapping either component for an equivalent one never changes what Component.Impl.parallel produces, up to InformationSystem.equivalent.

theorem Component.Impl.parallel_congr {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 : Nat}
    {c1 : Component.Impl State1 Input Output n1 m1} {c1' : Component.Impl State1' Input Output n1 m1}
    {c2 : Component.Impl State2 Input Output n2 m2} {c2' : Component.Impl 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 (Component.Impl.parallel c1 c2) (Component.Impl.parallel c1' c2')
      (s1, s2) (s1', s2') := by

Dependencies: Component.Impl, Component.Impl.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.Impl.Hom.tensor, Component.Impl.monoidalCategory

Reindex a component along a proof that its wire counts equal some other numbers n'/m' — e.g. turning a component with (n1+n2)+n3 wires into one with n1+(n2+n3) wires. Those two counts are always equal, but Lean still needs to be told so before it will treat one as the other; recast is how we tell it. This exists purely to state Component.Impl.parallel_assoc below.

abbrev Component.Impl.recast {State : Type} [Nonempty State] [Norm State] {n n' m m' : Nat}
    (hn : n = n') (hm : m = m') (c : Component.Impl State Input Output n m) :
    Component.Impl State Input Output n' m' where
  step s iv := let (s', ov) := c.step s (iv ∘ Fin.cast hn); (s', ov ∘ Fin.cast hm.symm)
  conserves s iv := by
    subst hn; subst hm
    simpa using c.conserves s iv

Outer dependencies: Component.Impl

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.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.recast, Component.Impl.Hom.recast_recast, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.parallel_assoc, Component.Impl.recast_congr, Component.Impl.recast_parallel_left, Component.Impl.recast_parallel_right, Component.Impl.recast_recast

Reindexing respects equivalence: if c1 ≃ c2, then reindexing both the same way gives equivalent results. Needed so that swapping the component for an equivalent one never changes what Component.Impl.recast produces, up to InformationSystem.equivalent.

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

Dependencies: Component.Impl, Component.Impl.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.Impl.Hom.recast

Placing components in parallel is associative — but only once we use Component.Impl.recast to line up the two sides’ wire counts ((n1+n2)+n3 and n1+(n2+n3) are equal numbers, but need recast to be treated as the same, as explained there), and only up to InformationSystem.equivalent rather than being identical outright (the combined state on each side is grouped differently).

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

Dependencies: Component.Impl, Component.Impl.parallel, Component.Impl.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.Impl.Hom.tensor_assoc

The empty (0-wire) component. Placing it beside any other component, in parallel, leaves that other component unchanged (see Component.Impl.parallel_empty/Component.Impl.empty_parallel below). It has nothing to say about its Input/Output types since it never touches any wire of either.

abbrev Component.Impl.empty (Input Output : Type) [Nonempty Input] [Norm Input]
    [Nonempty Output] [Norm Output] : Component.Impl Unit Input Output 0 0 where
  step _ _ := ((), Fin.elim0)
  conserves _ _ := by simp [Norm.norm]

Outer dependencies: Component.Impl, 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.Impl.Hom.tensorUnit, Component.Impl.empty_parallel, Component.Impl.monoidalCategory, Component.Impl.parallel_empty

Placing the empty component after c, in parallel, changes nothing observable: n + 0 is already just n (and likewise m + 0 is m), no recast needed — unlike Component.Impl.empty_parallel below, where 0 + n = n does need one.

theorem Component.Impl.parallel_empty {n m : Nat} (c : Component.Impl State1 Input Output n m)
    (s : State1) :
    InformationSystem.equivalent (Component.Impl.parallel c (Component.Impl.empty Input Output)) c
      (s, ()) s := by

Dependencies: Component.Impl, Component.Impl.empty, Component.Impl.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.Impl.monoidalCategory

Placing the empty component before c, in parallel, changes nothing observable — up to Component.Impl.recast, since 0 + n = n (unlike n + 0 = n) is not definitional here.

theorem Component.Impl.empty_parallel {n m : Nat} (c : Component.Impl State1 Input Output n m)
    (s : State1) :
    InformationSystem.equivalent
      (Component.Impl.recast (Nat.zero_add n) (Nat.zero_add m)
        (Component.Impl.parallel (Component.Impl.empty Input Output) c))
      c ((), s) s := by

Dependencies: Component.Impl, Component.Impl.empty, Component.Impl.parallel, Component.Impl.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.Impl.Hom.tensor_empty

Swapping two components placed in parallel is the same as placing the swapped pair in the other order, up to rewiring both ends with Component.Impl.symmetry.

theorem Component.Impl.parallel_comm {n1 m1 n2 m2 : Nat}
    (c1 : Component.Impl State1 Input Output n1 m1) (c2 : Component.Impl State2 Input Output n2 m2)
    (s1 : State1) (s2 : State2) :
    InformationSystem.equivalent (Component.Impl.parallel c1 c2)
      (Component.Impl.sequential (Component.Impl.sequential (Component.Impl.symmetry Input n1 n2)
        (Component.Impl.parallel c2 c1)) (Component.Impl.symmetry Output m2 m1))
      (s1, s2) (((), (s2, s1)), ()) := by

Dependencies: Component.Impl, Component.Impl.parallel, Component.Impl.sequential, Component.Impl.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.Impl.Hom.tensor_comm

Plain information systems as one-wire components

A plain InformationSystem takes and gives one value at a time. A Component.Impl.Simplex does exactly the same thing, just with that one value wrapped up as “one wire” instead, to match how every other Component.Impl is written. The two conversions below turn one into the other and back, and let sequential/parallel on plain information systems be defined as the one-wire special case of Component.Impl.sequential/Component.Impl.parallel.

View a plain information system as a component with exactly one input and one output wire.

abbrev InformationSystem.toSimplex (sys : InformationSystem State1 Input Output) :
    Component.Impl.Simplex State1 Input Output where
  step s iv := let (s', o) := sys.step s (iv 0); (s', fun _ => o)
  conserves s iv := by
    have h : ‖s‖ + ‖iv 0‖ = ‖(sys.step s (iv 0)).1‖ + ‖(sys.step s (iv 0)).2‖ :=
      sys.conserves s (iv 0)
    change ‖s‖ + ‖iv‖ = ‖(sys.step s (iv 0)).1‖ + ‖(fun _ => (sys.step s (iv 0)).2)‖
    have hiv : ‖iv‖ = ‖iv 0‖ := by
      change (∑ i, ‖iv i‖) = ‖iv 0‖
      rw [Fin.sum_univ_one]
    have hout : ‖(fun _ : Fin 1 => (sys.step s (iv 0)).2)‖ =
        ‖(sys.step s (iv 0)).2‖ := by
      change (∑ _i : Fin 1, ‖(sys.step s (iv 0)).2‖) = _
      rw [Fin.sum_univ_one]
    linarith

Outer dependencies: Component.Impl.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

Un-bundle a one-wire component back into a plain information system.

abbrev Component.Impl.Simplex.toInformationSystem (c : Component.Impl.Simplex State1 Input Output) :
    InformationSystem State1 Input Output where
  step s i := let (s', ov) := c.step s (fun _ => i); (s', ov 0)
  conserves s i := by
    have h : ‖s‖ + ‖(fun _ : Fin 1 => i)‖ =
        ‖(c.step s (fun _ => i)).1‖ + ‖(c.step s (fun _ => i)).2‖ :=
      c.conserves s (fun _ : Fin 1 => i)
    change ‖s‖ + ‖i‖ = ‖(c.step s (fun _ => i)).1‖ + ‖(c.step s (fun _ => i)).2 0‖
    have hin : ‖(fun _ : Fin 1 => i)‖ = ‖i‖ := by
      change (∑ _j : Fin 1, ‖i‖) = ‖i‖
      rw [Fin.sum_univ_one]
    have hout : ‖(c.step s (fun _ => i)).2‖ = ‖(c.step s (fun _ => i)).2 0‖ := by
      change (∑ j : Fin 1, ‖(c.step s (fun _ => i)).2 j‖) = _
      rw [Fin.sum_univ_one]
    linarith

Outer dependencies: Component.Impl.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

Run two information systems in sequence: the first’s output feeds the second’s input, and their states are paired up. The one-wire special case of Component.Impl.sequential.

abbrev InformationSystem.sequential
    (sys1 : InformationSystem State1 Input Mid) (sys2 : InformationSystem State2 Mid Output) :
    InformationSystem (State1 × State2) Input Output :=
  Component.Impl.Simplex.toInformationSystem (Component.Impl.sequential sys1.toSimplex sys2.toSimplex)

Outer dependencies: InformationSystem, instNormProd_computerNetworks

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

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Prod

Used by: InformationSystem.sequential_delta

The delta of a sequential composition is exactly the sum of the two systems’ deltas: linking two systems in sequence never creates or destroys information beyond what each part already gains or loses.

theorem InformationSystem.sequential_delta (sys1 : InformationSystem State1 Input Mid)
    (sys2 : InformationSystem State2 Mid Output) (s1 : State1) (s2 : State2) (i : Input) :
    (sequential sys1 sys2).delta (s1, s2) i =
      sys1.delta s1 i + sys2.delta s2 ((sys1.step s1 i).2) := by

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

Proof dependencies: Component.Impl.Simplex.toInformationSystem, Component.Impl.sequential, InformationSystem.Step.delta, InformationSystem.stepAt, 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)

Run two information systems side by side, independently, producing a two-wire component (one wire per system) — the special case of Component.Impl.parallel where each of the two pieces placed side by side has exactly one input wire and one output wire of its own.

abbrev InformationSystem.parallel (sys1 : InformationSystem State1 Input Output)
    (sys2 : InformationSystem State2 Input Output) : Component.Impl (State1 × State2) Input Output 2 2 :=
  Component.Impl.parallel sys1.toSimplex sys2.toSimplex

Outer dependencies: Component.Impl, InformationSystem, instNormProd_computerNetworks

Inner dependencies: Component.Impl.parallel, InformationSystem.toSimplex

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Prod

Used by: InformationSystem.parallel_delta

The delta of a parallel placement is exactly the sum of the two systems’ deltas at their own wire: placing two systems side by side never creates or destroys information beyond what each part already gains or loses on its own input.

theorem InformationSystem.parallel_delta (sys1 : InformationSystem State1 Input Output)
    (sys2 : InformationSystem State2 Input Output) (s1 : State1) (s2 : State2)
    (iv : Fin 2 → Input) :
    (parallel sys1 sys2).delta (s1, s2) iv = sys1.delta s1 (iv 0) + sys2.delta s2 (iv 1) := by

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

Proof dependencies: Component.Impl.parallel, InformationSystem.Step.delta, InformationSystem.stepAt, 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) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency
legend