System — Recognition explainer

formal statement (Lean)

  63structure System where
  64  /-- The energy levels. -/
  65  levels : List EnergyLevel
  66  /-- Non-empty. -/
  67  nonempty : levels.length > 0
  68
  69/-! ## The Partition Function -/
  70
  71/-- The Boltzmann factor for an energy level at inverse temperature β. -/

used by (36)

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

GeometricStrain in IndisputableMonolith.Applied.CoherenceTechnology decl_use
resonant_minimization in IndisputableMonolith.Applied.CoherenceTechnology decl_use
postural_minimization in IndisputableMonolith.Applied.PosturalAlignment decl_use
SystemStability in IndisputableMonolith.Applied.PosturalAlignment decl_use
tidalLockingFromPhiResonanceCert in IndisputableMonolith.Astrophysics.TidalLockingFromPhiResonance decl_use
ell0_ne_zero in IndisputableMonolith.Constants.Derivation decl_use
cosh_sum_via_dAlembert in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction decl_use
pairSystemCost in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction decl_use
scale_free_causal_closure in IndisputableMonolith.Papers.DIF.CausalClosure decl_use
solar_ratio_bound in IndisputableMonolith.Papers.DIF.CausalClosure decl_use
loadDatasetFromJson in IndisputableMonolith.PDG.Fits decl_use
einselection_from_jcost in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
macro_decohere_instant in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
QuantumClassicalCrossover in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
holographicPredictions in IndisputableMonolith.Quantum.HolographicBound decl_use
beta_def in IndisputableMonolith.Relativity.ILG.PPN decl_use
gamma_bound in IndisputableMonolith.Relativity.ILG.PPN decl_use
averageEnergy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy_nonneg_of_Z_ge_one in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
finset_sum_eq_list_sum in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
freeEnergy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
free_energy_identity in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
partitionFunction in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
partition_ge_ground in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
partition_positive in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
probability in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
prob_nonneg in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
prob_normalized in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
recognitionCost in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use

… and 6 more

depends on (4)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
empty in IndisputableMonolith.RRF.Foundation.Ledger decl_use
EnergyLevel in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
temperature in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use