gradient_superposition

formal source

  76    field equals the sum of the individual gradients.
  77
  78    This is the key result that justifies the linear addition in CoherenceFall. -/
  79theorem gradient_superposition (pair : WeakFieldPair) (h0 : Position)
  80    (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi h0)
  81    (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi h0) :
  82    deriv pair.combined.phi h0 =
  83    deriv pair.field_grav.phi h0 + deriv pair.field_ext.phi h0 := by
  84  simp only [WeakFieldPair.combined]
  85  exact deriv_add h_diff_grav h_diff_ext
  86
  87/-- COHERENCE DEFECT SUPERPOSITION: The coherence defect of the combined field
  88    decomposes as expected from the sum of gradients. -/
  89theorem coherence_defect_of_combined (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ)
  90    (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi obj.h_cm)
  91    (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi obj.h_cm) :
  92    coherence_defect pair.combined obj a =
  93    abs (2 * obj.extent *
  94      (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a)) := by
  95  rw [coherence_defect_simplify]
  96  congr 1; congr 1; congr 1
  97  exact gradient_superposition pair obj.h_cm h_diff_grav h_diff_ext
  98
  99/-! ## 3. The Superposition Justification Certificate -/
 100
 101/-- Structure packaging the full weak-field superposition justification. -/
 102structure SuperpositionJustification where
 103  /-- J-cost is exactly quadratic near balance -/
 104  quadratic_regime :
 105    ∀ ε : ℝ, -1 < ε → Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε))
 106  /-- Processing field gradients add linearly -/
 107  gradient_additivity :
 108    ∀ (pair : WeakFieldPair) (h0 : Position),
 109    DifferentiableAt ℝ pair.field_grav.phi h0 →