ExternalPhaseField

formal source

  60/-- An external phase/acoustic field that contributes its own processing potential.
  61    This represents any mechanism (acoustic standing waves, rotating superconductors,
  62    phase-locked electromagnetic fields) that modifies the local processing environment. -/
  63structure ExternalPhaseField where
  64  psi : Position → ℝ
  65
  66/-- The gradient of the external field at a given position. -/
  67def ExternalPhaseField.gradient (ext : ExternalPhaseField) (h : Position) : ℝ :=
  68  deriv ext.psi h
  69
  70/-! ## 2. Modified Coherence Defect -/
  71
  72/-- Total potential when BOTH gravitational and external phase fields are present,
  73    in a frame accelerating with `a`.
  74    Φ_total(z) = Φ_grav(h_cm + z) + Φ_ext(h_cm + z) + a·z
  75    (linearized around center of mass) -/
  76def modified_total_potential
  77    (field : ProcessingField) (ext : ExternalPhaseField)
  78    (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
  79  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  80  let phi_ext := ext.psi obj.h_cm + (deriv ext.psi obj.h_cm) * z
  81  let phi_acc := a * z
  82  phi_grav + phi_ext + phi_acc
  83
  84/-- Modified coherence defect with external phase field present. -/
  85def modified_coherence_defect
  86    (field : ProcessingField) (ext : ExternalPhaseField)
  87    (obj : ExtendedObject) (a : ℝ) : ℝ :=
  88  let pot_head := modified_total_potential field ext obj a obj.extent
  89  let pot_feet := modified_total_potential field ext obj a (-obj.extent)
  90  abs (pot_head - pot_feet)
  91
  92/-- Helper: expand modified_coherence_defect into explicit arithmetic. -/
  93private lemma modified_coherence_defect_expand