def definition def or abbrev

`phiPsiCouplingStub`

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

formal statement (Lean)

 115noncomputable def phiPsiCouplingStub : PhiPsiCouplingFacts where
 116  phi_minus_psi_difference := by

proof body

Definition body.

 117    intro ng α C_lag x
 118    refine ⟨0, ?_, ?_⟩
 119    · simp
 120    · norm_num
 121
 122instance : PhiPsiCouplingFacts := phiPsiCouplingStub
 123

depends on (1)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use