equilibrium_acceleration

formal source

 157  simp only [add_neg_cancel, add_zero, mul_zero, abs_zero]
 158
 159/-- The equilibrium acceleration under a modified field is -(∇Φ_grav + ∇Φ_ext). -/
 160def equilibrium_acceleration
 161    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) : ℝ :=
 162  -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm)
 163
 164/-- At the equilibrium acceleration, coherence defect is zero. -/
 165theorem equilibrium_is_coherent
 166    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) :
 167    modified_coherence_defect field ext obj (equilibrium_acceleration field ext obj) = 0 := by
 168  rw [modified_coherence_defect_simplify]
 169  unfold equilibrium_acceleration
 170  have : deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm +
 171         -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm) = 0 := by ring
 172  rw [this, mul_zero, abs_zero]
 173
 174/-! ## 4. Anti-Coherence Reduces Gravitational Coupling -/
 175
 176/-- Effective gravitational coupling: the magnitude of the equilibrium acceleration.
 177    Without external field: |a_eq| = |∇Φ_grav|.
 178    With external field: |a_eq| = |∇Φ_grav + ∇Φ_ext|. -/
 179def effective_gravitational_coupling
 180    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) : ℝ :=
 181  |deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm|
 182
 183/-- Baseline gravitational coupling (no external field). -/
 184def baseline_gravitational_coupling
 185    (field : ProcessingField) (obj : ExtendedObject) : ℝ :=
 186  |deriv field.phi obj.h_cm|
 187
 188/-- ANTI-COHERENCE COUPLING REDUCTION: When the external field gradient opposes the
 189    gravitational gradient (anti-coherence), the effective coupling is reduced.
 190