partial_weight_reduction
plain-language theorem explainer
Partial anti-coherence from an external phase field reduces the effective gravitational weight of an extended object by a factor at most 1. Researchers modeling acoustic levitation or coherence-modified gravity would cite the result to bound weight reduction in [0,1]. The term-mode proof unfolds the weight reduction factor, rewrites the division inequality from the positive gravitational gradient, and invokes the anti-coherence coupling lemma.
Claim. Let $g = (d phi / dh)(h_{cm}) > 0$ be the gravitational processing gradient at the center of mass and $e = (d psi / dh)(h_{cm}) leq 0$ the external phase gradient satisfying $-e leq g$. Then the weight reduction factor constructed from baseline gravitational coupling is at most 1.
background
The AcousticPhaseLevitation module extends coherence-seeking gravity by adding external phase fields that modify local processing potential. ExternalPhaseField is a structure supplying an additional psi field whose gradient contributes anti-coherence. ProcessingField supplies the gravitational phi field. Weight reduction factor is defined via baseline gravitational coupling, which normalizes the combined gradient effect. Upstream constants supply G in RS-native units and the tick as fundamental time quantum; the Chain structure provides the minimal recognition axioms used in the broader module.
proof idea
The proof is a one-line wrapper. It unfolds weight_reduction_factor, rewrites the division inequality using the positivity of g to obtain a valid denominator, and applies the sibling lemma anti_coherence_reduces_coupling to conclude the inequality.
why it matters
The theorem establishes the partial case of anti-coherence reducing gravitational coupling, the step immediately preceding full levitation in the module's forcing-chain summary. It sits inside the RS chain from RCL through J-uniqueness, phi self-similarity, eight-tick octave, and D=3 to coherence-seeking gravity. The result closes the partial-reduction link required for the acoustic-levitation claim that external phase fields can cancel weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.