SuperpositionJustification
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not address strong-field regimes where nonlinear terms appear.
- Does not derive the explicit functional form of individual processing fields.
- Does not compute numerical levitation thresholds or stability criteria.
- Does not incorporate quantum or higher-order corrections beyond the classical weak-field limit.
Lean usage
theorem superposition_justified : SuperpositionJustification where quadratic_regime := Jcost_one_plus_exact gradient_additivity := gradient_superposition coherence_defect_additivity := coherence_defect_of_combinedformal 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. -/