modified_falling_condition
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not assume any specific functional form for the external potential beyond differentiability at the object center.
- Does not address dynamical stability of the resulting equilibrium under small perturbations.
- Does not derive the external field from Recognition Science primitives; it is supplied as an independent structure.
- Does not apply when object extent is zero or negative.
Lean usage
theorem use_modified (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) : ∃! a, modified_coherence_defect field ext obj a = 0 := modified_falling_condition field ext objformal statement (Lean)
123theorem modified_falling_condition
124 (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) :
125 ∃! a : ℝ, modified_coherence_defect field ext obj a = 0 := by
proof body
Tactic-mode proof.
126 use -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm)
127 refine ⟨?_, ?_⟩
128 · show modified_coherence_defect field ext obj
129 (-(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm)) = 0
130 rw [modified_coherence_defect_simplify]
131 have : deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm +
132 -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm) = 0 := by ring
133 rw [this, mul_zero, abs_zero]
134 · intro a' h_zero
135 rw [modified_coherence_defect_simplify] at h_zero
136 have h0 : 2 * obj.extent * (deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a') = 0 := by
137 rwa [abs_eq_zero] at h_zero
138 have h_extent_pos : (0 : ℝ) < 2 * obj.extent :=
139 mul_pos (by norm_num : (0 : ℝ) < 2) obj.extent_pos
140 have h_extent_ne : 2 * obj.extent ≠ 0 := ne_of_gt h_extent_pos
141 have h2 : deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a' = 0 := by
142 cases mul_eq_zero.mp h0 with
143 | inl h => exact absurd h h_extent_ne
144 | inr h => exact h
145 linarith
146
147/-- LEVITATION THEOREM: If the external phase field gradient exactly cancels
148 the gravitational gradient at the object's position, then the coherence-restoring
149 acceleration is ZERO. The object maintains coherence while stationary.
150
151 This IS acoustic/phase levitation derived from RS first principles. -/