def definition def or abbrev

`levelEnergy`

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

formal statement (Lean)

  22def levelEnergy (n δ : ℤ) : ℝ :=

proof body

Definition body.

  23  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ) + (δ : ℝ))
  24
  25/‑ Sliding 8‑window sum over an occupancy/cost proxy `x`. -/

used by (1)

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

isClosure in IndisputableMonolith.Nuclear.Octave decl_use

depends on (3)

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use