theorem proved term proof

`vfeCert_holds`

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

formal statement (Lean)

 216theorem vfeCert_holds : VFECert :=

proof body

Term-mode proof.

 217{ vfe_at_boltz := @vfe_at_boltzmann_eq_helmholtzF
 218  boltz_minimizes := @boltzmann_minimizes_vfe }
 219
 220end
 221
 222end IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL

depends on (4)

Lean names referenced from this declaration's body.

Statistics in IndisputableMonolith.QFT.SpinStatistics decl_use
boltzmann_minimizes_vfe in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use
vfe_at_boltzmann_eq_helmholtzF in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use
VFECert in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use