Cardinal port selection for actual source incidences

The side convention agrees with the finite collar tables. Any zero, one, two, or three distinct prescribed source exits extends to one of the twenty-four ordered three-port assignments.

Main definitions

• directionSide, sideDirection: cardinal-vector and collar-side conversion.
• choosePorts: finite deterministic completion of a partial source exit assignment.

Main results

• sideDirection_directionSide: cardinal directions are preserved exactly.
• portsMatch_iff: matching is equality at every present indexed port.
• choosePorts_spec: the selected ports are distinct and retain every present source exit.

References

These finite collar-selection and geometric indexing proofs are original.

def Cslib.Complexity.SAT.ExactOne.sideDirection (s : Fin 4) : Orthogonal.Point

Collar sides are numbered left, right, bottom, top.

def Cslib.Complexity.SAT.ExactOne.directionSide (v : Orthogonal.Point) : Fin 4

Classify a cardinal direction using the collar side convention.

theorem Cslib.Complexity.SAT.ExactOne.sideDirection_directionSide {v : Orthogonal.Point} (hv : Orthogonal.UnitVector v) : sideDirection (directionSide v) = v

Converting a unit direction to its collar side and back recovers it.

theorem Cslib.Complexity.SAT.ExactOne.directionSide_injective {v w : Orthogonal.Point} (hv : Orthogonal.UnitVector v) (hw : Orthogonal.UnitVector w) (he : directionSide v = directionSide w) : v = w

Distinct unit vectors are classified as distinct collar sides.

def Cslib.Complexity.SAT.ExactOne.portsMatch (n a b c : Fin 4) (s : PortAssignment) : Bool

Check the source exits that are present in a clause of the indicated length.

theorem Cslib.Complexity.SAT.ExactOne.portsMatch_iff (n a b c : Fin 4) (s : PortAssignment) : portsMatch n a b c s = true ↔ ∀ (j : Fin 3), ↑j < ↑n → s.side j = PortAssignment.side (a, b, c) j

Matching constrains exactly the indexed ports that are present in the source clause.

def Cslib.Complexity.SAT.ExactOne.choosePorts (n a b c : Fin 4) : PortAssignment

Select the first ordered collar assignment extending the present source exits.

def Cslib.Complexity.SAT.ExactOne.PresentDirectionsDistinct (n a b c : Fin 4) : Prop

A partial source assignment needs pairwise distinct exits exactly at its present positions.

@[instance_reducible]

instance Cslib.Complexity.SAT.ExactOne.instDecidablePresentDirectionsDistinct (n a b c : Fin 4) : Decidable (PresentDirectionsDistinct n a b c)

theorem Cslib.Complexity.SAT.ExactOne.choosePorts_spec (n a b c : Fin 4) (h : PresentDirectionsDistinct n a b c) : (choosePorts n a b c).Distinct ∧ portsMatch n a b c (choosePorts n a b c) = true

Every admissible partial exit assignment has a deterministic distinct collar completion.

theorem Cslib.Complexity.SAT.ExactOne.choosePorts_matches (n a b c : Fin 4) (h : PresentDirectionsDistinct n a b c) (j : Fin 3) (hj : ↑j < ↑n) : (choosePorts n a b c).side j = PortAssignment.side (a, b, c) j

Each prescribed exit is retained by the selected collar assignment.

def Cslib.Complexity.SAT.ExactOne.sourceOccurrence (φ : Logic.PL.CNF ℕ) (i j : ℕ) : Logic.PL.Occurrence ℕ

A literal position identifies its own incidence, including repeated literals.

def Cslib.Complexity.SAT.ExactOne.sourceEdgeIndex (φ : Logic.PL.CNF ℕ) (i j : ℕ) : ℕ

The actual source edge position of a clause/literal occurrence.

def Cslib.Complexity.SAT.ExactOne.literalSide (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i j : ℕ) : Fin 4

The actual cardinal exit of one source literal.

def Cslib.Complexity.SAT.ExactOne.clausePorts (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) : PortAssignment

Complete the present exits to a deterministic ordered collar.

theorem Cslib.Complexity.SAT.ExactOne.sourceOccurrence_mem (φ : Logic.PL.CNF ℕ) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) : sourceOccurrence φ i j ∈ Logic.PL.occurrences φ

Existing clause and literal indices identify an actual source occurrence.

theorem Cslib.Complexity.SAT.ExactOne.sourceEdgeIndex_lt (φ : Logic.PL.CNF ℕ) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) : sourceEdgeIndex φ i j < (incidenceGraph φ).edges.length

Every actual source occurrence has a valid incidence-list index.

theorem Cslib.Complexity.SAT.ExactOne.sourceEdgeIndex_edge (φ : Logic.PL.CNF ℕ) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) : (incidenceGraph φ).edges.getD (sourceEdgeIndex φ i j) (0, 0) = (List.idxOf φ[i][j].1 φ.distinctVars, φ.distinctVars.length + i)

Source edge lookup recovers the actual variable and clause endpoints.

theorem Cslib.Complexity.SAT.ExactOne.sourceEdgeIndex_ne (φ : Logic.PL.CNF ℕ) {i j k : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) (_hk : k < List.length φ[i]) (hjk : j ≠ k) : sourceEdgeIndex φ i j ≠ sourceEdgeIndex φ i k

Distinct source literal positions have distinct listed source edges.

theorem Cslib.Complexity.SAT.ExactOne.literalSide_ne {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j k : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) (hk : k < List.length φ[i]) (hjk : j ≠ k) : literalSide φ d i j ≠ literalSide φ d i k

Actual source literal exits at the same clause have distinct collar sides.

theorem Cslib.Complexity.SAT.ExactOne.clausePorts_spec {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) : (clausePorts φ d i).Distinct ∧ portsMatch ⟨min (List.length (List.getD φ i [])) 3, ⋯⟩ (literalSide φ d i 0) (literalSide φ d i 1) (literalSide φ d i 2) (clausePorts φ d i) = true

A valid source drawing supplies a distinct ordered collar for every actual clause.

theorem Cslib.Complexity.SAT.ExactOne.clausePorts_side {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (j : Fin 3) (hj : ↑j < List.length φ[i]) : (clausePorts φ d i).side j = literalSide φ d i ↑j

Each present source literal uses its actual cardinal side in the selected collar.

theorem Cslib.Complexity.SAT.ExactOne.collarOuterPort_eq_center_add (s : Fin 4) : collarOuterPort s = (270000, 270000) + 270000 • sideDirection s

A collar's midpoint is its center plus its cardinal radius vector.