IndisputableMonolith.Foundation.Thermodynamics

declarations in this module (37)

• def rs_entropy L102
• def rs_energy L107
• theorem rs_entropy_nonneg L111
• theorem rs_entropy_zero_iff_unity L115
• theorem rs_energy_unity L120
• def equilibrium_entry L127
• theorem equilibrium_entry_pos L129
• def equilibrium_entropy L134
• theorem equilibrium_entropy_eq L138
• theorem equilibrium_entropy_nonneg L144
• theorem equilibrium_entropy_zero_iff L152
• def rs_temperature L180
• theorem temperature_zero_at_unity L189
• theorem temperature_positive L197
• theorem temperature_negative L207
• theorem temperature_odd L215
• theorem temperature_determines_equilibrium L224
• theorem first_law_derivative L250
• theorem first_law L271
• theorem full_defect_monotone L299
• def observer_entropy L306
• theorem observer_entropy_nonneg L311
• def system_entropy L320
• theorem entropy_decomposition L327
• def boltzmann_weight L338
• theorem boltzmann_weight_pos L341
• theorem boltzmann_at_equilibrium L351
• theorem canonical_from_ignorance L371
• def specific_heat L383
• theorem specific_heat_positive L387
• theorem specific_heat_is_second_deriv L396
• theorem specific_heat_at_zero L409
• theorem third_law L424
• theorem absolute_zero_unreachable L438
• def InThermalEquilibrium L456
• theorem thermal_eq_iff_equal_ratio L460
• theorem thermodynamics_certificate L498