Soundness of flat postorder coverage-certificate nodes #
Semantic validity accessors needed by the generic certificate proof.
- coverValid {identifier : ℕ} {cover : ConflictCover} : conflictCoverLookup identifier = some cover → cover.Valid
Every successful conflict-cover lookup is sound.
- patternValid {identifier : ℕ} {summary : PatternSummary} : densePatternSummaryLookup identifier = some summary → summary.Valid
Every successful dense pattern lookup is sound.
- hardValid {identifier : ℕ} {summary : HardSummary} : denseHardSummaryLookup identifier = some summary → summary.Valid
Every successful dense exact lookup is sound.
Instances For
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.impossible_of_patternIdentifier
(audits : CertificateAudits)
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
{assignments : List RowAssignment}
{code : UInt64}
(hassignments : AssignmentsMatch Q assignments)
(hcode : CodeMatches code assignments)
{identifier : ℕ}
(hidentifier : patternIdentifierPackedMatchesB identifier code = true)
:
A matching valid dense pattern identifier contradicts a realised convex table.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.BranchClaims.node_impossible
(audits : CertificateAudits)
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hSparse : Q.PairSparse)
(hBalanced : Q.Balanced)
(claims : BranchClaims)
(hlocally : claims.LocallyValid)
(identifier : ℕ)
:
identifier < claims.nodeCount →
∀ (assignments : List RowAssignment),
(List.map Prod.fst assignments).Perm (assignedCentres (claims.nodeAt identifier).depth) →
AssignmentsMatch Q assignments →
CodeMatches (claims.nodeAt identifier).code assignments →
{ seenOnce := (claims.nodeAt identifier).pairOnce, seenTwice := (claims.nodeAt identifier).pairTwice }.Exact
assignments →
False
A locally valid postorder node contradicts every matching semantic search prefix.