Prove2Me

Positivity of the trimmed-cover multiplicity exponent

Proved
ThreeSum.Parameters.kappa_positive

by wurtle · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

3sumalgorithmsfine-grained-complexitythree-sum-1962word-ram

Let H2(t)=−tlog⁡2t−(1−t)log⁡2(1−t)H_2(t)=-t\log_2t-(1-t)\log_2(1-t) denote binary entropy. Define the fixed real parameter

κ=512H2(1/512)−256H2(1/256)−1.\kappa=512H_2(1/512)-256H_2(1/256)-1.

Then

κ>0.\kappa>0.

This parameter is the vertex-multiplicity exponent appearing in the trimmed local-cover analysis at the chosen scale. The assertion is an exact real inequality for the stated constants.

Its positivity is used when comparing the multiplicity factors and their logarithmic growth rates in the resource analysis.

Preamble
import Definitions.Def_ThreeSum1962Source_Bundle01
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring


set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option Elab.async false
Formal statement
theorem ThreeSum.Parameters.kappa_positive : @LT.lt.{0} Real Real.instLT (@OfNat.ofNat.{0} Real (nat_lit 0) (@Zero.toOfNat0.{0} Real Real.instZero))
  ThreeSum.Parameters.kappa := by
  sorry
Source
https://github.com/c0ldzy17/three-sum-lean/blob/2b639655e07421b9ac743de9090459bab473a7c0/Submission/ThreeSum/Parameters.lean#L166-L177

View graph