OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound19.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1216 line 50
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1216 line 56
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1216 line 58
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1217 line 88
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1217 line 94
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1217 line 96
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1218 line 126
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1218 line 132
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1218 line 134
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1219 line 164
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1219 line 170
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1219 line 172
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1220 line 203
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1220 line 209
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1220 line 211
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1221 line 241
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1221 line 247
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1221 line 249
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1222 line 279
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1222 line 285
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1222 line 287
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1223 line 318
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1223 line 324
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1223 line 326
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1224 line 357
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1224 line 363
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1224 line 365
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1225 line 396
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1225 line 402
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1225 line 404
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1226 line 434
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1226 line 440
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1226 line 442
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1227 line 473
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1227 line 479
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1227 line 481
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1228 line 511
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1228 line 517
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1228 line 519
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1229 line 549
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1229 line 555
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1229 line 557
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1230 line 588
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1230 line 594
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1230 line 596
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1231 line 627
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1231 line 633
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1231 line 635
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1232 line 665
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1232 line 671
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1232 line 673
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1233 line 703
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1233 line 709
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1233 line 711
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1234 line 742
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1234 line 748
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1234 line 750
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1235 line 781
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1235 line 787
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1235 line 789
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1236 line 820
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1236 line 826
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1236 line 828
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1237 line 859
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1237 line 865
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1237 line 867
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1238 line 898
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1238 line 904
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1238 line 906
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1239 line 937
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1239 line 943
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1239 line 945
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1240 line 976
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1240 line 982
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1240 line 984
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1241 line 1015
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1241 line 1021
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1241 line 1023
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1242 line 1053
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1242 line 1059
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1242 line 1061
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1243 line 1091
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1243 line 1097
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1243 line 1099
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1244 line 1129
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1244 line 1135
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1244 line 1137
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1245 line 1168
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1245 line 1174
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1245 line 1176
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1246 line 1206
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1246 line 1212
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1246 line 1214
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1247 line 1244
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1247 line 1250
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1247 line 1252
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1248 line 1283
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1248 line 1289
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1248 line 1291
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1249 line 1322
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1249 line 1328
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1249 line 1330
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1250 line 1361
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1250 line 1367
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1250 line 1369
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1251 line 1400
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1251 line 1406
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1251 line 1408
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1252 line 1439
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1252 line 1445
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1252 line 1447
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1253 line 1477
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1253 line 1483
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1253 line 1485
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1254 line 1516
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1254 line 1522
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1254 line 1524
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1255 line 1555
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1255 line 1561
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1255 line 1563
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1256 line 1594
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1256 line 1600
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1256 line 1602
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1257 line 1633
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1257 line 1639
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1257 line 1641
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1258 line 1672
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1258 line 1678
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1258 line 1680
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1259 line 1711
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1259 line 1717
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1259 line 1719
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1260 line 1749
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1260 line 1755
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1260 line 1757
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1261 line 1787
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1261 line 1793
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1261 line 1795
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1262 line 1825
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1262 line 1831
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1262 line 1833
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1263 line 1863
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1263 line 1869
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1263 line 1871
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1264 line 1902
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1264 line 1908
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1264 line 1910
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1265 line 1940
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1265 line 1946
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1265 line 1948
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1266 line 1978
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1266 line 1984
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1266 line 1986
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1267 line 2017
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1267 line 2023
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1267 line 2025
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1268 line 2055
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1268 line 2061
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1268 line 2063
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1269 line 2093
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1269 line 2099
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1269 line 2101
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1270 line 2132
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1270 line 2138
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1270 line 2140
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1271 line 2171
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1271 line 2177
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1271 line 2179
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1272 line 2210
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1272 line 2216
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1272 line 2218
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1273 line 2249
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1273 line 2255
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1273 line 2257
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1274 line 2288
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1274 line 2294
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1274 line 2296
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1275 line 2327
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1275 line 2333
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1275 line 2335
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1276 line 2366
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1276 line 2372
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1276 line 2374
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1277 line 2405
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1277 line 2411
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1277 line 2413
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1278 line 2444
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1278 line 2450
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1278 line 2452
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1279 line 2483
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1279 line 2489
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1279 line 2491