Global validity of the generated conflict covers

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.conflictCoverGroups_entry_valid (group : Array ConflictCover) (hgroup : group ∈ conflictCoverGroups) (cover : ConflictCover) (hcover : cover ∈ group) : cover.validB = true

Every entry in the complete generated conflict-cover table is valid.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.conflictCoverLookup_valid {identifier : ℕ} {cover : ConflictCover} (hlookup : conflictCoverLookup identifier = some cover) : cover.Valid

Every successful generated conflict-cover lookup is semantically sound.