Separation of actual vertices in different clause boxes

The dilation separates the full closed boxes around distinct source vertices. Inside one box, the certified profile and its common injective affine placement distinguish every actual auxiliary and clause vertex. Inherited source-variable vertices stay at their shared centers.

Main results

• positiveVariablePoint_injective: occurring output variables occupy distinct actual points.
• positiveVariablePositions_nodup: the actual variable-position prefix has no repetitions.

References

These global placement and injectivity arguments are original.

def Cslib.Complexity.SAT.ExactOne.InPositiveLocalBox (p : Orthogonal.Point) : Prop

The common closed coordinate bounds of a local collared template.

theorem Cslib.Complexity.SAT.ExactOne.collarPoint_in_positiveBox (reflected : Bool) {p : Orthogonal.Point} (hp : 0 ≤ p.1 ∧ p.1 ≤ 180000 ∧ 0 ≤ p.2 ∧ p.2 ≤ 180000) : InPositiveLocalBox (collarPoint reflected p)

Affine placement sends every point of the inner square strictly inside the collar box.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_auxiliary_bounds (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables (clauseProfile c)) (ha : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) : InPositiveLocalBox ((clauseGeometry φ d i c).variablePosition (List.idxOf v (profileVariables (clauseProfile c))))

Every private actual variable lies in its own fixed collared box.

theorem Cslib.Complexity.SAT.ExactOne.positiveBox_owner_injective {a b q r : Orthogonal.Point} (hq : InPositiveLocalBox q) (hr : InPositiveLocalBox r) (he : positiveScale • a + q = positiveScale • b + r) : a = b

Equal placed points in closed local boxes determine the same integer source center.

theorem Cslib.Complexity.SAT.ExactOne.sourceClause_declared (φ : Logic.PL.CNF ℕ) {i : ℕ} (hi : i < List.length φ) : φ.distinctVars.length + i ∈ (incidenceGraph φ).1

A source clause's incidence-graph vertex is declared.

theorem Cslib.Complexity.SAT.ExactOne.sourceVariable_declared (φ : Logic.PL.CNF ℕ) {v : ℕ} (hv : v ∈ φ.vars) : List.idxOf v φ.distinctVars ∈ (incidenceGraph φ).1

A used source variable's incidence-graph vertex is declared.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_auxiliary_injective (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables (clauseProfile c)) (hw : w ∈ profileVariables (clauseProfile c)) (hva : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) (hwa : ∀ (n : ℕ), w ≠ Sum.inl (Sum.inl n)) (he : (clauseGeometry φ d i c).variablePosition (List.idxOf v (profileVariables (clauseProfile c))) = (clauseGeometry φ d i c).variablePosition (List.idxOf w (profileVariables (clauseProfile c)))) : v = w

Two private profile variables in one actual clause box have different points.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryPositions_point_injective {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p q : Orthogonal.Point} (hv : (v, p) ∈ positiveAuxiliaryPositions φ d) (hw : (w, q) ∈ positiveAuxiliaryPositions φ d) (he : p = q) : v = w

Equal points of two fresh-variable table entries have the same actual variable key.

theorem Cslib.Complexity.SAT.ExactOne.positiveSourceAuxiliary_positions_disjoint {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p q : Orthogonal.Point} (hv : (v, p) ∈ positiveSourcePositions φ d) (hw : (w, q) ∈ positiveAuxiliaryPositions φ d) : p ≠ q

A shared source-variable point cannot coincide with any private clause-box point.

theorem Cslib.Complexity.SAT.ExactOne.positiveSourcePositions_point_injective {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p q : Orthogonal.Point} (hv : (v, p) ∈ positiveSourcePositions φ d) (hw : (w, q) ∈ positiveSourcePositions φ d) (he : p = q) : v = w

Shared source-position table entries are injective in their actual source-variable names.

theorem Cslib.Complexity.SAT.ExactOne.positivePositionTable_point_injective {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p q : Orthogonal.Point} (hv : (v, p) ∈ positivePositionTable φ d) (hw : (w, q) ∈ positivePositionTable φ d) (he : p = q) : v = w

The actual position-table map is injective on all its entries.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_injective {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).vars) (hw : w ∈ (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).vars) (he : positiveVariablePoint φ d v = positiveVariablePoint φ d w) : v = w

Distinct occurring output variables occupy distinct actual positions.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePositions_nodup {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) : (List.map (positiveVariablePoint φ d) (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).distinctVars).Nodup

The actual variable-position prefix of the emitted drawing has no repetitions.