OAI/Computability/FourierCircuit/GraphBlocks.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.GraphReflection.block_relations line 10
  2. theorem OAI.ExactFourier.GraphReflection.offdiagonal_unit line 25
  3. theorem OAI.ExactFourier.GraphReflection.diagonalization line 61
  4. theorem OAI.ExactFourier.GraphReflection.lower_bound_blocks line 90
  5. def OAI.ExactFourier.SignedBits.weight line 132
  6. theorem OAI.ExactFourier.SignedBits.D_weight line 137
  7. def OAI.ExactFourier.SignedBits.V line 151
  8. def OAI.ExactFourier.SignedBits.Vi line 152
  9. def OAI.ExactFourier.SignedBits.X line 153
  10. theorem OAI.ExactFourier.SignedBits.ViV line 155
  11. theorem OAI.ExactFourier.SignedBits.XX line 156
  12. theorem OAI.ExactFourier.SignedBits.V_monomial line 157
  13. theorem OAI.ExactFourier.SignedBits.Vi_monomial line 161
  14. theorem OAI.ExactFourier.SignedBits.X_monomial line 165
  15. def OAI.ExactFourier.SignedBits.gauge line 169
  16. def OAI.ExactFourier.SignedBits.Q line 171
  17. theorem OAI.ExactFourier.SignedBits.gauge_monomial line 173
  18. theorem OAI.ExactFourier.SignedBits.blockDiagonal_mul_apply line 176
  19. theorem OAI.ExactFourier.SignedBits.mul_blockDiagonal_apply line 182
  20. theorem OAI.ExactFourier.SignedBits.gauge_intertwine line 188
  21. theorem OAI.ExactFourier.SignedBits.Q_unit line 202
  22. theorem OAI.ExactFourier.SignedBits.Q_price line 210
  23. theorem OAI.ExactFourier.SignedBits.Gamma_Q line 230
  24. theorem OAI.ExactFourier.SignedBits.Gamma_price line 237
  25. theorem OAI.ExactFourier.reflection_inequality line 258
  26. theorem OAI.ExactFourier.no_matrixPrice line 310
  27. theorem OAI.ExactFourier.finite_win line 324

    Source documentation

    The missing finite-win theorem, from exact comparison packing and the sparse reflection contradiction. No global price is taken as an assumption.

    theorem finite_win : FiniteWinStatement := by
…

    Mentions: OAI.ExactFourier.FiniteWinStatement

  28. inductive OAI.ExactFourier.Layered line 338

    Source documentation

    Exact-width mixed rounds. Monomial rounds are counted, not silently free scalar multiplications. Disjoint parallel blocks share a round.

    inductive Layered : {α : Type} → [Fintype α] → [DecidableEq α] → Matrix α α ℂ → ℕ → Prop
 | identity {α : Type} [Fintype α] [DecidableEq α] : Layered (1 : Matrix α α ℂ) 0
 | mono {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ)
   (hM : MonomialMatrix M) : Layered M 1
 | pair (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : IsUnit M) : Layered M 1
 | mul {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d e : ℕ}
   (hM : Layered M d) (hN : Layered N e) : Layered (M*N) (d+e)
 | reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
   (f : α≃β) {M : Matrix α α ℂ} {d : ℕ} (hM : Layered M d) :
   Layered (Matrix.reindex f f M) d
 | sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
   {M : Matrix α α ℂ} {N : Matrix β β ℂ} {d : ℕ}
…

    Mentions: OAI.ExactFourier.MonomialMatrix

  29. theorem OAI.ExactFourier.Layered.unit line 356
  30. theorem OAI.ExactFourier.Layered.parallel line 366
  31. theorem OAI.ExactFourier.Layered.embed line 371