theorem
proved
Q3_vertices
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 122.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
cube_vertices -
Q3_vertices -
J_curv -
Q3_vertices -
cube_vertices -
J_curv -
of -
A -
cost -
cost -
is -
of -
is -
of -
Q3_vertices -
is -
of -
A -
is -
A -
total -
total -
Q3_vertices -
cube_vertices
used by
formal source
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
147Solving for λ: J_bit = 2λ² ⟹ λ = √(J_bit/2). -/
148noncomputable def lambda_rec_from_Jbit : ℝ := sqrt (J_bit_val / 2)
149
150/-- λ_rec_from_Jbit > 0 since J_bit > 0. -/
151theorem lambda_rec_from_Jbit_pos : lambda_rec_from_Jbit > 0 := by
152 unfold lambda_rec_from_Jbit