Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateLookup

Canonical lookup and validity of coverage summaries #

source
def Erdos97Octagon.RawIncidence.StaticDirectCoverage.patternSummaryForOriginLookup (origin : ℕ) :
Option PatternSummary

Retrieve the generated pattern summary having one source origin.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Erdos97Octagon.RawIncidence.StaticDirectCoverage.hardSummaryForOriginLookup (origin : ℕ) :
    Option HardSummary

    Retrieve the generated hard summary having one source origin.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.patternSummaryForOriginLookup_valid {origin : ℕ} {summary : PatternSummary} (hlookup : patternSummaryForOriginLookup origin = some summary) :
      summary.Valid

      Every pattern returned by the canonical origin lookup is globally audited.

      source
      theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.hardSummaryForOriginLookup_valid {origin : ℕ} {summary : HardSummary} (hlookup : hardSummaryForOriginLookup origin = some summary) :
      summary.Valid

      Every exact summary returned by the canonical origin lookup is globally audited.