Common hash scale under numerator multiplication

Proved

mme_common_hash_scale_le_mul

by Robertboy18 · Sep 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

regional-extractiontensor-complexity

If d is at least one and every new load numerator is at most d times the old numerator, the common hash scale is at most d times the original common scale. The proof includes the integer quotient rounding and zero-denominator cases.

Preamble

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

Formal statement

theorem mme_common_hash_scale_le_mul {J : Type*} [Fintype J]
    (grade d : ℕ) (hd : 1 ≤ d) (num num' den : J → ℕ)
    (hnum : ∀ j, num' j ≤ d * num j) :
    commonScale grade num' den ≤ d * commonScale grade num den := by sorry

Source

Selected-count logarithms and uniformly controlled repair for the concrete released regional extraction.

View graph