def definition def or abbrev

`planckLength`

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

formal statement (Lean)

  51noncomputable def planckLength : ℝ := 1.6e-35  -- meters

Definition body.

  52
  53/-- Planck area = l_P². -/

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

planckArea in IndisputableMonolith.Quantum.BekensteinHawking decl_use
planckLength in IndisputableMonolith.Quantum.BekensteinHawking decl_use
planckArea in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
planckLength in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
planckArea in IndisputableMonolith.Quantum.HolographicBound decl_use
planckLength in IndisputableMonolith.Quantum.PlanckScale decl_use
planckArea_pos in IndisputableMonolith.Unification.RecognitionBandwidth decl_use

Lean names referenced from this declaration's body.