def definition def or abbrev

`ell_P`

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

formal statement (Lean)

 192noncomputable def ell_P : ℝ := sqrt (hbar * G / c^3)

Definition body.

 193
 194/-- The Planck length is positive. -/

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

ell_P_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_over_ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
PlanckScaleMatchingCert in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use