any_source_suffices
plain-language theorem explainer
Any phase field source that produces an external gradient exactly opposing the gravitational gradient at an object's center of mass drives the modified coherence defect to zero. Experimental groups studying acoustic standing waves or rotating superconductors would cite the result when deriving weight reduction from RS coherence dynamics. The proof is a direct one-line application of the acoustic_levitation theorem.
Claim. Let $ext$ be an external phase field with potential $psi$ and let $field$ be the gravitational processing field with potential $phi$. If the gradients satisfy $deriv(psi, h_{cm}) = -deriv(phi, h_{cm})$ at the center of mass of an extended object, then the modified coherence defect vanishes: $modified_coherence_defect(field, ext, obj, 0) = 0$.
background
The module treats acoustic phase levitation by adjoining an ExternalPhaseField structure whose psi : Position → ℝ supplies an arbitrary gradient that can cancel the gravitational processing potential. PhaseFieldSource is an inductive type enumerating three mechanisms (acoustic standing wave, rotating superconductor, rotating magnetic array) that generate such fields through rotation plus phase coherence. The central upstream result is the acoustic_levitation theorem, which states that exact gradient cancellation implies zero coherence-restoring acceleration and therefore zero modified coherence defect.
proof idea
The proof is a one-line wrapper that applies the acoustic_levitation theorem to the supplied field, external field, object, and cancellation hypothesis.
why it matters
The declaration shows that levitation depends only on the existence of a canceling gradient, not on the concrete source mechanism. It therefore generalizes the acoustic_levitation theorem to all PhaseFieldSource cases and supports the claim that coherence defect controls effective gravitational coupling. The result sits inside the Gravity domain and precedes the weight-reduction factor definitions; it draws on the coherence and eight-tick resonance structures from the foundation without introducing new open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.