Specification

Difficulty: optional — 17 definitions, 1 abbreviations, 15 lemmas, 1 theorems.

definition abbreviation lemma theorem

legend

A specification says what is allowed to happen on a component’s wires, without pinning down anything computable: for a given value on the input wires, more than one value on the output wires might be acceptable, or (if nothing satisfies it) none at all. Nothing here needs the input/output types to carry a measure, or even to be inhabited — a specification is a constraint to be satisfied, never something that gets run.

Component.Spec

Filling a shape with a specification: a constraint between a value on the input wires and a value on the output wires.

abbrev Component.Spec (Input Output : Type) : Component.Family :=
  fun n m => (Fin n → Input) → (Fin m → Output) → Prop

Outer dependencies: Component.Family

Lean core dependencies: Fin, Nat

Component.Spec.sequential

Run two specifications in sequence: an input and an output satisfy the combination exactly when some value in between satisfies the first specification together with the second.

def Component.Spec.sequential {Input Mid Output : Type} {n m p : Nat}
    (f : Component.Spec Input Mid n m) (g : Component.Spec Mid Output m p) :
    Component.Spec Input Output n p :=
  fun i o => ∃ mid, f i mid ∧ g mid o

Outer dependencies: Component.Spec

Lean core dependencies: And, Exists, Fin, Nat

Component.Spec.parallel

Place two specifications side by side: the combined wires satisfy it exactly when each half satisfies its own specification on its own share of the wires.

def Component.Spec.parallel {Input Output : Type} {n1 m1 n2 m2 : Nat}
    (f : Component.Spec Input Output n1 m1) (g : Component.Spec Input Output n2 m2) :
    Component.Spec Input Output (n1 + n2) (m1 + m2) :=
  fun iv ov =>
    f (fun k => iv (Fin.castAdd n2 k)) (fun k => ov (Fin.castAdd m2 k)) ∧
    g (fun k => iv (Fin.natAdd n1 k)) (fun k => ov (Fin.natAdd m1 k))

Outer dependencies: Component.Spec

Lean core dependencies: And, Fin, Fin.castAdd, Fin.natAdd, Nat

Component.Spec.id

The identity specification on n wires: the only allowed output is the input itself, wire for wire.

def Component.Spec.id (Input : Type) (n : Nat) : Component.Spec Input Input n n :=
  fun iv ov => ov = iv

Outer dependencies: Component.Spec

Lean core dependencies: Eq, Fin, Nat

Used by: Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.symmetry_symmetry, Component.Impl.Hom.toSpec_id, Component.Spec.braidedCategory, Component.Spec.category, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp, Component.Spec.eqToHom_eq_recast_id, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.id_eq_toSpec, Component.Spec.id_sequential, Component.Spec.monoidalCategory, Component.Spec.monoidalCategoryStruct, Component.Spec.not_cartesian, Component.Spec.parallel_id_id, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.sequential_id, Component.Spec.symmetry_symmetry, Component.Spec.symmetry_symmetry', Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_yanking

Component.Spec.symmetry

The symmetry (swap) specification: the only allowed output is the input’s first n wires and next m wires, swapped as two blocks.

def Component.Spec.symmetry (Input : Type) (n m : Nat) :
    Component.Spec Input Input (n + m) (m + n) :=
  fun iv ov => ov = Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k))

Outer dependencies: Component.Spec

Mathlib dependencies: Fin.append

Lean core dependencies: Eq, Fin, Fin.castAdd, Fin.natAdd, Nat

Used by: Component.Func.parallel_comm, Component.Func.symmetry_symmetry, Component.Spec.braidedCategory, Component.Spec.braiding, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_comm, Component.Spec.symmetry_eq_toSpec, Component.Spec.symmetry_symmetry, Component.Spec.symmetry_symmetry', Component.Spec.trace_yanking

Component.Spec.sequential_assoc

Composing specifications in sequence is associative, exactly — unlike Component.Impl.sequential, a specification carries no state to reassociate, so no further equivalence is needed.

