logLowerSimple
plain-language theorem explainer
logLowerSimple defines the rational expression 1 - 1/x as an elementary lower bound for the natural logarithm on positive rationals. Numerics code constructing interval enclosures for log(phi) or related constants in Recognition Science would cite this definition. The implementation is a direct one-line assignment with no lemmas or tactics required.
Claim. For rational $x > 0$, the expression $1 - 1/x$ satisfies the lower bound inequality $ln x >= 1 - 1/x$.
background
The module supplies rigorous interval bounds for the natural logarithm on positive intervals by combining monotonicity of log with Taylor error estimates for log(1+x) when |x|<1. The strategy begins from the fact that log is increasing on (0, ∞), so log([lo, hi]) lies inside [log(lo), log(hi)], then tightens the bounds via series remainders bounded by |x|^{n+1}/((n+1)(1-|x|)). This definition supplies the elementary rational lower bound log(x) >= 1 - 1/x for x > 0, which is applied when x = phi - 1 lies in (0,1). The listed upstream structure records meta-realization axioms but is not invoked by this numeric definition.
proof idea
Direct definition: the body is the single expression 1 - 1/x. No lemmas from Mathlib or sibling files are applied; the declaration is a pure abbreviation.
why it matters
The bound participates in the interval-arithmetic layer that produces concrete enclosures for log(phi) and thereby supports the phi-ladder mass formula and alpha-band numerics (alpha^{-1} inside (137.030, 137.039)). It fills a low-level numeric slot beneath the eight-tick octave and D=3 derivations, even though no downstream theorems are yet recorded. The module doc-comment explicitly ties the construction to the Recognition Science strategy of obtaining rigorous bounds without external constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.