`twoCubeUniversalityCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.TwoCubeUniversality
domain: CrossDomain
line: 110 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.TwoCubeUniversality on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 107  pair_64 : Fintype.card (DFTMode × Q3Vertex) = 64
 108  sixtyfour_identities : 64 = 8 * 8 ∧ 64 = 2^6
 109
 110def twoCubeUniversalityCert : TwoCubeUniversalityCert where
 111  dft_is_2cube := dft_has_2cube
 112  q3_is_2cube := q3_has_2cube
 113  pauli_is_2cube := pauli_has_2cube
 114  tick_is_2cube := tick_has_2cube
 115  all_equicardinal := fun _ _ _ _ => two_cube_equicardinal
 116  pair_64 := dft_q3_product
 117  sixtyfour_identities := sixtyfour_identities
 118
 119end IndisputableMonolith.CrossDomain.TwoCubeUniversality

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.