pith. machine review for the scientific record. sign in
def definition def or abbrev

C006_certificate

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 188def C006_certificate : String :=

proof body

Definition body.

 189  "═══════════════════════════════════════════════════════════\n" ++
 190  "  C-006: BOLTZMANN CONSTANT k_R — STATUS: DERIVED\n" ++
 191  "═══════════════════════════════════════════════════════════\n" ++
 192  "✓ k_R = ln(φ) — forced by ledger structure (T6)\n" ++
 193  "✓ k_R > 0 — positive temperature scale\n" ++
 194  "✓ k_R < 0.5 — bounded by φ < 1.62\n" ++
 195  "✓ k_R = J_bit — unified with bit cost\n" ++
 196  "✓ Thermal energy E = k_R · T\n" ++
 197  "ORIGIN: Self-similar ledger closure → φ → ln(φ) = k_R\n" ++
 198  "═══════════════════════════════════════════════════════════"
 199
 200end BoltzmannConstant
 201end Constants
 202end IndisputableMonolith

depends on (11)

Lean names referenced from this declaration's body.