Support lemmas for compact coverage certificates

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.bitSetB_or (left right : UInt64) (index : Fin 64) : bitSetB (left ||| right) ↑index = (bitSetB left ↑index || bitSetB right ↑index)

Bit testing reflects bitwise disjunction.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.bitSetB_and (left right : UInt64) (index : Fin 64) : bitSetB (left &&& right) ↑index = (bitSetB left ↑index && bitSetB right ↑index)

Bit testing reflects bitwise conjunction.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowIndexWord_eq_filter (rows : UInt64) (offset : ℕ) (hoffset : offset + 5 ≤ 64) : rowIndexWord rows offset = List.map (fun (index : ℕ) => offset + index) (List.filter (fun (index : ℕ) => bitSetB rows (offset + index)) (List.range 5))

One compact five-bit word enumerates exactly its set row indices.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowIndex_mem_word_of_bit (rows : UInt64) (index : Fin 35) (hbit : bitSetB rows ↑index = true) : ↑index ∈ rowIndexWord rows (5 * (↑index / 5))

Every set legal-row bit occurs in its unique compact five-row word.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowIndex_wordIndex_mem_range (index : Fin 35) : ↑index / 5 ∈ List.range 7

The compact word containing a legal-row index is one of the seven checked words.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.legalRows_bit (index : Fin 35) : bitSetB 34359738367 ↑index = true

The low-35-bit legal-row mask contains every legal row index.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.active_or_rejected_of_partition {active rejected incompatible : UInt64} (index : Fin 35) (hpartition : active ||| (rejected ||| incompatible) = 34359738367) (hcompatible : bitSetB incompatible ↑index = false) : bitSetB active ↑index = true ∨ bitSetB rejected ↑index = true

A complete row partition puts every cover-compatible legal row in either the active or semantically rejected mask.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.ConflictCover.Valid (cover : ConflictCover) : Prop

A conflict cover is sound when every rejected legal row contains one of its required pair bits at its recorded centre.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.ConflictCover.valid_of_validB {cover : ConflictCover} (hvalid : cover.validB = true) : cover.Valid

The finite cover audit implies semantic cover validity.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.conflictCoverLookup_valid_of_audit {identifier : ℕ} {cover : ConflictCover} (haudit : ∀ group ∈ conflictCoverGroups, ∀ entry ∈ group, entry.validB = true) (hlookup : conflictCoverLookup identifier = some cover) : cover.Valid

A table-wide audit makes every successful canonical cover lookup valid.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.requiredPairs_disjoint {state : PairState} {requiredPairs rowPairs : UInt64} (hrequired : requiredPairs &&& state.seenTwice = requiredPairs) (hcompatible : state.compatible rowPairs = true) : requiredPairs &&& rowPairs = 0

A required-pair submask is disjoint from every row accepted by the packed pair-state guard.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.requiredPairs_disjoint_of_pairState_exact {state : PairState} {assignments : List RowAssignment} (hexact : state.Exact assignments) (centre : Vertex) (rowIndex : Fin 35) (requiredPairs : UInt64) (hrequired : requiredPairs &&& state.seenTwice = requiredPairs) (hcompatible : pairCompatibleB assignments (searchRowChoiceAt centre rowIndex).rowMask = true) : requiredPairs &&& (searchRowChoiceAt centre rowIndex).pairMask = 0

A submask of the repeated pairs in an exact state is disjoint from every semantically compatible audited row.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.ConflictCover.compatible_row_not_incompatible {cover : ConflictCover} (hvalid : cover.Valid) {state : PairState} (centre : Vertex) (rowIndex : Fin 35) (hcentre : cover.centre = ↑centre) (hrequired : cover.requiredPairs &&& state.seenTwice = cover.requiredPairs) (hcompatible : state.compatible (searchRowChoiceAt centre rowIndex).pairMask = true) : bitSetB cover.incompatibleRows ↑rowIndex = false

An audited cover cannot mask a row accepted by the packed pair-state guard when its required pairs passed the subset gate.