def definition def or abbrev

`lambda_rec_SI`

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

formal statement (Lean)

 208noncomputable def lambda_rec_SI : ℝ := sqrt (hbar * G / (Real.pi * c^3))

Definition body.

 209
 210/-- λ_rec_SI > 0. -/

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

lambda_rec_over_ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_SI_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
PlanckScaleMatchingCert in IndisputableMonolith.Constants.PlanckScaleMatching 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
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use