Canonical validity of dense certificate summary identifiers #
def
Erdos97Octagon.RawIncidence.StaticDirectCoverage.patternSummaryCanonicalB
(summary : PatternSummary)
:
Check that a dense pattern summary agrees with its canonical source lookup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Erdos97Octagon.RawIncidence.StaticDirectCoverage.hardSummaryCanonicalB
(summary : HardSummary)
:
Check that a dense exact summary agrees with its canonical source lookup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.PatternSummary.valid_of_canonicalB
{summary : PatternSummary}
(hcanonical : patternSummaryCanonicalB summary = true)
:
summary.Valid
A successful canonical comparison supplies pattern-summary validity.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.HardSummary.valid_of_canonicalB
{summary : HardSummary}
(hcanonical : hardSummaryCanonicalB summary = true)
:
summary.Valid
A successful canonical comparison supplies exact-summary validity.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.densePatternSummaryLookup_valid_of_audit
{identifier : ℕ}
{summary : PatternSummary}
(haudit : ∀ group ∈ densePatternSummaryGroups, ∀ entry ∈ group, patternSummaryCanonicalB entry = true)
(hlookup : densePatternSummaryLookup identifier = some summary)
:
summary.Valid
A table-wide canonical audit validates every successful dense pattern lookup.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.denseHardSummaryLookup_valid_of_audit
{identifier : ℕ}
{summary : HardSummary}
(haudit : ∀ group ∈ denseHardSummaryGroups, ∀ entry ∈ group, hardSummaryCanonicalB entry = true)
(hlookup : denseHardSummaryLookup identifier = some summary)
:
summary.Valid
A table-wide canonical audit validates every successful dense exact lookup.