T_phi
plain-language theorem explainer
T_phi defines the natural temperature scale in Recognition Science as the natural logarithm of the golden ratio φ. It supplies the reference unit for finite-temperature extensions of J-cost minimization, including Gibbs measures and coherence thresholds. Researchers constructing recognition systems at the critical φ-temperature cite this scale when parameterizing TR. The definition is a direct noncomputable assignment drawn from the PhiForcing module.
Claim. $T_φ := ln(φ)$ where $φ$ is the golden ratio that sets the base of the recognition ladder and equals the self-similar fixed point of the forcing chain.
background
The RecognitionThermodynamics module extends zero-temperature J-cost minimization to finite Recognition Temperature TR. Recognition Temperature parameterizes the strictness of minimization, the Gibbs measure is the distribution p(x) ∝ exp(−J(x)/TR), and Recognition Entropy quantifies degeneracy of near-minima. The underlying J-cost is J(x) = ½(x + 1/x) − 1. The module doc states that the φ-ladder supplies natural discretization and the 8-tick cycle supplies the fundamental time unit τ₀. T_phi supplies the reference scale T_φ = ln(φ) for these constructions.
proof idea
This is a one-line definition that directly assigns the natural logarithm of φ from the PhiForcing foundation. No lemmas or tactics appear inside the definition body itself. The companion theorem T_phi_pos separately proves positivity by unfolding the definition and applying log_pos to phi_gt_one.
why it matters
T_phi anchors the thermodynamic layer of the framework and is used by phi_temperature_system (a recognition system at the φ-temperature) and rs_coherence (the threshold C = T_φ / TR that separates coherent and decoherent regimes). It realizes the φ-ladder scale required by the forcing chain (T5 J-uniqueness, T6 phi fixed point) and supplies the unit in which the Gibbs weight exp(−J/TR) is expressed. The definition closes the gap between the T=0 cost structure and finite-temperature statistics without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.