pith. machine review for the scientific record. sign in
def definition def or abbrev high

zeroPointEnergy

show as:
view Lean formalization →

Zero-point energy per mode with frequency ω equals ħω/2 in RS-native units. QFT researchers studying vacuum energy or Casimir effects would cite this definition as the base for fluctuation calculations. It is a direct one-line definition importing the RS value of ħ from the constants module.

claimThe zero-point energy for a mode of frequency $ω$ is $E_0 = ħω/2$, where $ħ$ is the reduced Planck constant in Recognition Science units.

background

The module derives vacuum fluctuations from the discreteness of τ₀ in Recognition Science. Empty space contains fluctuations because time is discrete at τ₀, implying energy fluctuations via the uncertainty relation at the minimal time interval. Zero-point energy represents the ground state energy of each quantum harmonic oscillator mode. The upstream definition of ħ sets it to φ^{-5} in native units, consistent with the forcing chain T5-T8. This aligns with the module's target of showing the vacuum is not empty but filled with activity from temporal discreteness.

proof idea

The declaration is a one-line definition that applies the standard formula for zero-point energy by multiplying the imported ħ by ω and dividing by 2.

why it matters in Recognition Science

It provides the energy expression used by the downstream theorem vacuum_has_energy, which establishes that zeroPointEnergy ω > 0 for ω > 0. This fills the QFT-010 objective of deriving zero-point energy from τ₀ discreteness, per the module documentation. It connects to the Recognition framework's constants derived via the eight-tick octave and phi fixed point.

scope and limits

Lean usage

theorem vacuum_has_energy (ω : ℝ) (hω : ω > 0) : zeroPointEnergy ω > 0 := by unfold zeroPointEnergy; apply div_pos; exact mul_pos hbar_pos hω

formal statement (Lean)

  65noncomputable def zeroPointEnergy (ω : ℝ) : ℝ := hbar * ω / 2

proof body

Definition body.

  66
  67/-- The vacuum state is NOT the zero-energy state.
  68    It's the minimum-energy state, with E_0 > 0 for each mode. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.