Repair changes the regional hash logarithm by at most log d

import Definitions.Def_mme_recursive_region_hash_loads
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
open BigOperators MME MME.RecursiveYZ MME.RegionRealization
open scoped Classical
set_option autoImplicit false
universe u

theorem mme_regional_hash_log_scale_le_repair_log
    {half R ell : ℕ} {parent : Fin R → Fin 3 → ℕ} {n : Fin R → ℕ}
    (htotal : ∀ r, parent r 0 + parent r 1 + parent r 2 = 2 * half)
    (m : ∀ r, RecursiveThinSplit.Split half (parent r) → ℕ) (d : ℕ) (hd : 1 ≤ d)
    (mu : Fin 2 → Cell half R parent → CompleteSplit.CompleteWord ell → ℕ)
    (keep : Fin 2 → Address half R parent n →
      (Position n → CompleteSplit.CompleteWord ell) → Prop) :
    Real.log (commonScale half (loadNum htotal m d mu keep) (loadDen m)) ≤
      Real.log d + Real.log (commonScale half (loadNum htotal m 1 mu keep) (loadDen m)) := by sorry