IndisputableMonolith.URCAdapters.TcGrowth

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Scales
   3
   4namespace IndisputableMonolith
   5namespace URCAdapters
   6
   7/-! Simple computation growth interface wired to a concrete monotonicity lemma on PhiPow.
   8    We export a Prop that holds because PhiPow is strictly increasing when φ>1. -/
   9def tc_growth_prop : Prop :=
  10  ∀ x y : ℝ, x ≤ y → IndisputableMonolith.RecogSpec.PhiPow x ≤ IndisputableMonolith.RecogSpec.PhiPow y
  11
  12lemma tc_growth_holds : tc_growth_prop := by
  13  intro x y hxy
  14  -- PhiPow(x) = exp(log φ * x); since log φ > 0, it is monotone.
  15  have hφpos : 0 < IndisputableMonolith.Constants.phi := IndisputableMonolith.Constants.phi_pos
  16  have hlogpos : 0 < Real.log (IndisputableMonolith.Constants.phi) := by
  17    have hx : 0 ≤ IndisputableMonolith.Constants.phi := le_of_lt hφpos
  18    have hx1 : 1 < IndisputableMonolith.Constants.phi := IndisputableMonolith.Constants.one_lt_phi
  19    exact (Real.log_pos_iff hx).2 hx1
  20  dsimp [IndisputableMonolith.RecogSpec.PhiPow]
  21  -- Use monotonicity of exp and multiplication by positive scalar
  22  have : Real.log (IndisputableMonolith.Constants.phi) * x ≤ Real.log (IndisputableMonolith.Constants.phi) * y :=
  23    by exact mul_le_mul_of_nonneg_left hxy (le_of_lt hlogpos)
  24  exact (Real.exp_le_exp.mpr this)
  25
  26end URCAdapters
  27end IndisputableMonolith
  28