OAI/Algebra/DepthFive/UpperBlockData.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem335.BlockData.Middle line 14

   Source documentation

   Block-entry gates: block number and two matrix indices.

   abbrev Middle (blocks : List (List (Fin n))) :=
   …

2. def OAI.Problem335.BlockData.paths line 17
3. abbrev OAI.Problem335.BlockData.Lower line 21

   Source documentation

   Each lower gate is an enumerated path for one block entry.

   abbrev Lower (blocks : List (List (Fin n))) :=
   …

4. def OAI.Problem335.BlockData.lowerInputs line 24
5. def OAI.Problem335.BlockData.middleInputs line 28
6. def OAI.Problem335.BlockData.middleDegree line 32
7. def OAI.Problem335.BlockData.upperPaths line 35
8. abbrev OAI.Problem335.BlockData.Upper line 39
9. def OAI.Problem335.BlockData.upperInputs line 42
10. def OAI.Problem335.BlockData.outputInputs line 46
11. theorem OAI.Problem335.BlockData.lowerInputs_labels line 50
12. theorem OAI.Problem335.BlockData.lowerInputs_length line 54
13. theorem OAI.Problem335.BlockData.middleInputs_homogeneous line 58
14. theorem OAI.Problem335.BlockData.upperInputs_labels line 65
15. theorem OAI.Problem335.BlockData.upperInputs_degree line 70
16. theorem OAI.Problem335.BlockData.paths_length line 81
17. theorem OAI.Problem335.BlockData.middleInputs_ne_nil line 86
18. theorem OAI.Problem335.BlockData.upperPaths_length line 94
19. theorem OAI.Problem335.BlockData.outputInputs_ne_nil line 100
20. theorem OAI.Problem335.BlockData.card_middle line 108
21. theorem OAI.Problem335.BlockData.card_upper line 112
22. theorem OAI.Problem335.BlockData.card_lower line 116
23. theorem OAI.Problem335.BlockData.card_lower_le line 130