Global continuous contacts of the actual positive incidence routes #

Main results #

positiveStem_different_boxes_disjoint: local prefixes of different clauses have disjoint supports.
positiveExterior_foreign_box: exterior routes avoid other clauses' closed boxes.
positiveStem_foreign_exterior_disjoint: a local prefix is disjoint from the exterior routes of other clauses.
positiveIncidenceRoute_endpoints: actual clause and globally shared variable endpoints.
positiveIncidenceRoute_contacts: full real-support contacts only at actual common endpoints.

References #

These continuous route-composition proofs are original.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_different_boxes_disjoint {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hij : i ≠ j) (c c' : Logic.PL.Clause ℕ) {e f : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) (hf : f ∈ (clauseGeometry φ d j c').incidenceRoutes) :

Disjoint (Orthogonal.support (positiveStem φ d i e)) (Orthogonal.support (positiveStem φ d j f))

Local prefixes belonging to different original clauses have disjoint full supports.

source

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_foreign_box {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j k : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hk : k < List.length φ[j]) (hij : i ≠ j) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support (positiveExterior φ d j k)) :

¬Orthogonal.inPointBox (positiveBoxOrigin φ d i + positiveTranslation) positiveRadius z

An inherited exterior route avoids every other original clause's entire closed box.

source

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_foreign_exterior_disjoint {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j k : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hk : k < List.length φ[j]) (hij : i ≠ j) (c : Logic.PL.Clause ℕ) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) :

Disjoint (Orthogonal.support (positiveStem φ d i e)) (Orthogonal.support (positiveExterior φ d j k))

A finite local prefix and an inherited route from another clause are disjoint.

source

def Cslib.Complexity.SAT.ExactOne.positiveIncidenceVariable (φ : Logic.PL.CNF ℕ) (i : ℕ) (c : Logic.PL.Clause ℕ) (e : LocalIncidence) :

Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ

The actual global variable attached to one local incidence row.

Instances For

source

theorem Cslib.Complexity.SAT.ExactOne.positiveIncidenceRoute_endpoints {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (h : (profilePrefixGeometry (clauseProfile φ[i])).PrefixCheck) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i φ[i]).incidenceRoutes) :

List.head? (positiveIncidenceRoute φ d i φ[i] e) = some (positiveBoxOrigin φ d i + (clauseGeometry φ d i φ[i]).clausePosition e.clauseIndex) ∧ List.getLast? (positiveIncidenceRoute φ d i φ[i] e) = some (positiveVariablePoint φ d (positiveIncidenceVariable φ i φ[i] e))

Actual emitted incidences have their specified local clause and globally shared variable endpoints. Private variables resolve through the actual finite position table.

source

theorem Cslib.Complexity.SAT.ExactOne.mem_support_positiveIncidenceRoute_iff {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (h : (profilePrefixGeometry (clauseProfile φ[i])).PrefixCheck) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i φ[i]).incidenceRoutes) {z : ℝ × ℝ} :

z ∈ Orthogonal.support (positiveIncidenceRoute φ d i φ[i] e) ↔ z ∈ Orthogonal.support (positiveStem φ d i e) ∨ ∃ (j : ℕ), (profileVariables (clauseProfile φ[i])).getD e.variableIndex (Sum.inl (Sum.inl 0)) = Sum.inl (Sum.inl j) ∧ z ∈ Orthogonal.support (positiveExterior φ d i j)

Full support of an emitted route splits into its finite stem and, for a source placeholder only, the inherited exterior support.

source

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_contacts {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j k l : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hk : k < List.length φ[i]) (hl : l < List.length φ[j]) (hne : (i, k) ≠ (j, l)) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support (positiveExterior φ d i k)) (hw : z ∈ Orthogonal.support (positiveExterior φ d j l)) :

φ[i][k].1 = φ[j][l].1 ∧ z = Orthogonal.realPoint (positiveVariablePoint φ d (Sum.inl (Sum.inl φ[i][k].1)))

Distinct inherited source incidences meet only at an actual common source-variable point, including repeated literals and distinct occurrences with equal signed variable names.

source