`cube_faces`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaDerivation
domain: Constants
line: 57 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 57.

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

  54def cube_edges (d : ℕ) : ℕ := d * 2^(d - 1)
  55
  56/-- Number of faces in the D-hypercube: 2D. -/
  57def cube_faces (d : ℕ) : ℕ := 2 * d
  58
  59/-- For D=3: vertices = 8 -/
  60theorem vertices_at_D3 : cube_vertices D = 8 := by native_decide
  61
  62/-- For D=3: edges = 12 -/
  63theorem edges_at_D3 : cube_edges D = 12 := by native_decide
  64
  65/-- For D=3: faces = 6 -/
  66theorem faces_at_D3 : cube_faces D = 6 := by native_decide
  67
  68/-! ## Part 2: Active vs Passive Edge Counting -/
  69
  70/-- Active edges per atomic tick (one edge transition per tick by T2). -/
  71def active_edges_per_tick : ℕ := 1
  72
  73/-- Passive (field) edges: total edges minus active edge.
  74    These are the edges that "dress" the interaction. -/
  75def passive_field_edges (d : ℕ) : ℕ := cube_edges d - active_edges_per_tick
  76
  77/-- The key number: for D=3, passive edges = 11. -/
  78theorem passive_edges_at_D3 : passive_field_edges D = 11 := by native_decide
  79
  80/-! ## Part 3: Structural Derivation of 4π from Q₃ Gauss-Bonnet
  81
  82The factor 4π in the geometric seed is NOT an imported property of the
  83abstract unit sphere — it is the total Gaussian curvature of ∂Q₃, the
  84boundary of the 3-cube, derived from vertex deficit angles via the
  85discrete Gauss-Bonnet theorem.
  86
  87### Why 4π appears in a theory built on 3-cubes

papers checked against this theorem

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