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

baseline_gravitational_coupling

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 184def baseline_gravitational_coupling
 185    (field : ProcessingField) (obj : ExtendedObject) : ℝ :=

proof body

Definition body.

 186  |deriv field.phi obj.h_cm|
 187
 188/-- ANTI-COHERENCE COUPLING REDUCTION: When the external field gradient opposes the
 189    gravitational gradient (anti-coherence), the effective coupling is reduced.
 190
 191    Specifically: if ∇Φ_ext has the opposite sign to ∇Φ_grav and
 192    |∇Φ_ext| ≤ |∇Φ_grav|, then |a_eq| ≤ |∇Φ_grav|. -/

used by (3)

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

depends on (9)

Lean names referenced from this declaration's body.