pith. machine review for the scientific record. sign in
structure definition def or abbrev

GDerivationChain

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)

 209structure GDerivationChain where
 210  step1_Q3_vertices : Q3_vertices = 8
 211  step2_gauss_bonnet : Q3_vertices * angular_deficit_per_vertex = 2 * Real.pi * euler_S2
 212  step3_J_curv_formula : ∀ λ, J_curv λ = 2 * λ ^ 2
 213  step4_balance_unique : ∃! λ, λ > 0 ∧ J_curv λ = J_bit_normalized
 214  step5_G_formula : Constants.G = (Constants.lambda_rec^2) * (Constants.c^3) / (Real.pi * Constants.hbar)
 215  step6_kappa : Constants.kappa_einstein = 8 * Constants.phi ^ (5 : ℝ)
 216

used by (1)

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

depends on (22)

Lean names referenced from this declaration's body.