OAI/Computability/WLIdentification/BufferedCircuits.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLIdentification.BufferAlgebra.Vector line 9
  2. def OAI.WLIdentification.BufferAlgebra.Determined line 11
  3. theorem OAI.WLIdentification.BufferAlgebra.determined_comp line 14
  4. theorem OAI.WLIdentification.BufferAlgebra.determined_zero line 28
  5. theorem OAI.WLIdentification.BufferAlgebra.determined_sum line 31
  6. theorem OAI.WLIdentification.BufferAlgebra.subsingleton_of_coordinates line 36
  7. theorem OAI.WLIdentification.BufferAlgebra.determined_of_subsingleton line 42
  8. theorem OAI.WLIdentification.BufferAlgebra.forward line 48

    Source documentation

    Arbitrarily shifted private buffers propagate singletonness only forwards.

    theorem forward {V W : Type} {Q : Set V} {R : Set W} {B : Set Vector}
    {f : V → Bit} {g : W → Bit} (d₁ d₂ d₃ : Bit)
    (h₁ : f '' Q = (fun v => d₁ + v 0) '' B)
    (h₂ : f '' Q = (fun v => d₂ + v 1) '' B)
    (h₃ : (fun v => v 0 + v 1) '' B = (fun w => d₃ + g w) '' R)
    (h : Determined Q f) : Determined R g := by
…

    Mentions: OAI.WLIdentification.BufferAlgebra.Vector, OAI.WLIdentification.Bit, OAI.WLIdentification.BufferAlgebra.Determined

  9. theorem OAI.WLIdentification.BufferAlgebra.self_value line 61

    Source documentation

    Two copies of one source value cancel, even for nonconstant wire shifts.

    theorem self_value (x z₁ z₂ d₁ d₂ d₃ : Bit)
    (h₁ : x = d₁ + z₁) (h₂ : x = d₂ + z₂)
    (h₃ : z₁ + z₂ = d₃ + x) : x = d₁ + d₂ + d₃ := by
…

    Mentions: OAI.WLIdentification.Bit

  10. def OAI.WLIdentification.BufferAlgebra.truthVectors line 67

    Source documentation

    Truth fixes a coordinate to zero; false coordinates remain free.

    def truthVectors {J : Type} (t : J → Prop) : Set (J → Bit) :=
…

    Mentions: OAI.WLIdentification.Bit

  11. theorem OAI.WLIdentification.BufferAlgebra.truthVectors_nonempty line 70
  12. theorem OAI.WLIdentification.BufferAlgebra.projection_truth line 73
  13. theorem OAI.WLIdentification.BufferAlgebra.sum_truth line 93
  14. def OAI.WLIdentification.BufferAlgebra.correlated line 121

    Source documentation

    Correlated coordinates keep both input images full while prescribing the sum.

    def correlated (D : Set Bit) : Set Vector := {v | v 0 + v 1 ∈ D}

    Mentions: OAI.WLIdentification.Bit, OAI.WLIdentification.BufferAlgebra.Vector

  15. theorem OAI.WLIdentification.BufferAlgebra.correlated_nonempty line 123
  16. theorem OAI.WLIdentification.BufferAlgebra.correlated_projection line 127
  17. theorem OAI.WLIdentification.BufferAlgebra.correlated_sum line 138
  18. structure OAI.WLIdentification.ProductMap line 150

    Source documentation

    A componentwise injection on a nonempty Boolean product domain. Values of mapping off the domain are immaterial.

    structure ProductMap (r : ℕ) where
…
  19. abbrev OAI.WLIdentification.ProductMap.Point line 158
  20. def OAI.WLIdentification.ProductMap.source line 159
  21. def OAI.WLIdentification.ProductMap.target line 160
  22. def OAI.WLIdentification.ProductMap.identity line 162
  23. def OAI.WLIdentification.ProductMap.flip line 168
  24. def OAI.WLIdentification.ProductMap.identityOn line 177
  25. def OAI.WLIdentification.ProductMap.ofAddress line 183
  26. theorem OAI.WLIdentification.ProductMap.source_ofAddress line 186
  27. structure OAI.WLIdentification.ProductCircuit line 190
  28. inductive OAI.WLIdentification.ProductCircuit.PortTrue line 211
  29. def OAI.WLIdentification.ProductCircuit.True line 218
  30. def OAI.WLIdentification.ProductCircuit.Accepted line 220
  31. theorem OAI.WLIdentification.ProductCircuit.accepted_reseed line 223
  32. abbrev OAI.WLIdentification.ProductCircuit.Primary line 243
  33. abbrev OAI.WLIdentification.ProductCircuit.primaryDimension line 245
  34. def OAI.WLIdentification.ProductCircuit.sumForm line 249
  35. theorem OAI.WLIdentification.ProductCircuit.sumForm_apply line 251
  36. inductive OAI.WLIdentification.ProductCircuit.Connection line 254
  37. abbrev OAI.WLIdentification.ProductCircuit.connectionSource line 263
  38. abbrev OAI.WLIdentification.ProductCircuit.connectionTarget line 271
  39. abbrev OAI.WLIdentification.ProductCircuit.connectionMap line 279
  40. abbrev OAI.WLIdentification.ProductCircuit.sourceForm line 287
  41. abbrev OAI.WLIdentification.ProductCircuit.targetForm line 296
  42. inductive OAI.WLIdentification.ProductCircuit.RealType line 305
  43. inductive OAI.WLIdentification.ProductCircuit.Comparison line 311
  44. abbrev OAI.WLIdentification.ProductCircuit.realDimension line 318
  45. abbrev OAI.WLIdentification.ProductCircuit.comparisonSource line 323
  46. abbrev OAI.WLIdentification.ProductCircuit.comparisonTarget line 329
  47. abbrev OAI.WLIdentification.ProductCircuit.comparisonMap line 335
  48. abbrev OAI.WLIdentification.ProductCircuit.comparisonLeft line 341
  49. abbrev OAI.WLIdentification.ProductCircuit.comparisonRight line 349
  50. def OAI.WLIdentification.ProductCircuit.connectionIndexValue line 359

    Source documentation

    Exactly seeds and three comparisons per private buffer, with two distinct copies of A's full-product identity self-connection.

    def connectionIndexValue : C.Connection → ℕ
  | .original e => Nat.pair 0 (C.edgeIndex e)
  | .test t => Nat.pair 1 (C.testIndex t)
  | .flip i => Nat.pair 2 i.val
  | .broadcast p j => Nat.pair 3 (Nat.pair (C.pointIndex p) j.val)
  | .self p j => Nat.pair 4 (Nat.pair (NaturalCode.option C.pointIndex p) j.val)
  | .conflict => Nat.pair 5 0

    Mentions: OAI.WLIdentification.NaturalCode.option

  51. def OAI.WLIdentification.ProductCircuit.connectionIndex line 367
  52. def OAI.WLIdentification.ProductCircuit.realIndexValue line 391
  53. def OAI.WLIdentification.ProductCircuit.realIndex line 396
  54. def OAI.WLIdentification.ProductCircuit.comparisonIndexValue line 407
  55. def OAI.WLIdentification.ProductCircuit.comparisonIndex line 413
  56. def OAI.WLIdentification.ProductCircuit.schemas line 425