SuperpositionJustification

formal source

  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 →
 110    DifferentiableAt ℝ pair.field_ext.phi h0 →
 111    deriv pair.combined.phi h0 =
 112    deriv pair.field_grav.phi h0 + deriv pair.field_ext.phi h0
 113  /-- The combined coherence defect respects superposition -/
 114  coherence_defect_additivity :
 115    ∀ (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ),
 116    DifferentiableAt ℝ pair.field_grav.phi obj.h_cm →
 117    DifferentiableAt ℝ pair.field_ext.phi obj.h_cm →
 118    coherence_defect pair.combined obj a =
 119    abs (2 * obj.extent *
 120      (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a))
 121
 122/-- The weak-field superposition principle is proved from RS first principles. -/
 123theorem superposition_justified : SuperpositionJustification where
 124  quadratic_regime := Jcost_one_plus_exact
 125  gradient_additivity := gradient_superposition
 126  coherence_defect_additivity := coherence_defect_of_combined
 127
 128end IndisputableMonolith.Gravity.WeakFieldSuperposition