theorem Component.Spec.sequential_assoc {Input Mid1 Mid2 Output : Type} {n m p q : Nat}
    (f : Component.Spec Input Mid1 n m) (g : Component.Spec Mid1 Mid2 m p)
    (h : Component.Spec Mid2 Output p q) :
    Component.Spec.sequential (Component.Spec.sequential f g) h =
      Component.Spec.sequential f (Component.Spec.sequential g h) := by

Dependencies: Component.Spec, Component.Spec.sequential

Lean core dependencies: And, Eq, Fin, Nat, funext

Used by: Component.Spec.braidedCategory, Component.Spec.category

Component.Spec.id_sequential

Composing the identity specification in front of f changes nothing, exactly.

theorem Component.Spec.id_sequential {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) :
    Component.Spec.sequential (Component.Spec.id Input n) f = f := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.sequential

Lean core dependencies: And, Eq, Fin, Nat, funext, rfl

Used by: Component.Spec.category, Component.Spec.eqToHom_comp

Component.Spec.sequential_id

Composing the identity specification behind f changes nothing, exactly.

theorem Component.Spec.sequential_id {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) :
    Component.Spec.sequential f (Component.Spec.id Output m) = f := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.sequential

Lean core dependencies: And, Eq, Fin, Nat, funext, rfl

Used by: Component.Spec.braidedCategory, Component.Spec.category, Component.Spec.comp_eqToHom

Component.Spec.recast

Reindex a specification along a proof that its wire counts equal some other numbers n'/m' — the specification-level counterpart of Component.Impl.recast, needed to state Component.Spec.parallel_assoc below.

def Component.Spec.recast {Input Output : Type} {n n' m m' : Nat} (hn : n = n') (hm : m = m')
    (f : Component.Spec Input Output n m) : Component.Spec Input Output n' m' :=
  fun iv ov => f (iv ∘ Fin.cast hn) (ov ∘ Fin.cast hm)

Outer dependencies: Component.Spec

Lean core dependencies: Eq, Fin, Fin.cast, Function.comp, Nat

Component.Spec.parallel_assoc

Placing specifications side by side is associative, up to Component.Spec.recast lining up the two sides’ wire counts (the same reindexing Component.Impl.parallel_assoc needs, for the same reason: (n1+n2)+n3 and n1+(n2+n3) are equal numbers, but not the same Fin type outright).

theorem Component.Spec.parallel_assoc {Input Output : Type} {n1 m1 n2 m2 n3 m3 : Nat}
    (f1 : Component.Spec Input Output n1 m1) (f2 : Component.Spec Input Output n2 m2)
    (f3 : Component.Spec Input Output n3 m3) :
    Component.Spec.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
        (Component.Spec.parallel (Component.Spec.parallel f1 f2) f3) =
      Component.Spec.parallel f1 (Component.Spec.parallel f2 f3) := by

Dependencies: Component.Spec, Component.Spec.parallel, Component.Spec.recast

Used by: Component.Func.parallel_assoc, Component.Spec.monoidalCategory

Component.Spec.parallel_sequential

Sequencing and placing side by side commute: running two pairs of specifications in sequence, then placing the two results side by side, allows exactly the same input/output pairs as placing each pair side by side first, then running the two combined halves in sequence. This is exactly what lets Component.Spec.parallel be applied to already-sequenced specifications without caring which order the two operations happen in.

theorem Component.Spec.parallel_sequential {Input Mid Output : Type} {n1 m1 p1 n2 m2 p2 : Nat}
    (f1 : Component.Spec Input Mid n1 m1) (g1 : Component.Spec Mid Output m1 p1)
    (f2 : Component.Spec Input Mid n2 m2) (g2 : Component.Spec Mid Output m2 p2) :
    Component.Spec.parallel (Component.Spec.sequential f1 g1) (Component.Spec.sequential f2 g2) =
      Component.Spec.sequential
        (Component.Spec.parallel f1 f2) (Component.Spec.parallel g1 g2) := by

Dependencies: Component.Spec, Component.Spec.parallel, Component.Spec.sequential

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

Lean core dependencies: And, Eq, Eq.mpr, Exists, Fin, Fin.castAdd, Fin.natAdd, Nat, congrArg, congrFun', funext, id

