anti_coherence_reduces_coupling
plain-language theorem explainer
When an external phase field gradient opposes the gravitational gradient and does not exceed it in magnitude, the effective gravitational coupling is bounded above by the baseline value. Researchers modeling acoustic levitation or phase-modified gravity cite this to quantify partial weight reduction. The proof unfolds the two coupling definitions, substitutes the given derivatives, replaces absolute values via sign lemmas, and closes with linear arithmetic.
Claim. Let $g = dPhi/dh(h_{cm}) > 0$ and $e = dpsi/dh(h_{cm}) leq 0$ with $-e leq g$. Then $|g + e| leq |g|$.
background
The AcousticPhaseLevitation module treats gravity via a ProcessingField whose potential Phi determines motion through its gradient at an ExtendedObject's center of mass. An ExternalPhaseField supplies an additional potential psi representing acoustic standing waves or phase-locked mechanisms. Baseline gravitational coupling is the absolute gradient of Phi alone; effective gravitational coupling is the absolute value of the sum of the two gradients. ExtendedObject provides the evaluation point h_cm together with a positive extent. This local setting extends the coherence-fall framework in which processing fields govern equilibrium acceleration.
proof idea
The tactic proof unfolds effective_gravitational_coupling and baseline_gravitational_coupling, then rewrites both derivatives using the supplied equalities hg and he. It applies abs_of_pos to the positive g and derives g + e leq g together with non-negativity of the sum via linarith. abs_of_nonneg replaces the remaining absolute value, after which linarith finishes the inequality.
why it matters
The result is invoked by partial_weight_reduction to establish that the weight reduction factor lies in [0,1]. It supplies the concrete anti-coherence bound required for the acoustic levitation development, showing how an opposing external gradient reduces effective coupling without changing the underlying potential structure. In the Recognition Science chain it illustrates modification of gravitational processing by external phase fields while preserving the phi-ladder mass relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.