def definition def or abbrev

`twoLevelSystem`

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

formal statement (Lean)

 253def twoLevelSystem (gap : ℝ) : System := {

proof body

Definition body.

 254  levels := [
 255    ⟨0, 1, by norm_num⟩,      -- Ground state
 256    ⟨gap, 1, by norm_num⟩     -- Excited state
 257  ],
 258  nonempty := by norm_num
 259}
 260
 261/-- Ground state probability for a two-level system. -/

depends on (10)

Lean names referenced from this declaration's body.

probability in IndisputableMonolith.Foundation.QuantumLedger decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
probability in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
probability in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
System in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use