Used by: Component.Spec.monoidalCategory

Component.Spec.symmetry_symmetry

Composing the symmetry specification with itself, both ways round, undoes the swap: swapping an n-then-m split into m-then-n and back again changes nothing.

theorem Component.Spec.symmetry_symmetry {Input : Type} (n m : Nat) :
    Component.Spec.sequential
        (Component.Spec.symmetry Input n m) (Component.Spec.symmetry Input m n) =
      Component.Spec.recast rfl rfl (Component.Spec.id Input (n + m)) := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.recast, Component.Spec.sequential, Component.Spec.symmetry

Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Fin.append_left, Fin.append_right

Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, Fin, Fin.cast, Fin.castAdd, Fin.cast_refl, Fin.natAdd, Function.comp, Nat, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true, rfl

Used by: Component.Func.symmetry_symmetry, Component.Spec.symmetry_symmetry'

Component.Spec.parallel_comm

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

theorem Component.Spec.parallel_comm {Wire : Type} {n1 m1 n2 m2 : Nat}
    (f1 : Component.Spec Wire Wire n1 m1) (f2 : Component.Spec Wire Wire n2 m2) :
    Component.Spec.parallel f1 f2 =
      Component.Spec.sequential
        (Component.Spec.sequential (Component.Spec.symmetry Wire n1 n2)
          (Component.Spec.parallel f2 f1))
        (Component.Spec.symmetry Wire m2 m1) := by

Dependencies: Component.Spec, Component.Spec.parallel, Component.Spec.sequential, Component.Spec.symmetry

Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Fin.append_left, Fin.append_right

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, Fin, Fin.castAdd, Fin.natAdd, Nat, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true, rfl

Used by: Component.Func.parallel_comm, Component.Spec.braidedCategory

`Component.Func`’s own algebra

A rule is a plain function, so composing rules in sequence is plain function composition — Component.Func.sequential_assoc/id_sequential/sequential_id below all hold outright (rfl), not just up to some further equivalence, the same way Component.Spec’s own versions do exactly (and unlike Component.Impl’s, which only hold up to InformationSystem.equivalent).

Component.Func.sequential

Run two rules in sequence: feed the first rule’s output straight into the second.

def Component.Func.sequential {Input Mid Output : Type} {n m p : Nat}
    (f : Component.Func Input Mid n m) (g : Component.Func Mid Output m p) :
    Component.Func Input Output n p :=
  g ∘ f

Outer dependencies: Component.Func

Lean core dependencies: Fin, Function.comp, Nat

Used by: Component.Func.braidedCategory, Component.Func.category, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.id_sequential, Component.Func.monoidalCategory, Component.Func.parallel_comm, Component.Func.parallel_sequential, Component.Func.sequential_assoc, Component.Func.sequential_id, Component.Func.symmetry_symmetry, Component.Func.symmetry_symmetry', Component.Func.toSpec_sequential, Component.Impl.Hom.toSpec_comp, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

Component.Func.parallel

Place two rules side by side: each half runs on its own share of the wires, independently.

def Component.Func.parallel {Input Output : Type} {n1 m1 n2 m2 : Nat}
    (f : Component.Func Input Output n1 m1) (g : Component.Func Input Output n2 m2) :
    Component.Func Input Output (n1 + n2) (m1 + m2) :=
  fun iv => Fin.append (f (fun k => iv (Fin.castAdd n2 k))) (g (fun k => iv (Fin.natAdd n1 k)))

Outer dependencies: Component.Func

Mathlib dependencies: Fin.append

Lean core dependencies: Fin, Fin.castAdd, Fin.natAdd, Nat

Used by: Component.Func.braidedCategory, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.parallel_sequential, Component.Func.recast_parallel_left, Component.Func.recast_parallel_right, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_toSpec_eq

Component.Func.id

The identity rule on n wires: hand every input straight back, unchanged.

def Component.Func.id (Input : Type) (n : Nat) : Component.Func Input Input n n :=
  _root_.id

Outer dependencies: Component.Func

Lean core dependencies: Fin, Nat, id

