pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.GrowthBounds

show as:
view Lean formalization →

GrowthBounds supplies lower bounds on exponential and phi-power growth rates in the Recognition Science framework. It proves Bernoulli's inequality for a ≥ 1 and extends it to show phi-powers exceed linear and cubic terms. Researchers deriving mass ladders or density thresholds cite these results. The structure consists of inductive proofs building from the time quantum τ₀ = 1 tick.

claim$a ≥ 1 → a^n ≥ 1 + n(a-1)$ for natural $n$, together with bounds showing φ^k exceeds linear and cubic polynomials on the phi-ladder.

background

This module sits in the Foundation layer and imports the RS time quantum τ₀ = 1 tick from Constants. It develops growth comparisons needed to control the self-similar fixed point phi and the eight-tick octave. Bernoulli's inequality serves as the base case for all subsequent exponential bounds. Upstream, Constants fixes τ₀ as the fundamental tick, providing the discrete time setting for all growth arguments.

proof idea

The module proceeds by induction on the exponent for the base Bernoulli inequality, then specializes the result to phi-powers via the algebraic properties of the golden ratio fixed point. Later lemmas apply these to defeat cubic growth and set density thresholds.

why it matters in Recognition Science

These bounds close gaps in the forcing chain from T0 to T8 by ensuring exponential growth dominates lower-order terms, supporting the emergence of three spatial dimensions. They feed into mass formula derivations on the phi-ladder and the alpha inverse band.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)