IndisputableMonolith.Numerics.IntervalProofs
The IntervalProofs module supplies lemmas establishing strict monotonicity of the exponential and power functions, the algebraic identity satisfied by the golden ratio phi, and tight interval bounds on phi together with its logarithm. Researchers auditing numerical steps in the Recognition Science formalization cite these lemmas to justify machine-checked bounds on constants. The module consists of independent short proofs that apply Mathlib interval tactics and linear arithmetic to derive exact inequalities.
claimThe module proves that the map $xmapsto e^x$ is strictly increasing on $mathbb{R}$, that $x mapsto x^y$ is strictly monotone for fixed $y>0$, that $phi^2=phi+1$ where $phi=(1+sqrt{5})/2$, and that $phi$ and $log phi$ lie in explicit closed intervals obtained from their definitions.
background
This module resides in the Numerics domain and supplies supporting facts for the Recognition Science framework. It imports Mathlib real analysis, special functions for exp, log, pow and sqrt, the golden-ratio definition, and tactics for interval cases and linear arithmetic. No new RS concepts such as J-cost or defectDist appear; the lemmas instead deliver the numerical precision required for phi as the self-similar fixed point. Upstream results include the standard derivative of exp and the minimal polynomial of phi.
proof idea
The module contains several independent lemmas. Monotonicity statements follow from positivity of the derivative of exp or from the sign of the exponent. The identity phi_sq is obtained by direct algebraic simplification of the golden-ratio definition. Bound lemmas invoke the interval_cases tactic to partition the reals, then close each case with linarith or norm_num.
why it matters in Recognition Science
These lemmas feed into parent theorems that derive physical constants from the phi-ladder and the Recognition Composition Law. They supply the verified numerical content needed for the T6 forcing step that identifies phi as the self-similar fixed point and for placing alpha inverse inside (137.030, 137.039). The module thereby closes numerical gaps that would otherwise remain in the eight-tick octave and mass-formula constructions.
scope and limits
- Does not derive physical laws or constants from first principles.
- Does not interact directly with the J-function or Recognition Composition Law.
- Does not contain proofs of the main forcing-chain theorems T0-T8.