OAI/Computability/FourierCircuit/SlotAssembly.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactFourier.Packing.Inventory line 14
  2. abbrev OAI.ExactFourier.Packing.ActiveSpace line 15
  3. def OAI.ExactFourier.Packing.inventoryMatrix line 17
  4. theorem OAI.ExactFourier.Packing.layer_decompose line 20
  5. theorem OAI.ExactFourier.Packing.gather_active line 30
  6. def OAI.ExactFourier.Packing.inventoryWithIdentity line 50
  7. theorem OAI.ExactFourier.Packing.embedded_inl line 53
  8. theorem OAI.ExactFourier.Packing.assemble_slot line 63

    Source documentation

    One full slot, with spectators carrying arbitrary data, is exactly one J call.

    theorem assemble_slot (k : τ→ℕ) (S : ∀ p,Step D A (β p))
    (hc : ∀ t,Fintype.card {p // (S p).kind=some t}=k t)
    (hw : Fintype.card (ActiveSpace D k ⊕ ν)≤Fintype.card (Σ p,β p)) :
    ∃ (M : Matrix (Σ p,β p) (Σ p,β p) ℂ) (e : ActiveSpace D k ⊕ ν ↪ (Σ p,β p)),
      MonomialMatrix M ∧ Matrix.blockDiagonal' (fun p=>(S p).matrix)=
        M*Embedded.matrix e (inventoryWithIdentity (A := A) (ν := ν) k) := by
…

    Mentions: OAI.ExactFourier.Packing.Step, OAI.ExactFourier.Packing.ActiveSpace, OAI.ExactFourier.MonomialMatrix, OAI.ExactFourier.Embedded.matrix, OAI.ExactFourier.Packing.inventoryWithIdentity

  9. abbrev OAI.ExactFourier.Packing.SpeciesDomain line 88
  10. instance OAI.ExactFourier.Packing.SpeciesDomain_fintype line 91
  11. instance OAI.ExactFourier.Packing.SpeciesDomain_decEq line 93
  12. def OAI.ExactFourier.Packing.speciesMatrix line 96
  13. abbrev OAI.ExactFourier.Packing.speciesCopies line 100
  14. abbrev OAI.ExactFourier.Packing.SpeciesSpace line 104
  15. def OAI.ExactFourier.Packing.speciesCoordinates line 107
  16. theorem OAI.ExactFourier.Packing.speciesCoordinates_matrix line 122
  17. abbrev OAI.ExactFourier.Packing.LivePair line 147
  18. abbrev OAI.ExactFourier.Packing.PairDomain line 148
  19. def OAI.ExactFourier.Packing.pairMatrix line 150
  20. abbrev OAI.ExactFourier.Packing.LiveSpace line 153
  21. def OAI.ExactFourier.Packing.liveCoordinates line 156
  22. structure OAI.ExactFourier.Packing.Frame line 185
  23. def OAI.ExactFourier.Packing.Frame.matrix line 192
  24. def OAI.ExactFourier.Packing.Frame.pre line 194
  25. structure OAI.ExactFourier.Packing.FramedWord line 197
  26. def OAI.ExactFourier.Packing.FramedWord.matrix line 203
  27. def OAI.ExactFourier.Packing.FramedWord.types line 206
  28. def OAI.ExactFourier.Packing.FramedWord.pre line 208
  29. theorem OAI.ExactFourier.Packing.FramedWord.matrix_pre line 213
  30. theorem OAI.ExactFourier.Packing.FramedWord.types_pre line 218
  31. def OAI.ExactFourier.Packing.Word.framed line 223
  32. theorem OAI.ExactFourier.Packing.Word.matrix_framed line 228
  33. theorem OAI.ExactFourier.Packing.Word.types_framed line 236
  34. def OAI.ExactFourier.Packing.Frame.word line 248
  35. theorem OAI.ExactFourier.Packing.Frame.matrix_word line 251
  36. def OAI.ExactFourier.Packing.speciesWord line 266
  37. theorem OAI.ExactFourier.Packing.speciesWord_matrix line 270
  38. def OAI.ExactFourier.Packing.standardPair line 280
  39. theorem OAI.ExactFourier.Packing.standardPair_matrix line 283
  40. def OAI.ExactFourier.Packing.pairBaseline line 287
  41. theorem OAI.ExactFourier.Packing.speciesWord_count line 291
  42. theorem OAI.ExactFourier.Packing.standardPair_count line 301
  43. structure OAI.ExactFourier.Packing.PairComparison line 306

    Source documentation

    Exact two-factor comparison; identity factors have width one and zero price.

    structure PairComparison where
…
  44. def OAI.ExactFourier.Packing.PairComparison.delta line 311
  45. abbrev OAI.ExactFourier.Packing.speciesPrice line 326
  46. def OAI.ExactFourier.Packing.pairPrice line 330
  47. theorem OAI.ExactFourier.Packing.pair_baseline_price line 334
  48. theorem OAI.ExactFourier.Packing.comparison_ineq line 348
  49. abbrev OAI.ExactFourier.Packing.singlePair line 359
  50. def OAI.ExactFourier.Packing.singleCoordinates line 360
  51. def OAI.ExactFourier.Packing.singleComparison line 366
  52. theorem OAI.ExactFourier.Packing.singleComparison_price line 375
  53. theorem OAI.ExactFourier.Packing.singleComparison_weight line 383