log_phi_lt_one
The auxiliary inequality log φ < 1 holds for the RS golden-ratio constant φ. Black-hole entropy modelers and ecologists working on species-area scaling cite it to separate the RS leading-log coefficient c_RS = -log φ / 2 from the LQG value -1/2 and the string-theory value -3/2. The proof chains the numerical bound φ < 1.62 with the elementary fact 1.62 < e, then applies monotonicity of the logarithm.
claim$log φ < 1$, where φ is the golden-ratio fixed point of the Recognition Composition Law.
background
The module recovers the Bekenstein-Hawking entropy S_BH = A / (4 ℓ_P²) from the discrete RS ledger as the count of admissible horizon states modulo σ-equivalence. RS predicts a φ-rational coefficient for the leading log correction c · log A, already distinguishable from LQG (-1/2) and string-theory (-3/2) predictions. The constant φ is the self-similar fixed point forced in the UnifiedForcingChain (T6). The upstream lemma phi_lt_onePointSixTwo supplies the tighter numerical bound φ < 1.62 (since √5 < 2.24).
proof idea
The tactic proof first obtains φ < 1.62 from Constants.phi_lt_onePointSixTwo. It then proves 1.62 < exp(1) by invoking Real.exp_one_gt_d9 and linarith. Chaining via lt_trans yields φ < exp(1). Real.log_lt_log (with φ_pos) produces log φ < log(exp(1)). The final rewrite Real.log_exp simplifies the right-hand side to 1.
why it matters in Recognition Science
This result supplies the strict inequality required by the distinguishability theorems c_RS_neq_LQG and c_RS_neq_string in the same module. Those theorems establish that the RS coefficient -log φ / 2 differs from both the LQG canonical -1/2 and the string-theory canonical -3/2. The module doc-comment identifies the combined formula S_RS(A) = A/4 + c_RS · log A and lists the falsifier as an independent measurement of the leading-log coefficient lying outside (c_RS - 0.05, c_RS + 0.05). The inequality also appears in the BiodiversityScalingCert structure used for species-area exponent bounds.
scope and limits
- Does not compute a numerical value for log φ.
- Does not prove positivity of log φ or other inequalities.
- Does not derive the entropy formula itself; only supports coefficient comparison.
- Does not address the empirical status of the coefficient match with observation.
Lean usage
theorem c_RS_neq_LQG : c_RS ≠ -1 / 2 := by intro h; unfold c_RS at h; have h_log_lt := log_phi_lt_one; linarithformal statement (Lean)
73private theorem log_phi_lt_one : Real.log Constants.phi < 1 := by
proof body
Tactic-mode proof.
74 have h_phi_lt : Constants.phi < 1.62 := Constants.phi_lt_onePointSixTwo
75 have h_e_gt : (1.62 : ℝ) < Real.exp 1 := by
76 have h_e := Real.exp_one_gt_d9
77 linarith
78 have h_phi_lt_e : Constants.phi < Real.exp 1 := lt_trans h_phi_lt h_e_gt
79 have h_log_lt : Real.log Constants.phi < Real.log (Real.exp 1) :=
80 Real.log_lt_log Constants.phi_pos h_phi_lt_e
81 rw [Real.log_exp] at h_log_lt
82 exact h_log_lt
83
84/-- The RS leading-log coefficient is strictly distinct from the LQG
85 canonical `-1/2`. -/