`ScalingModel`

definition

show as: view math explainer →

module: IndisputableMonolith.TruthCore.MRD.Scaling
domain: TruthCore
line: 7 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.TruthCore.MRD.Scaling on GitHub at line 7.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

   4namespace TruthCore
   5namespace MRD
   6
   7structure ScalingModel where
   8  gamma : ℝ
   9  f     : ℝ → ℝ → ℝ
  10  f_hom0 : ∀ {c t1 t2}, 0 < c → f (c * t1) (c * t2) = f t1 t2
  11
  12noncomputable section
  13
  14@[simp] noncomputable def predicted_ratio (M : ScalingModel) (tau_m1 tau_m2 tau_f : ℝ) : ℝ :=
  15  ((tau_m1 / tau_m2) ^ M.gamma) * M.f (tau_m1 / tau_f) (tau_m2 / tau_f)
  16
  17lemma predicted_ratio_rescale (M : ScalingModel)
  18  (c tau_m1 tau_m2 tau_f : ℝ) (hc : 0 < c) :
  19  predicted_ratio M (c * tau_m1) (c * tau_m2) (c * tau_f)
  20    = predicted_ratio M tau_m1 tau_m2 tau_f := by
  21  dsimp [predicted_ratio]
  22  have h12 : (c * tau_m1) / (c * tau_m2) = tau_m1 / tau_m2 := by
  23    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  24    field_simp [hc0]
  25  have h1f : (c * tau_m1) / (c * tau_f) = tau_m1 / tau_f := by
  26    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  27    field_simp [hc0]
  28  have h2f : (c * tau_m2) / (c * tau_f) = tau_m2 / tau_f := by
  29    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  30    field_simp [hc0]
  31  have hf : M.f ((c * tau_m1) / (c * tau_f)) ((c * tau_m2) / (c * tau_f))
  32            = M.f (tau_m1 / tau_f) (tau_m2 / tau_f) := by
  33    simpa [h1f, h2f, one_mul] using
  34      (M.f_hom0 (c:=1) (t1:=tau_m1 / tau_f) (t2:=tau_m2 / tau_f) (by norm_num))
  35  simp [h12, hf]
  36
  37end

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.