IntervalCover

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

def ConwaySoifer.Certificates.coverChain (stop : ℚ) : ℚ → List CertData → Bool

Consecutive coverage of (start, stop] by the intervals (C.lo, C.hi].

Equations

• ConwaySoifer.Certificates.coverChain stop x✝ [] = false
• ConwaySoifer.Certificates.coverChain stop x✝ [C] = (decide (C.lo ≤ x✝) && decide (stop ≤ C.hi))
• ConwaySoifer.Certificates.coverChain stop x✝ (C :: C' :: rest) = (decide (C.lo ≤ x✝) && ConwaySoifer.Certificates.coverChain stop C.hi (C' :: rest))

theorem ConwaySoifer.Certificates.coverChain_sound (stop : ℚ) (certs : List CertData) (cur : ℚ) : coverChain stop cur certs = true → ∀ (s : ℝ), ↑cur < s → s ≤ ↑stop → ∃ C ∈ certs, ↑C.lo < s ∧ s ≤ ↑C.hi