`cube_faces`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.PlanckScaleMatching
domain: Constants
line: 113 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 113.

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

 110/-! ## Part 2: Curvature Cost from Q₃ Geometry -/
 111
 112/-- The number of faces of the D-hypercube (D-cube). F = 2D. -/
 113def cube_faces (D : ℕ) : ℕ := 2 * D
 114
 115/-- The 3-cube Q₃ has 6 faces. -/
 116theorem Q3_faces : cube_faces 3 = 6 := rfl
 117
 118/-- The number of vertices of the D-hypercube. V = 2^D. -/
 119def cube_vertices (D : ℕ) : ℕ := 2^D
 120
 121/-- The 3-cube Q₃ has 8 vertices (= 8 ticks in the Gray cycle). -/
 122theorem Q3_vertices : cube_vertices 3 = 8 := rfl
 123
 124/-- **Curvature Packet Axiom** (PHYSICAL HYPOTHESIS):
 125
 126A ±4 curvature packet is distributed over the 8 vertices of Q₃.
 127The curvature cost per vertex is proportional to λ²/4.
 128
 129The total curvature cost is then 8 × (λ²/4) = 2λ².
 130
 131This is the curvature functional J_curv(λ). -/
 132noncomputable def J_curv (lam : ℝ) : ℝ := 2 * lam^2
 133
 134/-- J_curv(0) = 0. -/
 135theorem J_curv_zero : J_curv 0 = 0 := by simp [J_curv]
 136
 137/-- J_curv is non-negative. -/
 138theorem J_curv_nonneg (lam : ℝ) : J_curv lam ≥ 0 := by
 139  unfold J_curv
 140  have h : lam^2 ≥ 0 := sq_nonneg lam
 141  linarith
 142
 143/-! ## Part 3: Curvature Extremum Condition -/

papers checked against this theorem

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