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

inflatonPotentialCert

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)

 113def inflatonPotentialCert : InflatonPotentialCert where
 114  vacuum := V_vacuum

proof body

Definition body.

 115  nonneg := V_nonneg
 116  pos_off_vacuum := V_pos_off_vacuum
 117  reciprocal_symm := V_reciprocal_symm
 118  quadratic_form := V_eq_quadratic
 119
 120end
 121end InflatonPotentialFromJCost
 122end Cosmology
 123end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.