IndisputableMonolith.Foundation.GrowthBounds
GrowthBounds module supplies a collection of inequalities for exponential and phi-power growth in the Recognition Science framework. It centers on Bernoulli's inequality and applies it to show phi^n and exp(x) exceed linear and cubic bounds. Researchers building the phi-ladder or mass formula cite these results. Proofs consist of direct applications of Mathlib real-analysis lemmas to the constants from the upstream module.
claimFor $a \geq 1$ and natural $n$, $a^n \geq 1 + n(a-1)$. Further results establish $\exp(x) ext{ exceeds linear bounds}$, $\phi^n$ exceeds linear and cubic polynomials, and density exceeds threshold, where $ au_0 = 1$ is the RS time quantum.
background
The module sits in the Foundation layer and imports Mathlib together with Constants. Constants fixes the RS-native time quantum as $ au_0 = 1$ tick. No new definitions appear; the module instead records quantitative growth controls needed for the phi-ladder and rung counting.
These controls rest on the golden-ratio fixed point phi forced at T6 and on the eight-tick octave at T7. The listed siblings (exp_ge_linear through density_exceeds_threshold) are the concrete statements that later steps invoke when comparing yardstick multiples to creation thresholds such as phi^{-1}.
proof idea
The module is a flat collection of independent lemmas. Each applies Bernoulli's inequality or the standard exp(x) >= 1+x bound to the specific constants phi and exponentials. No overarching tactic chain or term-mode reduction; each lemma is a one-line or short wrapper around Mathlib results.
why it matters in Recognition Science
These bounds close quantitative gaps in the forcing chain (T5 J-uniqueness through T8 D=3) by guaranteeing that phi-powers on the ladder surpass Berry and density thresholds. They supply the concrete estimates required by the mass formula yardstick * phi^(rung-8+gap(Z)) and by any downstream use of the Recognition Composition Law.
scope and limits
- Does not derive the numerical value of phi.
- Does not treat non-real bases or complex exponents.
- Does not prove convergence of infinite series.
- Does not connect directly to the alpha band or G constant.