falling_restores_coherence
plain-language theorem explainer
The theorem establishes that for any processing field with potential function and extended object there exists a unique real acceleration that nullifies the coherence defect. Physicists modeling gravity as coherence restoration in Recognition Science would cite this result. The proof exhibits the candidate acceleration explicitly as the negative derivative of the potential at the center of mass and verifies uniqueness by reducing the defect equation to a product that vanishes only when the acceleration matches that value.
Claim. Let $Φ$ be the potential function of a processing field and let an extended object have center-of-mass position $h_{cm}$ together with positive extent $e>0$. Then there exists a unique real number $a$ such that the coherence defect, defined as the absolute difference between the total potentials (gravitational plus linear acceleration term) evaluated at the head and feet of the object, equals zero. This unique $a$ equals $-Φ'(h_{cm})$.
background
ProcessingField is the structure containing a potential function $Φ$ from position to real numbers. ExtendedObject packages a center-of-mass position, a positive extent $e>0$, and the linear approximation for total potential in an accelerating frame: $Φ(h_{cm}+z)+a·z$. Coherence defect is the absolute difference of this total potential between the head ($z=+e$) and feet ($z=-e$) positions; it vanishes precisely when the frame accelerates to cancel the gradient of $Φ$ across the object. The module Gravity.CoherenceFall interprets gravity as the acceleration required to maintain local coherence. The proof draws on the defect functional from LawOfExistence and the zero-divisor property mul_eq_zero from IntegersFromLogic.
proof idea
The proof posits the candidate $a=-(deriv field.phi obj.h_cm)$. Existence is immediate by simplification of the coherence_defect definition, which cancels the linear terms. Uniqueness proceeds by assuming another value $a'$ also yields zero defect, reducing via coherence_defect_simplify and abs_eq_zero to the equation $2·e·(Φ'+a')=0$. Positivity of the extent forces $Φ'+a'=0$, hence $a'=a$, using mul_eq_zero to split the product and linarith to solve the resulting linear equation.
why it matters
This theorem supplies the gravity_is_coherence step in LevitationInevitability and is referenced directly in forcing_chain_complete, full_levitation_cert, levitation_is_inevitable, and levitation_unconditional inside AcousticPhaseLevitation. It realizes the Recognition Science claim that gravity is the requirement to accelerate in order to maintain a locally constant processing environment, thereby linking the phi-ladder and eight-tick octave structures to observable free-fall behavior. The result closes one link in the chain from primitives to acoustic levitation without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.