Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateDenseSummaryValidity

Global validity of dense certificate summaries #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.densePatternSummaryLookup_valid {identifier : ℕ} {summary : PatternSummary} (hlookup : densePatternSummaryLookup identifier = some summary) :
summary.Valid

Every successful dense pattern-summary lookup is semantically valid.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.denseHardSummaryLookup_valid {identifier : ℕ} {summary : HardSummary} (hlookup : denseHardSummaryLookup identifier = some summary) :
summary.Valid

Every successful dense exact-summary lookup is semantically valid.