Native polynomial-time positive incidence drawing compilation

Coordinates and original source labels use binary encodings. Clause, literal, and list indices use unary counters bounded by the emitted lists. The finite profile and collar choices are fixed independently of the input; there is no enumeration of the coordinate rectangle.

The input, a source formula with its supplied binary-coordinate drawing, is encoded by DrawingFinitePolyTime.encInput.

Main results

Native certificates for source route normalization, constant-scale trimming, and the actual positive drawing compiler.

References

These are original native certificates for the explicit drawing construction.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.DrawingNative.encSourceIndex : (Graph × Graph.OrthogonalDrawing) × ℕ ↪ List Bool

Listed graphs retain binary vertex labels; edge positions use unary counters.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.instListEncodingPointEncPointEncRoute : Turing.MultiTapeTM.ListEncoding Orthogonal.encPoint Orthogonal.encRoute

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.instSizedListEncodingPointEncPointEncRoute : Turing.MultiTapeTM.SizedListEncoding Orthogonal.encPoint Orthogonal.encRoute

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.drawingPosition : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × Graph.OrthogonalDrawing) × ℕ) => p.1.1.drawingPosition p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph Graph.encOrthogonalDrawing) Turing.MultiTapeTM.encNat) Orthogonal.encPoint

Position lookup compares binary graph labels and scans only the declared vertex list.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.sourceStart : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × Graph.OrthogonalDrawing) × ℕ) => ExactOne.sourceStart p.1.1 p.1.2 p.2) encSourceIndex Orthogonal.encPoint

The clause endpoint of an indexed source edge is computed without expanding labels.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.sourceRoute : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × Graph.OrthogonalDrawing) × ℕ) => ExactOne.sourceRoute p.1.1 p.1.2 p.2) encSourceIndex Orthogonal.encRoute

Reading and, when necessary, reversing an actual source route is polynomial-time.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.sourceDirection : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × Graph.OrthogonalDrawing) × ℕ) => ExactOne.sourceDirection p.1.1 p.1.2 p.2) encSourceIndex Orthogonal.encPoint

The source exit direction needs only the first two listed route points.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.cutStart (k radius : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (Orthogonal.cutStart k radius) Orthogonal.encRoute Orthogonal.encRoute

Constant-scale endpoint trimming scans the supplied route and computes two point images.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.exteriorRoute (k radius : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × Graph.OrthogonalDrawing) × ℕ) => ExactOne.exteriorRoute k radius p.1.1 p.1.2 p.2) encSourceIndex Orthogonal.encRoute

The trimmed exterior of each indexed source edge is polynomial-time.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.sourceEdgeIndex : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × ℕ × ℕ) => ExactOne.sourceEdgeIndex p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair encCNF (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encUnary

Clause and literal indices of a source occurrence are unary; original labels stay binary.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.literalSide (j : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) × ℕ) => ExactOne.literalSide p.1.1 p.1.2 p.2 j) (Turing.MultiTapeTM.encPair DrawingFinitePolyTime.encInput Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encFinite (Fin 4))

Each actual source exit has a native finite cardinal-direction tag.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.clausePorts : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) × ℕ) => ExactOne.clausePorts p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair DrawingFinitePolyTime.encInput Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encFinite PortAssignment)

Complete the present exits to one of the fixed ordered collars in native polynomial time.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.positiveBoxOrigin : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) × ℕ) => ExactOne.positiveBoxOrigin p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair DrawingFinitePolyTime.encInput Turing.MultiTapeTM.encUnary) Orthogonal.encPoint

The lower-left box origin uses the source's actual clause position and a constant dilation.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.positiveExterior (j : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) × ℕ) => ExactOne.positiveExterior p.1.1 p.1.2 p.2 j) (Turing.MultiTapeTM.encPair DrawingFinitePolyTime.encInput Turing.MultiTapeTM.encUnary) Orthogonal.encRoute

The actual dilated and trimmed inherited route is emitted without searching the plane.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.signedOffset : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × ℕ) => Logic.PL.CNF.PositiveExactOneCompile.signedOffset p.1 p.2) (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary

Prefix offsets are computed as lengths of the already certified signed clause compiler.

theorem Cslib.Complexity.SAT.ExactOne.DrawingNative.computableInPolyTime_positiveDrawing : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) => positiveDrawing p.1 p.2) DrawingFinitePolyTime.encInput Graph.encOrthogonalDrawing

The actual emitted drawing is natively polynomial-time on binary coordinates and labels. The proof scans the explicit lists and dispatches among fixed local templates.