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

k_R

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  48noncomputable def k_R : ℝ := Real.log Constants.phi

proof body

Definition body.

  49
  50/-- **THEOREM C-006.1**: k_R is positive.
  51
  52    Proof: φ > 1, so ln(φ) > 0. -/

used by (35)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 5 more

depends on (6)

Lean names referenced from this declaration's body.