Documentation

LeanPool.Erdos97ConvexOctagon.CoverageSummaryData12

Lightweight coverage summaries, buckets 96–103 #

source
def Erdos97Octagon.RawIncidence.patternSummaryBuckets12 :
Array (List PatternSummary)

Lightweight monotone-obstruction summaries for this hash-bucket group.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Erdos97Octagon.RawIncidence.hardSummaryBuckets12 :
    Array (List HardSummary)

    Lightweight exact-table summaries for this hash-bucket group.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Erdos97Octagon.RawIncidence.patternSummaryBuckets12_valid :
      (patternSummaryBuckets12.toList.all fun (bucket : List PatternSummary) => bucket.all (PatternSummary.validAgainstB patternBuckets12)) = true

      Every pattern summary in this shard resolves to a valid obstruction entry.

      source
      theorem Erdos97Octagon.RawIncidence.hardSummaryBuckets12_valid :
      (hardSummaryBuckets12.toList.all fun (bucket : List HardSummary) => bucket.all (HardSummary.validAgainstB hardBuckets12)) = true

      Every hard summary in this shard resolves to a valid exact-table entry.