Q3_faces

formal source

 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 -/
 144
 145/-- **THE EXTREMUM EQUATION**: J_bit = J_curv(λ).
 146