superposition_justified
plain-language theorem explainer
The weak-field superposition principle follows from the exact quadratic identity for J-cost near equilibrium together with linear additivity of field gradients and coherence defects. Researchers completing the forcing chain to acoustic levitation in Recognition Science cite this result to close the weak-field gap. The proof is a direct structure constructor that assembles the three required properties from the J-cost identity, gradient superposition, and coherence defect additivity lemmas.
Claim. In the weak-field regime, for any gravitational and external field pair, the J-cost satisfies $J(1 + ε) = ε² / (2(1 + ε))$ whenever $ε > -1$; the derivative of the combined potential equals the sum of the individual derivatives at every differentiable point; and the coherence defect of the combined field equals $|2 · extent · (deriv_grav + deriv_ext + a)|$.
background
The J-cost function measures recognition cost of a field value, with the exact identity Jcost(1 + ε) = ε² / (2(1 + ε)) for ε > -1 serving as the bridge to kinetic-energy approximations in the Hamiltonian. A WeakFieldPair packages a gravitational potential, an external potential, and their pointwise sum as the combined field, all assumed differentiable. Coherence defect quantifies the absolute deviation of an extended object from perfect coherence under the total gradient plus an acceleration parameter a.
proof idea
The proof is a one-line structure constructor for SuperpositionJustification. It supplies the quadratic_regime field directly from the Jcost_one_plus_exact theorem, the gradient_additivity field from gradient_superposition (via simp on the combined definition), and the coherence_defect_additivity field from coherence_defect_of_combined (via the summed-derivative decomposition).
why it matters
This theorem fills the gap2_superposition slot in the full_levitation_cert and levitation_unconditional certificates of AcousticPhaseLevitation, completing the forcing chain from RS primitives to levitation. It thereby links the quadratic J-cost regime and linear gradient addition to the coherence-based account of gravity, supporting the weak-field limit of the coherence-fall mechanism within the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.