gradient_superposition
The theorem shows that at any position where both are differentiable, the derivative of the combined gravitational-plus-external processing field equals the sum of the separate derivatives. Workers on weak-field coherence models in Recognition Science cite it to license linear addition when computing defects. The proof is a one-line term wrapper that unfolds the combined-field definition and applies the standard derivative-additivity lemma.
claimLet $P$ be a pair of independent gravitational and external processing fields. At a position $h_0$ where both fields are differentiable, the derivative of the combined field at $h_0$ equals the sum of the individual field derivatives.
background
The WeakFieldPair structure consists of two independent processing fields (gravitational and external) whose combined field is defined by pointwise addition of their phi functions. This construction lives inside the weak-field regime of the Gravity module and supplies the linear-addition step required by CoherenceFall calculations. Upstream results include the defect functional (equal to J for positive arguments) from LawOfExistence, the J-cost structures from PhiForcingDerived, and the continuum-bridge identification from SimplicialLedger that together ground the field definitions and the differentiability hypotheses.
proof idea
The term proof first simplifies the combined-field definition to expose the explicit sum of the two phi functions, then applies the exact derivative-additivity rule under the supplied differentiability assumptions.
why it matters in Recognition Science
The result supplies the gradient-additivity clause inside the SuperpositionJustification record, which is then used to prove coherence-defect additivity for combined fields. It therefore closes the justification for linear superposition in the weak-field limit, consistent with the Recognition Science treatment of phi-ladder field processing and the absence of cross terms at leading order.
scope and limits
- Does not establish differentiability of the input fields.
- Does not address strong-field or nonlinear regimes.
- Does not incorporate higher-order cross terms or curvature corrections.
- Does not treat quantum or discrete-lattice corrections to the continuum limit.
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/