theorem proved term proof

`phi_hierarchy_exponential`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 184theorem phi_hierarchy_exponential : phi > 1 := one_lt_phi

proof body

Term-mode proof.

 185
 186/-- **THEOREM IC-005.15**: φⁿ grows without bound.
 187    For any bound M, there exists n such that φⁿ > M.
 188    This places the computation of high-rung RS states in EXPTIME. -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
rung in IndisputableMonolith.Compat.Constants decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use