Used by: Component.Func.braidedCategory, Component.Func.category, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.eqToHom_eq_recast_id, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.id_sequential, Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.sequential_id, Component.Func.symmetry_symmetry, Component.Func.symmetry_symmetry', Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.id_eq_toSpec

Component.Func.symmetry

The symmetry (swap) rule: swap the first n wires and the next m wires as two blocks.

def Component.Func.symmetry (Input : Type) (n m : Nat) :
    Component.Func Input Input (n + m) (m + n) :=
  fun iv => Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k))

Outer dependencies: Component.Func

Mathlib dependencies: Fin.append

Lean core dependencies: Fin, Fin.castAdd, Fin.natAdd, Nat

Used by: Component.Func.braidedCategory, Component.Func.braiding, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.parallel_comm, Component.Func.symmetry_symmetry, Component.Func.symmetry_symmetry', Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.symmetry_eq_toSpec

Component.Func.recast

Reindex a rule along a proof that its wire counts equal some other numbers n'/m'.

def Component.Func.recast {Input Output : Type} {n n' m m' : Nat} (hn : n = n') (hm : m = m')
    (f : Component.Func Input Output n m) : Component.Func Input Output n' m' :=
  fun iv => (f (iv ∘ Fin.cast hn)) ∘ Fin.cast hm.symm

Outer dependencies: Component.Func

Lean core dependencies: Eq, Eq.symm, Fin, Fin.cast, Function.comp, Nat

Used by: Component.Func.braidedCategory, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.eqToHom_eq_recast_id, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.monoidalCategory, Component.Func.parallel_assoc, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.recast_eqToHom, Component.Func.recast_parallel_left, Component.Func.recast_parallel_right, Component.Func.recast_recast, Component.Func.symmetry_symmetry, Component.Func.symmetry_symmetry', Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.recast_toSpec_eq

Component.Func.sequential_assoc

Composing rules in sequence is associative, exactly.

theorem Component.Func.sequential_assoc {Input Mid1 Mid2 Output : Type} {n m p q : Nat}
    (f : Component.Func Input Mid1 n m) (g : Component.Func Mid1 Mid2 m p)
    (h : Component.Func Mid2 Output p q) :
    Component.Func.sequential (Component.Func.sequential f g) h =
      Component.Func.sequential f (Component.Func.sequential g h) := rfl

Dependencies: Component.Func, Component.Func.sequential

Lean core dependencies: Eq, Nat, rfl

Used by: Component.Func.braidedCategory, Component.Func.category

Component.Func.id_sequential

Composing the identity rule in front of f changes nothing, exactly.

theorem Component.Func.id_sequential {Input Output : Type} {n m : Nat}
    (f : Component.Func Input Output n m) :
    Component.Func.sequential (Component.Func.id Input n) f = f := rfl

Dependencies: Component.Func, Component.Func.id, Component.Func.sequential

Lean core dependencies: Eq, Nat, rfl

Used by: Component.Func.category, Component.Func.eqToHom_comp

Component.Func.sequential_id

Composing the identity rule behind f changes nothing, exactly.

theorem Component.Func.sequential_id {Input Output : Type} {n m : Nat}
    (f : Component.Func Input Output n m) :
    Component.Func.sequential f (Component.Func.id Output m) = f := rfl

Dependencies: Component.Func, Component.Func.id, Component.Func.sequential

Lean core dependencies: Eq, Nat, rfl

Used by: Component.Func.braidedCategory, Component.Func.category, Component.Func.comp_eqToHom

Component.Func.parallel_sequential

Sequencing and placing side by side commute — the interchange law, exactly, the same way Component.Spec.parallel_sequential does.

theorem Component.Func.parallel_sequential {Input Mid Output : Type} {n1 m1 p1 n2 m2 p2 : Nat}
    (f1 : Component.Func Input Mid n1 m1) (g1 : Component.Func Mid Output m1 p1)
    (f2 : Component.Func Input Mid n2 m2) (g2 : Component.Func Mid Output m2 p2) :
    Component.Func.parallel (Component.Func.sequential f1 g1) (Component.Func.sequential f2 g2) =
      Component.Func.sequential
        (Component.Func.parallel f1 f2) (Component.Func.parallel g1 g2) := by

