theorem proved term proof

`phi_rung_complexity_unbounded`

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

formal statement (Lean)

 189theorem phi_rung_complexity_unbounded (M : ℝ) : ∃ n : ℕ, phi ^ n > M :=

proof body

Term-mode proof.

 190  pow_unbounded_of_one_lt M one_lt_phi
 191
 192/-- **THEOREM IC-005.16**: Gradient descent on J-cost converges toward x = 1.
 193    For x > 1: one gradient step x₁ = x₀ - η J'(x₀) moves closer to x = 1.
 194    This makes J-cost minimization efficiently solvable. -/

depends on (13)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
gradient in IndisputableMonolith.Relativity.Fields.Scalar decl_use