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

CouplingLawCert

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)

 253structure CouplingLawCert where
 254  enhancement_universal :
 255    ∀ (t : ℝ), t ≠ 0 →
 256      exactCost t = coshEnhancement t * perturbativeCost t
 257  perturbative_limit :
 258    coshEnhancement 0 = 1
 259  enhancement_symmetric :
 260    ∀ (t : ℝ), coshEnhancement (-t) = coshEnhancement t
 261  geometric_dominance :
 262    ∀ (t : ℝ), t ≠ 0 → 1 < coshEnhancement t
 263
 264/-- The coupling law certificate is inhabited. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.