OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound32.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2048 line 96
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2048 line 102
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2048 line 104
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2049 line 139
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2049 line 145
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2049 line 147
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2050 line 182
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2050 line 188
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2050 line 190
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2051 line 225
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2051 line 231
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2051 line 233
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2052 line 268
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2052 line 274
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2052 line 276
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2053 line 311
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2053 line 317
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2053 line 319
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2054 line 354
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2054 line 360
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2054 line 362
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2055 line 397
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2055 line 403
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2055 line 405
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2056 line 440
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2056 line 446
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2056 line 448
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2057 line 483
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2057 line 489
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2057 line 491
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2058 line 526
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2058 line 532
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2058 line 534
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2059 line 569
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2059 line 575
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2059 line 577
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2060 line 612
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2060 line 618
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2060 line 620
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2061 line 655
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2061 line 661
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2061 line 663
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2062 line 698
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2062 line 704
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2062 line 706
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2063 line 741
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2063 line 747
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2063 line 749
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2064 line 784
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2064 line 790
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2064 line 792
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2065 line 827
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2065 line 833
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2065 line 835
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2066 line 870
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2066 line 876
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2066 line 878
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2067 line 913
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2067 line 919
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2067 line 921
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2068 line 956
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2068 line 962
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2068 line 964
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2069 line 999
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2069 line 1005
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2069 line 1007
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2070 line 1042
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2070 line 1048
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2070 line 1050
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2071 line 1085
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2071 line 1091
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2071 line 1093
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2072 line 1128
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2072 line 1134
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2072 line 1136
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2073 line 1171
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2073 line 1177
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2073 line 1179
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2074 line 1214
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2074 line 1220
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2074 line 1222
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2075 line 1257
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2075 line 1263
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2075 line 1265
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2076 line 1300
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2076 line 1306
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2076 line 1308
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2077 line 1343
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2077 line 1349
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2077 line 1351
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2078 line 1386
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2078 line 1392
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2078 line 1394
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2079 line 1429
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2079 line 1435
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2079 line 1437
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2080 line 1472
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2080 line 1478
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2080 line 1480
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2081 line 1515
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2081 line 1521
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2081 line 1523
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2082 line 1558
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2082 line 1564
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2082 line 1566
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2083 line 1601
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2083 line 1607
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2083 line 1609
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2084 line 1644
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2084 line 1650
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2084 line 1652
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2085 line 1687
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2085 line 1693
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2085 line 1695
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2086 line 1730
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2086 line 1736
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2086 line 1738
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2087 line 1773
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2087 line 1779
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2087 line 1781
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2088 line 1816
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2088 line 1822
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2088 line 1824
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2089 line 1859
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2089 line 1865
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2089 line 1867
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2090 line 1907
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2090 line 1913
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2090 line 1915
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2091 line 1955
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2091 line 1961
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2091 line 1963
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2092 line 2003
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2092 line 2009
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2092 line 2011
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2093 line 2051
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2093 line 2057
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2093 line 2059
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2094 line 2099
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2094 line 2105
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2094 line 2107
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2095 line 2147
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2095 line 2153
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2095 line 2155
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2096 line 2195
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2096 line 2201
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2096 line 2203
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2097 line 2243
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2097 line 2249
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2097 line 2251
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2098 line 2291
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2098 line 2297
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2098 line 2299
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2099 line 2339
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2099 line 2345
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2099 line 2347
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2100 line 2387
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2100 line 2393
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2100 line 2395
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2101 line 2435
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2101 line 2441
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2101 line 2443
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2102 line 2483
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2102 line 2489
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2102 line 2491
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2103 line 2531
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2103 line 2537
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2103 line 2539
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2104 line 2579
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2104 line 2585
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2104 line 2587
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2105 line 2627
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2105 line 2633
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2105 line 2635
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2106 line 2675
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2106 line 2681
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2106 line 2683
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2107 line 2723
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2107 line 2729
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2107 line 2731
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2108 line 2771
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2108 line 2777
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2108 line 2779
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2109 line 2819
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2109 line 2825
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2109 line 2827
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2110 line 2867
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2110 line 2873
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2110 line 2875
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2111 line 2915
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2111 line 2921
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2111 line 2923