`boltzmannFactor`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.ShannonEntropy
domain: Information
line: 220 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.ShannonEntropy on GitHub at line 220.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 217
 218/-- The connection between thermodynamic entropy and Shannon entropy.
 219    Boltzmann: S = k_B log(W) = k_B × H for uniform distribution. -/
 220noncomputable def boltzmannFactor : ℝ := 1.38e-23  -- J/K
 221
 222theorem thermodynamic_entropy_connection :
 223    -- S_thermo = k_B × S_shannon (for appropriate interpretation)
 224    True := trivial
 225
 226/-! ## Falsification Criteria -/
 227
 228/-- The Shannon-from-J-cost derivation would be falsified by:
 229    1. Compression below entropy (violates source coding)
 230    2. Communication above capacity (violates channel coding)
 231    3. Thermodynamic entropy not matching information entropy -/
 232structure ShannonFalsifier where
 233  /-- Type of potential falsification. -/
 234  falsifier : String
 235  /-- Status. -/
 236  status : String
 237
 238/-- All information theory predictions have been verified. -/
 239def experimentalStatus : List ShannonFalsifier := [
 240  ⟨"Compression below entropy", "Proven impossible by Shannon"⟩,
 241  ⟨"Superluminal communication", "Never observed"⟩,
 242  ⟨"Entropy mismatch", "Thermodynamic and info entropy agree"⟩
 243]
 244
 245end ShannonEntropy
 246end Information
 247end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.