The actual positive exact-one drawing compiler

Every source clause is replaced by its positive exact-one profile with a collar matching the source exit directions. Source variable vertices remain shared at scaled positions. Private source placeholders are removed, and their incidences join the trimmed source routes.

Main definitions

• positiveDrawing: finite drawing data for the actual positive exact-one output formula.
• positivePlacedClauses: clause records in the actual compiler's list order.
• PositivePlacedClause: a placed clause record, read through clause, point and routes.

Main results

• positivePlacedClauses_formula: exact agreement with the actual logical formula.

References

The finite-profile assembly and its explicit placement are original.

def Cslib.Complexity.SAT.ExactOne.positiveRadius : ℕ

The common radius of all collared positive clause replacements.

def Cslib.Complexity.SAT.ExactOne.positiveScale : ℕ

Dilation separates all closed clause boxes.

def Cslib.Complexity.SAT.ExactOne.positiveTranslation : Orthogonal.Point

Translate away from the source coordinate axes.

def Cslib.Complexity.SAT.ExactOne.clauseGeometry (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : LocalGeometry

The collared local geometry selected for one original clause.

def Cslib.Complexity.SAT.ExactOne.positiveBoxOrigin (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Point

The lower-left corner of one replacement box.

def Cslib.Complexity.SAT.ExactOne.positiveExterior (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i j : ℕ) : Orthogonal.Route

The inherited route outside its own local replacement box.

def Cslib.Complexity.SAT.ExactOne.positiveIncidenceRoute (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) (e : LocalIncidence) : Orthogonal.Route

A source prefix joins its inherited route; an auxiliary prefix already ends at its variable.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.PositivePlacedClause : Type

An actual clause, its position, and its literal routes in literal order.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.PositivePlacedClause.clause (pc : PositivePlacedClause) : Logic.PL.Clause (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)

The output clause.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.PositivePlacedClause.point (pc : PositivePlacedClause) : Orthogonal.Point

The position of the clause vertex.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.PositivePlacedClause.routes (pc : PositivePlacedClause) : List Orthogonal.Route

The routes of the clause's literals, in literal order.

def Cslib.Complexity.SAT.ExactOne.positiveClauseBlock (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : List PositivePlacedClause

One original clause's output, using its actual global auxiliary offsets.

def Cslib.Complexity.SAT.ExactOne.positivePlacedClauses (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : List PositivePlacedClause

Actual output clause records in source-block and local-clause order.

def Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryBlock (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : List (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ × Orthogonal.Point)

Fresh-variable positions in one clause box; source placeholders are omitted.

def Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryPositions (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : List (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ × Orthogonal.Point)

The finite position table for actual output auxiliaries.

def Cslib.Complexity.SAT.ExactOne.positiveSourcePositions (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : List (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ × Orthogonal.Point)

Shared original-variable vertices are listed before the fresh-variable position records.

def Cslib.Complexity.SAT.ExactOne.positivePositionTable (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : List (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ × Orthogonal.Point)

The position table keeps both shared source vertices and fresh clause-box vertices.

def Cslib.Complexity.SAT.ExactOne.positiveVariablePoint (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ) : Orthogonal.Point

Read the position of an actual output variable from the finite position table.

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

The actual compact output drawing omits all private source-placeholder vertices.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_source (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {v : ℕ} (hv : v ∈ φ.vars) : positiveVariablePoint φ d (Sum.inl (Sum.inl v)) = positiveScale • (incidenceGraph φ).drawingPosition d (List.idxOf v φ.distinctVars) + positiveTranslation

A used source variable resolves to its common original scaled vertex.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_of_mem (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (hnd : (List.map Prod.fst (positivePositionTable φ d)).Nodup) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p : Orthogonal.Point} (hm : (v, p) ∈ positivePositionTable φ d) : positiveVariablePoint φ d v = p

Any uniquely indexed position-table entry resolves to its prescribed actual point.

theorem Cslib.Complexity.SAT.ExactOne.positivePlacedClauses_formula (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : List.map Prod.fst (positivePlacedClauses φ d) = Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ

Geometric clause records retain the actual formula, variable names, and clause order.