OAI/Analysis/MatrixSigning/Complexity/PolynomialFaceOrbit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CurrentKS.Realization.FaceParams.GoodAtoms line 16
2. def OAI.CurrentKS.Realization.FaceParams.normal line 24
3. def OAI.CurrentKS.Realization.FaceParams.orbit line 26
4. lemma OAI.CurrentKS.Realization.orbit_eq line 28
5. lemma OAI.CurrentKS.Realization.orbit_count_le line 35
6. lemma OAI.CurrentKS.Realization.normal_fuel_bound line 38
7. lemma OAI.CurrentKS.Realization.orbit_query_bounds line 44
8. lemma OAI.CurrentKS.Realization.qparts_bitSize line 55
9. lemma OAI.CurrentKS.Realization.faceCode_base_bound line 59
10. lemma OAI.CurrentKS.Realization.orbit_wire_bound line 63
11. lemma OAI.CurrentKS.Realization.isPoly_face_dimensions line 86
12. lemma OAI.CurrentKS.Realization.isPoly_face_orbit line 94