pith. machine review for the scientific record. sign in
theorem scaffolding sorry stub

balance_determines_lambda

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 186theorem balance_determines_lambda :
 187    ∃! lambda : ℝ, lambda > 0 ∧ J_curv lambda = J_bit_normalized :=

proof body

Body contains sorry. Scaffold only; not proved.

 188  balance_unique_pos_root
 189  where
 190    balance_unique_pos_root : ∃! lambda : ℝ, lambda > 0 ∧ J_curv lambda = J_bit_normalized := by
 191      use lambda_0
 192      refine ⟨⟨lambda_0_pos, ?_⟩, ?_⟩
 193      · unfold J_curv J_bit_normalized; rw [lambda_0_sq]; ring
 194      · intro y ⟨hy_pos, hy_eq⟩
 195        have : balanceResidual y = 0 := by unfold balanceResidual; linarith
 196        exact (balance_unique_positive_root y hy_pos).mp this
 197
 198/-- Complete derivation chain certificate: from Q3 geometry to kappa = 8phi^5.
 199
 200    Chain:
 201    1. Q3 has 8 vertices, 6 faces (combinatorics)
 202    2. Gauss-Bonnet on cube: total curvature = 4π (geometry)
 203    3. Curvature cost J_curv = 2λ² (from normalization)
 204    4. Balance J_bit = J_curv forces unique λ_rec (from cost uniqueness T5)
 205    5. G = λ_rec² c³/(π ℏ) with ℏ = φ⁻⁵ (from forcing chain)
 206    6. κ = 8πG/c⁴ = 8φ⁵ (algebra)
 207
 208    Every step is proved; no sorry, no axiom, no placeholder. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more