module module

`IndisputableMonolith.QFT.Confinement`

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

used by (1)

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

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (22)

def cornellPotential L52
def alphaSshort L56
def stringTension L59
theorem potential_confining L63
def jcostColorPotential L89
theorem asymptotic_freedom L97
def cornellPotentialVal L103
theorem confinement_at_long_distance L108
structure QCDString L124
theorem string_breaking L136
def lightQuarkMass L141
def breakingLength L146
theorem confinement_from_ledger L158
theorem gluon_confinement L166
structure HadronMass L175
def protonMassBreakdown L188
theorem mass_without_mass L198
def confinementPredictions L210
def deconfinementTemperature L219
theorem deconfinement_at_high_T L221
structure ConfinementFalsifier L233
def experimentalStatus L240