boltzmann_analog_positive
plain-language theorem explainer
The declaration proves that the natural logarithm of the golden ratio is strictly positive. Researchers deriving thermodynamic relations in Recognition Science cite it to establish that the Boltzmann analog k_R is positive. The proof reduces immediately to the standard positivity of the logarithm once phi exceeds one is available.
Claim. $0 < k_R$ where $k_R = ln(phi)$ and $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module supplies calculated proofs for registry items C-001 through C-006. The Boltzmann analog k_R is defined as the natural logarithm of phi and represents the information cost per ledger bit in RS-native thermodynamics. This replaces the conventional Boltzmann constant. The result relies on the upstream lemma one_lt_phi, which establishes that the golden ratio exceeds one.
proof idea
The proof is a one-line wrapper that applies Real.log_pos to the fact one_lt_phi. The tactic discharges the hypothesis that the argument exceeds one, yielding the strict positivity of the logarithm.
why it matters
This theorem supplies the lower bound for the Boltzmann analog in the constants registry. It is used by boltzmann_analog_bounds to establish the full interval 0 < k_R < 0.5 and by constants_predictions_cert_exists to certify the collection of constant predictions. Within the framework it anchors the positivity of the recognition cost per bit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.