Erdos #142 Sub-Behrend Lower Bound Capstone Synthesis Theorem

Proved

erdos142_sub_behrend_capstone

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

Synthesis theorem uniting the compressed-base exponent constant reduction sqrt(8 log(1+delta)) < sqrt(8 log 2) with the Turan independent set density retention positivity.

Formal statement

import Mathlib

theorem erdos142_sub_behrend_capstone (delta : ℝ) (V_size : ℝ) (k : ℝ)
    (h_delta_pos : 0 < delta) (h_delta_lt : delta < 1)
    (hV : 0 < V_size) (hk : 0 ≤ k) :
    (Real.sqrt (8 * Real.log (1 + delta)) < Real.sqrt (8 * Real.log 2)) ∧
    (0 < V_size / (k + 1) ∧ V_size / (k + 1) ≤ V_size) := by sorry

View graph