pith. machine review for the scientific record. sign in
def definition def or abbrev high

modified_coherence_defect

show as:
view Lean formalization →

Modified coherence defect measures the absolute difference in total potential across the extent of an extended object when gravitational and external phase fields are superposed in an accelerating frame. Researchers working on acoustic or phase-based levitation from first principles would cite this quantity when establishing zero-defect equilibria. The definition is a direct arithmetic wrapper that evaluates the modified total potential at symmetric head and feet positions and returns their absolute difference.

claimFor a processing field with potential function $Φ$, an external phase field with potential $ψ$, an extended object with center-of-mass height $h_{cm}$ and positive extent $e$, and frame acceleration $a$, the modified coherence defect is defined by $D = |Φ_{total}(h_{cm}+e) - Φ_{total}(h_{cm}-e)|$, where the total potential is the sum $Φ_{total}(z) = Φ(h_{cm}+z) + ψ(h_{cm}+z) + a z$.

background

Recognition Science treats gravity as a coherence-restoring process acting on spatially extended objects. A ProcessingField supplies the underlying gravitational potential $Φ(h)$. An ExternalPhaseField supplies an additional differentiable phase potential $ψ(h)$ that can be realized by acoustic standing waves, rotating superconductors, or phase-locked electromagnetic sources. An ExtendedObject is specified by its center-of-mass position $h_{cm}$ and a positive half-extent $e$ that defines the head and feet locations.

proof idea

This is a one-line wrapper that applies modified_total_potential at the head and feet of the object and returns the absolute value of their difference.

why it matters in Recognition Science

The definition supplies the central scalar for every levitation theorem in the module. It is invoked directly by acoustic_levitation to prove that exact gradient cancellation yields zero defect at zero acceleration, by equilibrium_is_coherent to confirm coherence at the equilibrium acceleration, and by FullLevitationCert to close the integration of EnergyProcessingBridge, WeakFieldSuperposition, CoherenceGain, and EightTickResonance. The surrounding ForcingChainToLevitation structure traces the construction back to the Recognition Composition Law and the T5–T8 forcing chain.

scope and limits

formal statement (Lean)

  85def modified_coherence_defect
  86    (field : ProcessingField) (ext : ExternalPhaseField)
  87    (obj : ExtendedObject) (a : ℝ) : ℝ :=

proof body

Definition body.

  88  let pot_head := modified_total_potential field ext obj a obj.extent
  89  let pot_feet := modified_total_potential field ext obj a (-obj.extent)
  90  abs (pot_head - pot_feet)
  91
  92/-- Helper: expand modified_coherence_defect into explicit arithmetic. -/

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.