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

ExternalPhaseField

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)

  63structure ExternalPhaseField where
  64  psi : Position → ℝ
  65
  66/-- The gradient of the external field at a given position. -/
  67def ExternalPhaseField.gradient (ext : ExternalPhaseField) (h : Position) : ℝ :=

proof body

Definition body.

  68  deriv ext.psi h
  69
  70/-! ## 2. Modified Coherence Defect -/
  71
  72/-- Total potential when BOTH gravitational and external phase fields are present,
  73    in a frame accelerating with `a`.
  74    Φ_total(z) = Φ_grav(h_cm + z) + Φ_ext(h_cm + z) + a·z
  75    (linearized around center of mass) -/

used by (21)

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

depends on (19)

Lean names referenced from this declaration's body.