`V`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SpectralEmergence on GitHub at line 81.

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

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.