Dependencies: Component.Func, Component.Func.parallel, Component.Func.sequential

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

Lean core dependencies: Eq, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, Nat, True, congrArg, eq_self, funext, id, of_eq_true

Used by: Component.Func.monoidalCategory

Implementation, rule, specification

Component.Impl (a measured Mealy machine), Component.Func (a stateless rule), and Component.Spec (a possibly-nondeterministic constraint) each fill the same shape, but say increasingly less about how the wires behave. Going from more committed to less committed costs nothing: any component fixed at some state induces the rule it happens to follow right now, and any rule induces the specification it always satisfies (itself, seen as a constraint). Going the other way, from less committed to more, is where the real content is: it needs a reason (realizability, or measure-preservation) before it can be done at all, matching this project’s own rule that a claim of existence needs a witness.

Component.Impl.toFunc

Read a component’s own rule off, at a state it currently happens to be in: what it hands back right now, for each possible input, dropping what state it moves to next.

def Component.Impl.toFunc {State Input Output : Type} [Nonempty State] [Norm State]
    [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] {n m : Nat}
    (c : Component.Impl State Input Output n m) (s : State) : Component.Func Input Output n m :=
  fun i => (c.step s i).2

Outer dependencies: Component.Func, Component.Impl

Inner dependencies: instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_comp

Component.Func.toSpec

Every rule satisfies one specification for sure: the constraint that the output is exactly what the rule itself hands back.

def Component.Func.toSpec {Input Output : Type} {n m : Nat} (f : Component.Func Input Output n m) :
    Component.Spec Input Output n m :=
  fun i o => o = f i

Outer dependencies: Component.Func, Component.Spec

Lean core dependencies: Eq, Fin, Nat

Component.Func.toSpec_realizable

A rule always satisfies the specification it induces — the one fact Component.Func.toSpec promises for free, with nothing further to check.

theorem Component.Func.toSpec_realizable {Input Output : Type} {n m : Nat}
    (f : Component.Func Input Output n m) : ∀ i, ∃ o, f.toSpec i o :=

Dependencies: Component.Func, Component.Func.toSpec

Lean core dependencies: Exists, Fin, Nat, rfl

Used by: (none)

Component.Spec.Univalent

A specification is univalent when it never allows more than one output for the same input — it may still allow none at all. This is what a partial rule looks like as a specification: deterministic wherever it says anything, just not required to say something everywhere.

def Component.Spec.Univalent {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) : Prop :=
  ∀ i o1 o2, f i o1 → f i o2 → o1 = o2

Outer dependencies: Component.Spec

Lean core dependencies: Eq, Fin, Nat

Used by: Component.Func.toSpec_univalent, Component.Spec.eq_toSpec_of_univalent, Component.Spec.impossible_univalent

Component.Func.toSpec_univalent

The specification a rule induces is always univalent: a rule hands back one and the same output for one and the same input, never two different ones.

theorem Component.Func.toSpec_univalent {Input Output : Type} {n m : Nat}
    (f : Component.Func Input Output n m) : f.toSpec.Univalent :=

Dependencies: Component.Func, Component.Func.toSpec, Component.Spec.Univalent

Lean core dependencies: Eq.symm, Eq.trans, Fin, Nat

Used by: (none)

Component.Spec.Realizable

A specification is realizable when it allows some output for every input — not yet a recipe for finding one, only a promise that one always exists.

def Component.Spec.Realizable {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) : Prop :=
  ∀ i, ∃ o, f i o

Outer dependencies: Component.Spec

Lean core dependencies: Exists, Fin, Nat

Used by: Component.Spec.eq_toSpec_of_univalent, Component.Spec.fixedPoint_realizable, Component.Spec.toFunc, Component.Spec.toFunc_spec, notRule_fixedPoint_unrealizable

Component.Spec.toFunc

Turning a realizable specification into an actual rule: for every input, pick some output the specification allows. Different choices are all equally valid whenever the specification allows more than one output for the same input — this is one of them, not the one. Noncomputable on purpose: nothing here promises the choice can be produced by any effective procedure, only that it exists.

