OAI/Computability/WLIdentification/CellularCircuits.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLIdentification.CellularCircuit.Address line 11
  2. def OAI.WLIdentification.CellularCircuit.time line 12
  3. def OAI.WLIdentification.CellularCircuit.position line 13
  4. def OAI.WLIdentification.CellularCircuit.address line 14
  5. theorem OAI.WLIdentification.CellularCircuit.time_address line 16
  6. theorem OAI.WLIdentification.CellularCircuit.position_address line 17
  7. theorem OAI.WLIdentification.CellularCircuit.address_parts line 18
  8. theorem OAI.WLIdentification.CellularCircuit.concat_address line 24
  9. inductive OAI.WLIdentification.CellularCircuit.Gate line 29
  10. abbrev OAI.WLIdentification.CellularCircuit.dimension line 35
  11. inductive OAI.WLIdentification.CellularCircuit.Connection line 40
  12. abbrev OAI.WLIdentification.CellularCircuit.ConnectionCode line 48
  13. def OAI.WLIdentification.CellularCircuit.Connection.encode line 52
  14. def OAI.WLIdentification.CellularCircuit.Connection.decode line 59
  15. def OAI.WLIdentification.CellularCircuit.Connection.equiv line 66
  16. instance OAI.WLIdentification.CellularCircuit.(instance at line 80) line 80
  17. theorem OAI.WLIdentification.CellularCircuit.card_connection line 82
  18. abbrev OAI.WLIdentification.CellularCircuit.source line 89
  19. abbrev OAI.WLIdentification.CellularCircuit.target line 96
  20. abbrev OAI.WLIdentification.CellularCircuit.port line 103
  21. def OAI.WLIdentification.CellularCircuit.edgeMap line 111
  22. def OAI.WLIdentification.CellularCircuit.gateIndexValue line 123
  23. def OAI.WLIdentification.CellularCircuit.gateIndex line 128
  24. def OAI.WLIdentification.CellularCircuit.connectionIndex line 137
  25. abbrev OAI.WLIdentification.CellularCircuit.circuit line 145
  26. def OAI.WLIdentification.CellularCircuit.evolution line 164

    Source documentation

    A genuine synchronous radius-one automaton on the cyclic address alphabet.

    noncomputable def evolution (init : Bits d → A) : ℕ → Bits d → A
  | 0 => init
  | t + 1 => fun j => F (evolution init t ((rotation d).symm j))
      (evolution init t j) (evolution init t (rotation d j))

variable (init : Bits d → A)

/-- The intended input-port semantics; only scalar gates can be seeds. -/

    Mentions: OAI.WLIdentification.CellularCircuit.port

  27. def OAI.WLIdentification.CellularCircuit.SemPort line 172

    Source documentation

    The intended input-port semantics; only scalar gates can be seeds.

    noncomputable def SemPort : (p : Gate A) → Address d → Fin (dimension p) → Prop
  | .scalar f, x, _ => f = evolution F init (value (time x)) (position x)
  | .first a b _, x, i => 0 < value (time x) ∧
      if i = 0 then a = evolution F init (value (time x) - 1) ((rotation d).symm (position x))
      else b = evolution F init (value (time x) - 1) (position x)
  | .second a b c, x, i => 0 < value (time x) ∧
      if i = 0 then
        a = evolution F init (value (time x) - 1) ((rotation d).symm (position x)) ∧
        b = evolution F init (value (time x) - 1) (position x)
      else c = evolution F init (value (time x) - 1) (rotation d (position x))

variable {F init}
…

    Mentions: OAI.WLIdentification.CellularCircuit.Gate, OAI.WLIdentification.CellularCircuit.Address, OAI.WLIdentification.CellularCircuit.dimension, OAI.WLIdentification.CellularCircuit.evolution, OAI.WLIdentification.CellularCircuit.time, OAI.WLIdentification.CellularCircuit.position

  28. theorem OAI.WLIdentification.CellularCircuit.edge_sound line 186
  29. def OAI.WLIdentification.CellularCircuit.SeedCorrect line 226

    Source documentation

    Exact compressed initialization, to be instantiated by singletons plus at most d+1 threshold domains below.

    def SeedCorrect : Prop := ∀ f x,
…
  30. theorem OAI.WLIdentification.CellularCircuit.port_sound line 232
  31. theorem OAI.WLIdentification.CellularCircuit.scalar_complete line 249
  32. theorem OAI.WLIdentification.CellularCircuit.accepted_iff line 307