k_R
plain-language theorem explainer
k_R is defined as the natural logarithm of the golden ratio phi. Workers deriving RS thermodynamics or ledger-based statistical mechanics cite this as the base cost per recognition bit. The declaration is a direct one-line assignment with no lemmas or reduction steps.
Claim. $k_R := {ln} φ$ where $φ = (1 + √5)/2$ denotes the golden ratio fixed by the self-similar ledger.
background
Recognition Science treats the Boltzmann constant as an emergent ledger quantity rather than a free parameter. The module sets k_R equal to the per-bit cost J_bit, which equals ln(φ) once φ is fixed by the forcing chain at T6. Temperature then scales as average cost per degree of freedom, so thermal energy takes the form E = k_R · T in RS-native units. The upstream Constants structure supplies phi together with the inequalities one_lt_phi, phi_gt_onePointSixOne and phi_lt_onePointSixTwo that later bound k_R.
proof idea
The declaration is a direct definition that unfolds to Real.log Constants.phi. No tactics, no lemmas, and no reduction are required; the body is the assignment itself.
why it matters
This definition supplies the anchor for the C006_certificate and for the family of results k_R_pos, k_R_ne_zero, k_R_lt_half, k_R_bounds and k_R_eq_J_bit. It realizes the T6 step that forces phi as the self-similar fixed point and thereby fixes the information cost of each ledger bit. The same quantity appears in horizonArea calculations inside UltramassiveBH, closing the link between gravitational and thermodynamic scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.