`D`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 48.

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

  45/-! ## Part 1: Cube Combinatorics -/
  46
  47/-- The spatial dimension forced by T9 (linking requires D=3). -/
  48def D : ℕ := 3
  49
  50/-- Number of vertices in the D-hypercube: 2^D. -/
  51def cube_vertices (d : ℕ) : ℕ := 2^d
  52
  53/-- Number of edges in the D-hypercube: D · 2^(D-1). -/
  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

papers checked against this theorem

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