superposition_cross_term

formal source

  47/-- The cross-term in the additive decomposition.
  48    J(1 + ε₁ + ε₂) - J(1 + ε₁) - J(1 + ε₂) is the non-linear correction.
  49    In the exact form: this equals ε₁·ε₂ times a bounded factor. -/
  50def superposition_cross_term (ε₁ ε₂ : ℝ) : ℝ :=
  51  Jcost (1 + (ε₁ + ε₂)) - Jcost (1 + ε₁) - Jcost (1 + ε₂)
  52
  53/-- The cross-term is exactly ε₁·ε₂ times a rational function of the strains. -/
  54theorem cross_term_factored (ε₁ ε₂ : ℝ)
  55    (h1 : -(1 : ℝ) < ε₁) (h2 : -(1 : ℝ) < ε₂) (h12 : -(1 : ℝ) < ε₁ + ε₂) :
  56    superposition_cross_term ε₁ ε₂ =
  57      (ε₁ + ε₂) ^ 2 / (2 * (1 + (ε₁ + ε₂))) -
  58      ε₁ ^ 2 / (2 * (1 + ε₁)) -
  59      ε₂ ^ 2 / (2 * (1 + ε₂)) := by
  60  unfold superposition_cross_term
  61  rw [Jcost_one_plus_exact _ h12, Jcost_one_plus_exact _ h1, Jcost_one_plus_exact _ h2]
  62
  63/-! ## 2. Weak-Field Superposition for Processing Fields -/
  64
  65/-- Two independent processing fields (gravitational + external).
  66    In the weak-field regime, their combined effect is their sum. -/
  67structure WeakFieldPair where
  68  field_grav : ProcessingField
  69  field_ext : ProcessingField
  70
  71/-- The combined processing field: pointwise addition. -/
  72def WeakFieldPair.combined (pair : WeakFieldPair) : ProcessingField where
  73  phi h := pair.field_grav.phi h + pair.field_ext.phi h
  74
  75/-- SUPERPOSITION THEOREM: In the weak-field regime, the gradient of the combined
  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)