modified_falling_condition
plain-language theorem explainer
The theorem proves that an external phase field shifts the unique coherence-restoring acceleration from the pure gravitational case to a = -(gradient of gravitational potential plus gradient of external potential). Researchers deriving acoustic levitation or coherence-modified gravity equilibria would cite this result when assembling forcing chains. The proof constructs the candidate acceleration explicitly then verifies uniqueness by algebraic reduction to a linear equation whose only solution follows from positive object extent.
Claim. Let field be a processing field with potential gradient deriv field.phi, ext an external phase field with gradient deriv ext.psi, and obj an extended object with center-of-mass height obj.h_cm and positive extent. Then there exists a unique real number a such that the modified coherence defect vanishes: 2 * obj.extent * |deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a| = 0.
background
In the Recognition Science gravity module, coherence defect quantifies mismatch between object motion and local processing potential, with zero defect marking equilibrium. ProcessingField supplies the gravitational potential phi while ExternalPhaseField adds an independent potential psi arising from acoustic or phase-locked mechanisms. ExtendedObject records center-of-mass position and positive extent. This theorem extends the base falling_restores_coherence result by allowing external fields to shift the equilibrium point.
proof idea
The proof is tactic-mode. It first supplies the explicit candidate a = -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm). It then rewrites via the sibling lemma modified_coherence_defect_simplify, cancels the resulting expression by ring, and obtains zero defect. For uniqueness it rewrites the defect equation, applies mul_eq_zero to the factored form 2 * extent * (sum + a) = 0, discards the extent factor by positivity, and concludes a is the unique solution by linarith.
why it matters
This declaration supplies the second step of the forcing chain to levitation inside AcousticPhaseLevitation. It is invoked directly by levitation_is_inevitable, forcing_chain_complete, and LevitationInevitability to show external fields modify the coherence landscape. The result closes the gap between pure gravitational coherence restoration and full acoustic levitation certificates, aligning with the eight-tick resonance and coherence-gain components of the unconditional levitation argument. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.