`V`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SpectralEmergence
domain: Foundation
line: 81 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SpectralEmergence on GitHub at line 81.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  78gap-45 synchronization, and self-similar cost structure. -/
  79
  80/-- Vertices of the D-dimensional binary cube: |V| = 2^D. -/
  81def V (D : ℕ) : ℕ := 2 ^ D
  82
  83/-- Edges of the D-cube: |E| = D × 2^(D-1). Each vertex has D neighbors;
  84    each edge is shared between 2 vertices. -/
  85def E (D : ℕ) : ℕ := D * 2 ^ (D - 1)
  86
  87/-- 2-faces (squares) of the D-cube: each pair of coordinate axes gives
  88    a family of 2^(D-2) parallel squares. Total = C(D,2) × 2^(D-2). -/
  89def F₂ (D : ℕ) : ℕ := (D * (D - 1) / 2) * 2 ^ (D - 2)
  90
  91/-- Face pairs: opposite faces sharing a normal axis. For the D-cube,
  92    the number of 2-face pair axes equals C(D,2). -/
  93def face_pairs (D : ℕ) : ℕ := D * (D - 1) / 2
  94
  95/-- Order of the hyperoctahedral group B_D = Aut(Q_D): signed
  96    permutations of D coordinate axes. |B_D| = 2^D × D!. -/
  97def aut_order (D : ℕ) : ℕ := 2 ^ D * Nat.factorial D
  98
  99/-! ### Q₃-Specific Values (D = 3) -/
 100
 101theorem Q3_vertices : V 3 = 8 := by norm_num [V]
 102theorem Q3_edges : E 3 = 12 := by norm_num [E]
 103theorem Q3_faces : F₂ 3 = 6 := by native_decide
 104theorem Q3_face_pairs : face_pairs 3 = 3 := by native_decide
 105theorem Q3_aut_order : aut_order 3 = 48 := by norm_num [aut_order, Nat.factorial]
 106
 107/-- Euler characteristic of the Q₃ surface: V + F = E + 2 (sphere).
 108    Written as V + F = E + 2 to avoid natural subtraction underflow. -/
 109theorem Q3_euler_characteristic : V 3 + F₂ 3 = E 3 + 2 := by native_decide
 110
 111/-- The Q₃ cube is self-dual: the number of vertices equals the number

papers checked against this theorem

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