Semantic consequences of compact coverage certificates

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.AssignmentsMatch (Q : OctagonIncidence) (assignments : List RowAssignment) : Prop

Every stored assignment agrees with the corresponding mathematical row.

Equations

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.AssignmentsMatch.cons {Q : OctagonIncidence} {assignments : List RowAssignment} (hmatch : AssignmentsMatch Q assignments) (centre : Vertex) (row : UInt64) (hrow : Q.targets centre = packedRow row) : AssignmentsMatch Q ((centre, row) :: assignments)

Prepending a matching row preserves semantic assignment agreement.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.selectedByAssignmentsB_sound {Q : OctagonIncidence} {assignments : List RowAssignment} (hassignments : AssignmentsMatch Q assignments) {centre target : Vertex} (hselected : selectedByAssignmentsB assignments centre target = true) : target ∈ Q.targets centre

A selected bit in matching assignments is a mathematical incidence.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.selectedByAssignmentsB_complete_of_mem {Q : OctagonIncidence} {assignments : List RowAssignment} (hassignments : AssignmentsMatch Q assignments) {centre target : Vertex} (hcentre : centre ∈ List.map Prod.fst assignments) (hselected : target ∈ Q.targets centre) : selectedByAssignmentsB assignments centre target = true

A mathematical incidence is selected when its centre occurs in matching assignments.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignmentColumnBounds (Q : OctagonIncidence) (hBalanced : Q.Balanced) {assignments : List RowAssignment} {remaining : List Vertex} (hcentres : (List.map Prod.fst assignments ++ remaining).Perm (List.finRange 8)) (hassignments : AssignmentsMatch Q assignments) (target : Vertex) : assignmentColumnCount assignments target ≤ 4 ∧ 4 ≤ assignmentColumnCount assignments target + remainingColumnCapacity remaining target

Balanced incidence tables satisfy both semantic column bounds on a prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.pairCompatibleB_of_pairSparse_perm (Q : OctagonIncidence) (hSparse : Q.PairSparse) {assignments : List RowAssignment} {centre : Vertex} {remaining : List Vertex} {row : UInt64} (hcentres : (List.map Prod.fst assignments ++ centre :: remaining).Perm (List.finRange 8)) (hassignments : AssignmentsMatch Q assignments) (hrow : Q.targets centre = packedRow row) : pairCompatibleB assignments row = true

Pair sparsity accepts the actual next row of any permuted prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.impossible_of_patternSummary {p : Vertex → Plane} {Q : OctagonIncidence} (hC : ConvexIndependent ℝ p) (hR : Realises p Q) {code : UInt64} {assignments : List RowAssignment} {summary : PatternSummary} (hassignments : AssignmentsMatch Q assignments) (hcodeExact : CodeMatches code assignments) (hsummary : summary.Valid) (hmatch : (summary.mask &&& code == summary.mask) = true) : False

A valid monotone summary contradicts the realised convex configuration.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.impossible_of_hardSummary {p : Vertex → Plane} {Q : OctagonIncidence} (hC : ConvexIndependent ℝ p) (hR : Realises p Q) {code : UInt64} {assignments : List RowAssignment} {summary : HardSummary} (hcentres : (List.map Prod.fst assignments).Perm (List.finRange 8)) (hassignments : AssignmentsMatch Q assignments) (hcodeExact : CodeMatches code assignments) (hsummary : summary.Valid) (hmatch : (summary.code == code) = true) : False

A valid exact summary contradicts the realised convex configuration.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowFromCode_bit (code : UInt64) (centre target : Vertex) : bitSetB (rowFromCode code centre) ↑target = bitSetB code (varIndex centre target)

Reading a packed row preserves every one of its eight incidence bits.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignmentsFromCode_match {Q : OctagonIncidence} {code : UInt64} {assignments : List RowAssignment} {depth : ℕ} (hcentres : (List.map Prod.fst assignments).Perm (assignedCentres depth)) (hassignments : AssignmentsMatch Q assignments) (hcode : CodeMatches code assignments) : AssignmentsMatch Q (assignmentsFromCode code depth)

Exact packed code semantics reconstructs rows matching every assigned centre.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.searchCentres_drop_eq_cons (depth : ℕ) (hdepth : depth < searchCentres.length) : List.drop depth searchCentres = searchCentres.getD depth 0 :: List.drop (depth + 1) searchCentres

Search-centre suffixes expose the current centre followed by the next suffix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignedCentres_remaining_perm (depth : ℕ) (hdepth : depth ≤ searchCentres.length) : (assignedCentres depth ++ List.drop depth searchCentres).Perm (List.finRange 8)

Assigned centres followed by the search suffix enumerate all eight centres.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.nextAssignedCentres_perm (depth : ℕ) (hdepth : depth < searchCentres.length) : (searchCentres.getD depth 0 :: assignedCentres depth).Perm (assignedCentres (depth + 1))

Prepending the current search centre advances the assigned-centre prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.reconstructedCentres_perm (code row : UInt64) (depth : ℕ) (hdepth : depth < searchCentres.length) : (List.map Prod.fst ((searchCentres.getD depth 0, row) :: assignmentsFromCode code depth) ++ List.drop (depth + 1) searchCentres).Perm (List.finRange 8)

Reconstructed prefixes and the remaining search suffix cover all centres.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.initialAssignmentsMatch {Q : OctagonIncidence} (hN : Q.Normalized) (orbit : Fin 7) (hrowOne : Q.targets 1 = packedRow (canonicalRowMask orbit)) : AssignmentsMatch Q [(1, canonicalRowMask orbit), (0, 30)]

The normalized zeroth row and a canonical first row match the initial prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.initialCodeMatches (orbit : Fin 7) : CodeMatches (addRowCode (addRowCode 0 30 0) (canonicalRowMask orbit) 1) [(1, canonicalRowMask orbit), (0, 30)]

The packed two-row code exactly denotes the normalized canonical prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.initialAssignmentsMatchThree {Q : OctagonIncidence} (hN : Q.Normalized) (orbit : Fin 7) (hrowOne : Q.targets 1 = packedRow (canonicalRowMask orbit)) (rowTwo : Fin 35) (hrowTwo : Q.targets 2 = packedRow (rowTwoMask rowTwo)) : AssignmentsMatch Q [(2, rowTwoMask rowTwo), (1, canonicalRowMask orbit), (0, 30)]

Adding the indexed second row preserves semantic agreement with the prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.initialCodeMatchesThree (orbit : Fin 7) (rowTwo : Fin 35) : CodeMatches (addRowCode (addRowCode (addRowCode 0 30 0) (canonicalRowMask orbit) 1) (rowTwoMask rowTwo) 2) [(2, rowTwoMask rowTwo), (1, canonicalRowMask orbit), (0, 30)]

The packed three-row root code exactly denotes the fixed branch prefix.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.initialPairStateExactThree (orbit : Fin 7) (rowTwo : Fin 35) : have choice0 := searchChoiceForRow 0 30; have choice1 := searchChoiceForRow 1 (canonicalRowMask orbit); have choice2 := searchChoiceForRow 2 (rowTwoMask rowTwo); (((PairState.empty.add choice0.pairMask).add choice1.pairMask).add choice2.pairMask).Exact [(2, rowTwoMask rowTwo), (1, canonicalRowMask orbit), (0, 30)]

The packed three-row pair state exactly denotes the fixed branch prefix.