fractions_sum

formal source

  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
  57
  58/-- Master certificate. -/
  59structure VacuumUniformityCert where
  60  passive_frac : passiveFraction = 11 / 16
  61  fracs_sum : passiveFraction + activeFraction = 1
  62  energy_pos : phaseLockEnergy > 0
  63  uniform : VoxelSymmetric (fun _ => phaseLockEnergy)
  64
  65noncomputable def vacuumUniformityCert : VacuumUniformityCert where
  66  passive_frac := rfl
  67  fracs_sum := fractions_sum