IndisputableMonolith.CrossDomain.TwoCubeUniversality

declarations in this module (18)

• def HasTwoCubeCount L28
• inductive DFTMode L32
• inductive Q3Vertex L36
• inductive PauliElement L40
• inductive TickPhase L44
• theorem dft_has_2cube L48
• theorem q3_has_2cube L50
• theorem pauli_has_2cube L52
• theorem tick_has_2cube L54
• theorem two_cube_equicardinal L60
• theorem two_cube_pair_64 L68
• theorem two_cube_powerset_256 L76
• theorem dft_q3_equicardinal L82
• theorem pauli_tick_equicardinal L87
• theorem dft_q3_product L92
• theorem sixtyfour_identities L97
• structure TwoCubeUniversalityCert L99
• def twoCubeUniversalityCert L110