k_R_ne_zero
plain-language theorem explainer
The theorem establishes that the RS Boltzmann constant k_R, defined as the natural logarithm of the golden ratio, is nonzero. Thermodynamic calculations in Recognition Science that divide by k_R would cite this result to ensure well-defined expressions. The proof is a one-line term application of the fact that a positive real number cannot be zero.
Claim. Let $k_R = ln φ$ where $φ = (1 + √5)/2$ is the golden ratio. Then $k_R ≠ 0$.
background
In the module on Boltzmann constant derivation, k_R is introduced as the RS analog of k_B, set equal to the fundamental ledger bit cost J_bit = ln(φ). The definition unfolds to k_R := Real.log Constants.phi. The immediate upstream result k_R_pos proves k_R > 0 by applying Real.log_pos to the fact that φ > 1. This sits inside the C-006 series that derives temperature-energy relations from the self-similar ledger structure rather than treating k_B as a free parameter.
proof idea
The proof is a term-mode one-liner that applies ne_of_gt directly to the positivity theorem k_R_pos.
why it matters
This result guarantees that division by k_R remains valid in thermodynamic expressions such as thermal energy at unit temperature. It completes the C-006.2 step immediately after the positivity theorem C-006.1 and supports downstream ledger-based derivations of mass-to-light ratios and nucleosynthesis tiers. Within the Recognition framework it anchors the exchange rate between thermal energy and ledger cost at the phi scale forced by T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.