pith. sign in
module module high

IndisputableMonolith.Numerics.Interval.Log

show as:
view Lean formalization →

Numerics.Interval.Log supplies verified interval bounds for the natural logarithm, anchored on the inequality log(x) ≥ 1 - 1/x for x > 0. Researchers computing phi-ladder energies or superconducting critical temperatures cite these bounds when composing power and exponential expressions. The module lifts elementary inequalities to monotonic interval statements that integrate directly with rational-endpoint arithmetic.

claimThe module establishes $log x ≥ 1 - 1/x$ for $x > 0$, together with monotonicity of the log interval map and containment results that bound $log([a,b])$ for positive intervals.

background

The module extends Verified Interval Arithmetic, which computes rigorous bounds on transcendental functions using rational endpoints that Lean handles exactly. It also imports algebraic bounds on the golden ratio φ = (1 + √5)/2 obtained from 2.236² < 5 < 2.237². The local setting is the numerics layer that supplies controlled-error bounds for Recognition Science calculations involving log, exp, and powers.

proof idea

The module collects lemmas that apply the standard inequality log(x) ≥ 1 - 1/x, lift it via monotonicity to interval versions, and add phi-specific and Taylor-error results. Each lemma follows from basic analysis facts already available in the imported Basic and PhiBounds modules.

why it matters in Recognition Science

The module is imported by Numerics.Interval.Pow to bound x^y = exp(y log x), by Chemistry.SuperconductingTc for φ-gap ladder energy scales in superconductors, by Numerics.Interval.Tactic for bound tactics, and by Papers.GCIC.Thermodynamics for phase-structure calculations. It supplies the logarithm component required for eight-tick coherence and phi-ladder mechanisms.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (27)