IndisputableMonolith.Numerics.IntervalProofs
The Numerics.IntervalProofs module collects convenience lemmas for strict monotonicity of the exponential and power functions together with explicit bounds on the golden ratio phi and log phi. These support interval-based numerical verification inside the Recognition Science framework. Proofs are built from Mathlib analysis primitives and interval tactics.
claimLemmas establishing that $x < y$ implies $e^x < e^y$, $x < y$ implies $x^r < y^r$ for $r > 0$, the identity $phi^2 = phi + 1$, explicit lower and upper bounds on $phi$, and a bound on $log phi$.
background
The module sits in the Numerics domain and imports Mathlib components for real analysis, exp, pow, log, sqrt, the golden-ratio definition, and tactics (IntervalCases, Linarith, NormNum). It supplies supporting results for the phi-ladder and J-cost calculations that appear throughout Recognition Science. The local setting is the numerical verification of inequalities required by the forcing chain T5-T8 and the Recognition Composition Law.
proof idea
The module consists of several independent lemmas. Each is proved in tactic mode by applying interval case analysis, linear arithmetic, and norm_num to discharge the required inequalities; no single central argument exists.
why it matters in Recognition Science
These lemmas supply the numerical infrastructure needed to certify bounds on alpha inverse and the phi-based mass formula. They feed parent results in the UnifiedForcingChain and related modules that close the T5 J-uniqueness step and the D=3 spatial-dimension claim.
scope and limits
- Does not prove the central Recognition Science functional equation.
- Does not compute any physical constants or mass values.
- Limited to the listed bounds on exp, phi, and log.