log_phi_bound
plain-language theorem explainer
The lemma pins the natural logarithm of the golden ratio between 0.481211 and 0.481212. Numerics work in Recognition Science cites it to anchor phi-based interval calculations without external libraries. The proof is a one-line wrapper that splits the conjunction via constructor and verifies each side with num_ineq.
Claim. $0.481211 ≤ ln(φ) ≤ 0.481212$, where φ denotes the golden ratio.
background
The IntervalProofs module supplies minimal helpers that convert small numerical inequalities into Lean proofs by combining norm_num with monotonicity. The golden ratio enters Recognition Science as the self-similar fixed point forced at step T6 of the unified forcing chain. No upstream lemmas are invoked; the bound is obtained directly from floating-point evaluation inside the real numbers.
proof idea
The proof is a one-line wrapper. Constructor splits the conjunction into two inequalities; num_ineq then numerically confirms each bound holds.
why it matters
The bound supplies a concrete numerical anchor for phi in the Recognition framework, supporting later calculations of the phi-ladder mass formula and the alpha inverse interval. It belongs to the numerics layer that keeps all constants inside RS-native units (c=1, ħ=φ^{-5}). No downstream theorems are recorded, so the lemma functions as a reusable numerical fact rather than a chain link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.