antiGravField_cancels
plain-language theorem explainer
The anti-gravitational phase field negates the gravitational potential of a processing field, and its derivative at an extended object's center of mass exactly cancels the original gradient whenever the potential is differentiable there. Acoustic levitation modelers in Recognition Science cite this result to justify zero net force in coherence calculations. The proof is a direct term application of the derivative negation rule.
Claim. Assume the potential function of a processing field is differentiable at the center-of-mass position $h_{cm}$ of an extended object. The anti-gravitational field defined by pointwise negation of this potential then satisfies $d( -Phi )/dh (h_{cm}) = - d Phi / dh (h_{cm})$.
background
Processing fields are structures carrying a potential function Phi from position to real numbers that enters coherence defect calculations via the defect functional J. Extended objects are structures specified by a center-of-mass coordinate h_cm together with positive spatial extent. The anti-gravitational field is the external phase field obtained by negating this potential pointwise, as introduced in the sibling definition antiGravField.
proof idea
The proof is a term-mode reduction that rewrites the derivative of the negated potential and invokes the lemma deriv_neg to obtain the sign flip. It proceeds by exhibiting the equality directly and discharging it with exact on the negated-derivative identity.
why it matters
This theorem supplies the derivative cancellation used by the downstream results concrete_levitation and levitation_field_exists to establish zero modified coherence defect at zero acceleration. It completes the local step in the acoustic levitation construction, consistent with eight-tick phase periodicity in the Recognition Science forcing chain. The claim is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.