theorem proved term proof

`ilg_coercivity`

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

formal statement (Lean)

 188theorem ilg_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
 189    (ilgModel P h_energy).defectMass s ≤
 190    ((ilgModel P h_energy).C.Knet * (ilgModel P h_energy).C.Cproj * (ilgModel P h_energy).C.Ceng) *
 191    (ilgModel P h_energy).energyGap s :=

proof body

Term-mode proof.

 192  (ilgModel P h_energy).defect_le_constants_mul_energyGap s
 193
 194/-- Reverse coercivity: energy gap is at least c_min times defect. -/

depends on (16)

Lean names referenced from this declaration's body.

defect_le_constants_mul_energyGap in IndisputableMonolith.CPM.LawOfExistence decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
defectMass in IndisputableMonolith.ILG.CPMInstance decl_use
EnergyControlHypothesis in IndisputableMonolith.ILG.CPMInstance decl_use
energyGap in IndisputableMonolith.ILG.CPMInstance decl_use
ilgModel in IndisputableMonolith.ILG.CPMInstance decl_use
ILGState in IndisputableMonolith.ILG.CPMInstance decl_use
KernelParams in IndisputableMonolith.ILG.Kernel decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use