module module high

`IndisputableMonolith.Numerics.Interval.Log`

The Numerics.Interval.Log module supplies verified interval bounds for the natural logarithm, centered on the inequality log(x) >= 1 - 1/x for x > 0 together with monotonicity and phi-specific containments. Interval users in power computations and tactic libraries cite it when deriving bounds for exp(y log x) or thermodynamic expressions. Proofs reduce to standard calculus inequalities inside the rational-endpoint arithmetic of the Basic module.

claim$log x >= 1 - 1/x$ for $x > 0$, with interval monotonicity $logIntervalMono$ and containment results such as $logPhiInterval$ that respect rational endpoints.

background

The module sits inside the Verified Interval Arithmetic setting, which bounds real numbers by rational endpoints that Lean can compute exactly. It imports algebraic bounds on phi = (1 + sqrt(5))/2 obtained from comparing squares 2.236^2 < 5 < 2.237^2. These ingredients enable safe enclosure of transcendental functions needed for Recognition Science numerics.

proof idea

The module consists of lemmas (logLowerSimple, logUpperSimple, logIntervalMono, logPhiInterval, etc.) proved by direct application of the inequality log(x) >= 1 - 1/x, monotonicity of log, and interval arithmetic rules imported from Basic and PhiBounds. No single large tactic script; each lemma is a short algebraic reduction or containment check.

why it matters in Recognition Science

Supplies the log bounds required by Numerics.Interval.Pow (via x^y = exp(y log x)), Numerics.Interval.Tactic (interval_bound tactic), Chemistry.SuperconductingTc (phi-ladder energy scales), and Papers.GCIC.Thermodynamics (GCIC phase constants). It therefore supports the phi-ladder and eight-tick coherence steps in the RS forcing chain.

scope and limits

Does not treat complex logarithms or branch cuts.
Does not supply bounds for x <= 0.
Does not include Taylor remainder estimates beyond the listed simple bounds.
Does not produce floating-point or arbitrary-precision numeric output.

used by (4)

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

IndisputableMonolith.Chemistry.SuperconductingTc module_import
IndisputableMonolith.Numerics.Interval.Pow module_import
IndisputableMonolith.Numerics.Interval.Tactic module_import
IndisputableMonolith.Papers.GCIC.Thermodynamics module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Numerics.Interval.Basic module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import

declarations in this module (27)

def logLowerSimple L31
def logUpperSimple L34
def logIntervalMono L37
theorem logIntervalMono_contains_log L46
def logPhiInterval L69
lemma phi_minus_one_abs L92
lemma phi_minus_one_abs_lt_one L96
lemma complex_norm_ofReal L101
lemma log_taylor_error_bound L106
lemma log_one_add_bounds L136
def exp_taylor_10_at_048 L179
def exp_error_10_at_048 L184
lemma exp_048_lt_phi L189
theorem log_phi_gt_048 L196
def exp_taylor_10_at_0481 L222
def exp_error_10_at_0481 L227
lemma exp_0481_lt_phi L232
theorem log_phi_gt_0481 L239
def exp_taylor_10_at_0483 L262
def exp_error_10_at_0483 L267
lemma phi_lt_exp_0483 L272
theorem log_phi_lt_0483 L279
theorem log_phi_in_interval L312
def log2Interval L333
theorem log_2_in_interval L339
def log10Interval L358
theorem log_10_in_interval L369