passiveFraction

formal source

  23open Constants
  24
  25/-- Fraction of phase-locked modes from Q₃ mode budget. -/
  26noncomputable def passiveFraction : ℝ := 11 / 16
  27
  28theorem passive_fraction_pos : passiveFraction > 0 := by
  29  unfold passiveFraction; norm_num
  30
  31theorem passive_fraction_lt_one : passiveFraction < 1 := by
  32  unfold passiveFraction; norm_num
  33
  34/-- Active fraction complements passive to 1. -/
  35noncomputable def activeFraction : ℝ := 1 - passiveFraction
  36
  37theorem fractions_sum : passiveFraction + activeFraction = 1 := by
  38  unfold activeFraction; ring
  39
  40/-- Voxel symmetry: no distinguished location on the carrier.
  41    This is the ℤ³ translation invariance from VoxelSymmetry. -/
  42structure VoxelSymmetric (f : ℤ × ℤ × ℤ → ℝ) : Prop where
  43  shift_invariant : ∀ (v d : ℤ × ℤ × ℤ), f (v.1 + d.1, v.2.1 + d.2.1, v.2.2 + d.2.2) = f v
  44
  45/-- Phase-locked energy is constant per voxel. -/
  46noncomputable def phaseLockEnergy : ℝ := passiveFraction * E_coh
  47
  48/-- The vacuum energy density function is spatially uniform. -/
  49theorem vacuum_energy_uniform :
  50    VoxelSymmetric (fun _ => phaseLockEnergy) :=
  51  ⟨fun _ _ => rfl⟩
  52
  53/-- The vacuum J-cost is non-negative (since passiveFraction > 0 and E_coh > 0). -/
  54theorem vacuum_energy_pos : phaseLockEnergy > 0 := by
  55  unfold phaseLockEnergy
  56  exact mul_pos passive_fraction_pos E_coh_pos