noncomputable def Component.Spec.toFunc {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) (h : f.Realizable) : Component.Func Input Output n m :=
  fun i => (h i).choose

Outer dependencies: Component.Func, Component.Spec, Component.Spec.Realizable

Lean core dependencies: Exists.choose, Fin, Nat

Used by: Component.Spec.eq_toSpec_of_univalent, Component.Spec.toFunc_spec

Component.Spec.toFunc_spec

The rule Component.Spec.toFunc produces really does satisfy the specification it came from, on every input.

theorem Component.Spec.toFunc_spec {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) (h : f.Realizable) (i : Fin n → Input) :
    f i (f.toFunc h i) :=

Dependencies: Component.Spec, Component.Spec.Realizable, Component.Spec.toFunc

Lean core dependencies: Exists.choose_spec, Fin, Nat

Used by: Component.Spec.eq_toSpec_of_univalent

Component.Spec.eq_toSpec_of_univalent

A realizable, univalent specification isn’t just satisfied by some rule — it says exactly what that rule says, on every input and every output alike: a specification this well-behaved carries no more information than a rule already would.

theorem Component.Spec.eq_toSpec_of_univalent {Input Output : Type} {n m : Nat}
    (f : Component.Spec Input Output n m) (hr : f.Realizable) (hu : f.Univalent) :
    f = (f.toFunc hr).toSpec := by

Dependencies: Component.Func.toSpec, Component.Spec, Component.Spec.Realizable, Component.Spec.Univalent, Component.Spec.toFunc

Proof dependencies: Component.Spec.toFunc_spec

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, congrArg, funext, id

Used by: (none)

Component.Func.Conserves

A rule conserves information when its output always carries exactly as much as its input did — neither losing nor gaining any. Most rules don’t: BitFunctions with more inputs than outputs, say, necessarily lose some.

def Component.Func.Conserves {Input Output : Type} [Norm Input] [Norm Output] {n m : Nat}
    (f : Component.Func Input Output n m) : Prop :=
  ∀ i, ‖i‖ = ‖f i‖

Outer dependencies: Component.Func

Inner dependencies: instNormForallFin_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, Fin, Nat

Used by: Component.Func.toImpl

Component.Func.toImpl

Turning a measure-conserving rule into an actual component: the simplest possible state (a single value, carrying no information of its own) that just runs the rule every time, never changing. This only works because the rule already conserves information on its own — with no state of its own to absorb any surplus or deficit, a rule that didn’t conserve information would break the first law here.

def Component.Func.toImpl {Input Output : Type} [Nonempty Input] [Norm Input]
    [Nonempty Output] [Norm Output] {n m : Nat} (f : Component.Func Input Output n m)
    (h : f.Conserves) : Component.Impl Unit Input Output n m where
  step _ i := ((), f i)
  conserves _ i := by simpa [Norm.norm] using h i

Outer dependencies: Component.Func, Component.Func.Conserves, 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.mpr, Eq.trans, Fin, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, id

Used by: (none)

Component.Func.toSpec_sequential

Running two rules in sequence and reading off the specification they satisfy together is the same as reading off each rule’s own specification first, then running those two specifications in sequence: Component.Func.toSpec respects composition.

theorem Component.Func.toSpec_sequential {Input Mid Output : Type} {n m p : Nat}
    (f : Component.Func Input Mid n m) (g : Component.Func Mid Output m p) :
    Component.Spec.sequential f.toSpec g.toSpec =
      Component.Func.toSpec (Component.Func.sequential f g) := by

Dependencies: Component.Func, Component.Func.sequential, Component.Func.toSpec, Component.Spec, Component.Spec.sequential

Lean core dependencies: And, Eq, Eq.symm, Exists, Fin, Function.comp, Nat, funext, id, rfl

Used by: Component.Func.parallel_comm, Component.Func.symmetry_symmetry, Component.Impl.Hom.toSpec_comp, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

Dependency diagram

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

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend

Component.Func’s own algebra

Implementation, rule, specification

Dependency diagram

`Component.Func`’s own algebra