SuperpositionJustification
plain-language theorem explainer
The SuperpositionJustification structure bundles three properties that establish weak-field superposition directly from Recognition Science cost and defect axioms. Gravity modelers cite it when closing integration gaps in levitation certificates or when adding independent processing fields. Each property is supplied by an upstream lemma with no extra hypotheses required.
Claim. A structure asserting: (i) for all real numbers ε with -1 < ε, the J-cost satisfies Jcost(1 + ε) = ε² / (2(1 + ε)); (ii) for any pair of gravitational and external processing fields and any position h0 at which both fields are differentiable, the derivative of their pointwise sum equals the sum of the individual derivatives; (iii) for any such pair, any extended object, and any real a, the coherence defect of the combined field equals |2 × object extent × (sum of the two field derivatives + a)|.
background
Recognition Science defines the defect functional as J(x) for positive x, with the associated cost measuring recognition cost of deviations from unity. A WeakFieldPair consists of two independent processing fields whose combined phi is their pointwise sum. The Gravity.WeakFieldSuperposition module works in the regime where these fields remain differentiable and their gradients add linearly, so that coherence defects of the combined field also add. Upstream lemmas supply the exact quadratic expansion of Jcost near 1 and the additivity of gradients and defects.
proof idea
This is a definition that packages three properties. The quadratic_regime field is supplied by the lemma Jcost_one_plus_exact. The gradient_additivity field is supplied by gradient_superposition. The coherence_defect_additivity field is supplied by coherence_defect_of_combined. The structure serves as the target type for the theorem that constructs an explicit instance.
why it matters
The structure supplies the interface for the weak-field superposition principle invoked inside UnconditionalLevitationCert to close Gap 2 of the RS-to-levitation integration. It rests on the forcing chain steps that fix the J-function and the eight-tick octave. The parent theorem superposition_justified builds an instance of the structure from the three named lemmas, completing the bridge from primitive cost additivity to macroscopic field superposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.