log_phi_lt_one
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.