k_R_pos
plain-language theorem explainer
The declaration proves that the Recognition Science Boltzmann constant k_R, defined as the natural logarithm of the golden ratio, is strictly positive. Researchers deriving thermodynamic relations or black hole entropies in Recognition Science would invoke this to guarantee positive energy scales. The proof reduces directly to the positivity of the logarithm applied to the established inequality that phi exceeds one.
Claim. $k_R > 0$, where $k_R :=$ natural logarithm of the golden ratio $phi = (1 + sqrt(5))/2$.
background
The module derives the Boltzmann analog k_R from the ledger bit cost in Recognition Science. It sets k_R = ln(phi), where phi is the self-similar fixed point forced by the forcing chain at step T6. This replaces the conventional k_B in native units, with the physical interpretation that each ledger bit carries cost ln(phi) approximately 0.481. The module doc states that temperature relates to energy via this constant derived from self-similarity, and SI conversion uses coherence scales.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of k_R to Real.log phi, then applies the Real.log_pos lemma, discharging the goal with the upstream fact one_lt_phi that phi exceeds one.
why it matters
This result anchors the positivity of thermodynamic quantities throughout the framework. It directly supports the nonzero theorem k_R_ne_zero and feeds into entropy positivity for ultramassive black holes, saturation acceleration bounds, and bandwidth capacity equalities in unification modules. It fills the C-006.1 slot in the constants derivation, linking to the phi-ladder and eight-tick octave structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.