structure
definition
def or abbrev
SuperpositionJustification
show as:
view Lean formalization →
formal statement (Lean)
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. -/