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)
195theorem ell_P_pos : ell_P > 0 := by
proof body
Term-mode proof.
196 unfold ell_P
197 apply sqrt_pos.mpr
198 apply div_pos
199 · exact mul_pos hbar_pos G_pos
200 · exact pow_pos c_pos 3
201
202/-- **THE PLANCK GATE IDENTITY**:
203
204λ_rec = √(ℏG/(πc³)) = ℓ_P / √π
205
206This follows from the face-averaging principle applied to the
207curvature extremum. -/
depends on (15)
Lean names referenced from this declaration's body.
-
applied
in IndisputableMonolith.Action.EnergyConservationDomainCert
decl_use
-
c_pos
in IndisputableMonolith.Constants
decl_use
-
G
in IndisputableMonolith.Constants
decl_use
-
G_pos
in IndisputableMonolith.Constants
decl_use
-
hbar_pos
in IndisputableMonolith.Constants
decl_use
-
c_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
G
in IndisputableMonolith.Constants.Codata
decl_use
-
G_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
hbar_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
ell_P
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
G
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
c_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
G_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
G
in IndisputableMonolith.Gravity.JCostInflaton
decl_use