Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Coverage

Exact half-open interval cover for the third-pass selection only.

source
def ConwaySoifer.Simplified.Certificates.caseCerts (c : Certificates.Case) :
List Certificates.CertData

Certificates belonging to the specified geometric contact case.

Equations
Instances For
    source
    def ConwaySoifer.Simplified.Certificates.caseStart :
    Certificates.Case → ℚ

    The endpoint where each case passes from a geometric proof to certificates.

    Equations
    Instances For
      source
      def ConwaySoifer.Simplified.Certificates.caseStop :
      Certificates.Case → ℚ

      The upper endpoint of each case's certificate chain.

      Equations
      Instances For
        source
        theorem ConwaySoifer.Simplified.Certificates.chain (c : Certificates.Case) :
        Certificates.coverChain (caseStop c) (caseStart c) (caseCerts c) = true
        source
        theorem ConwaySoifer.Simplified.Certificates.count_certificates :
        allData.length = 100
        source
        theorem ConwaySoifer.Simplified.Certificates.count_assignments :
        (List.map (fun (C : Certificates.CertData) => C.steps.length) allData).sum = 3188
        source
        theorem ConwaySoifer.Simplified.Certificates.counts_by_case :
        (caseCerts Certificates.Case.Sext).length = 26 ∧ (caseCerts Certificates.Case.Sint).length = 26 ∧ (caseCerts Certificates.Case.Aown).length = 26 ∧ (caseCerts Certificates.Case.Across).length = 22
        source
        theorem ConwaySoifer.Simplified.Certificates.assignments_by_case :
        (List.map (fun (C : Certificates.CertData) => C.steps.length) (caseCerts Certificates.Case.Sext)).sum = 1226 ∧ (List.map (fun (C : Certificates.CertData) => C.steps.length) (caseCerts Certificates.Case.Sint)).sum = 1165 ∧ (List.map (fun (C : Certificates.CertData) => C.steps.length) (caseCerts Certificates.Case.Aown)).sum = 688 ∧ (List.map (fun (C : Certificates.CertData) => C.steps.length) (caseCerts Certificates.Case.Across)).sum = 109
        source
        theorem ConwaySoifer.Simplified.Certificates.no_small_nonAcross :
        (allData.all fun (C : Certificates.CertData) => decide (C.case = Certificates.Case.Across) || !Certificates.smallHi C.hi) = true
        source
        theorem ConwaySoifer.Simplified.Certificates.caseExcluded (c : Certificates.Case) {T : Configuration} {r s : ℝ} (H : Canonical c.toContact T r s) (hlo : ↑(caseStart c) < s) (hhi : s ≤ ↑(caseStop c)) :
        False

        Each point in the retained interval is excluded by a checked shortened trace. No small-case geometric strengthening is required for these traces.

        source
        theorem ConwaySoifer.Simplified.Certificates.ranges_complete (c : Certificates.Case) {s : ℝ} (hs : 0 < s) :
        s ≤ ↑(caseStart c) ∨ ↑(caseStart c) < s ∧ s ≤ ↑(caseStop c) ∨ match c with | Certificates.Case.Sext => 1 / 3 ≤ s | Certificates.Case.Sint => 9 / 25 ≤ s | Certificates.Case.Aown => 7 / 20 ≤ s | Certificates.Case.Across => 3 / 25 ≤ s

        Closed geometric ranges join the original half-open intervals, including all overlaps. This arithmetic theorem is independent of the certificate evaluations.