def definition def or abbrev

`stringTension`

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

formal statement (Lean)

  59noncomputable def stringTension : ℝ := 0.18  -- GeV²

proof body

Definition body.

  60
  61/-- **THEOREM**: The potential is confining (grows with r).
  62    Proof: V(r₂) - V(r₁) = (r₂ - r₁)(α/(r₁r₂) + σ) > 0 since r₂ > r₁, α ≥ 0, σ > 0. -/

used by (11)

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

alpha_over_sigma_gt_one in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
alpha_over_sigma_pos in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
cornell_at_r0_formula in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
cornellPotential in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
r_min in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
stringTension in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
stringTension_bounds in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
stringTension_pos in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
breakingLength in IndisputableMonolith.QFT.Confinement decl_use
jcostColorPotential in IndisputableMonolith.QFT.Confinement decl_use
QCDString in IndisputableMonolith.QFT.Confinement decl_use

depends on (8)

Lean names referenced from this declaration's body.

V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
stringTension in IndisputableMonolith.Nuclear.QCDToNuclearBridge decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use