Polynomial-time finite dispatch in the positive exact-one drawing compiler

The local profiles and ordered port assignments range over fixed finite types. Native finite case analysis certifies their variable, clause, and route tables under binary coordinates. Dynamic clause/literal indices remain unary counters. Source-role classification is a lookup in a fixed finite option table, avoiding recursion through the structured raw variable type.

Main definitions

• encLocalIncidence: unary local clause/variable indices and binary-coordinate routes.
• profileRole, profileRoleTable: finite source-slot or internal-variable classification.

Main results

• computableInPolyTime_clauseProfile, computableInPolyTime_directionSide.
• computableInPolyTime_variablePositions, computableInPolyTime_incidenceRoutes.
• computableInPolyTime_profileRole: polynomial lookup with an unbounded unary index.
• computableInPolyTime_clausePorts_of_literalSide: compose dynamic source exit computation with the fixed finite collar completion.

References

These are original computational certificates for the fixed drawing tables.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.encClause : Logic.PL.Clause ℕ ↪ List Bool

The existing literal encoding, with binary natural variable labels.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.encInput : Logic.PL.CNF ℕ × Graph.OrthogonalDrawing ↪ List Bool

Native encoding of an input formula and its supplied binary-coordinate drawing.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.encLocalIncidence : LocalIncidence ↪ List Bool

Unary local incidence indices and a binary-coordinate route.

@[reducible, inline]

noncomputable abbrev Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.encProfilePorts : ClauseProfile × PortAssignment ↪ List Bool

Encodings of the two fixed finite dispatch tags.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.encRawVariable : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ ↪ List Bool

Structured logical variables retain the source's binary natural encoding.

def Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.boundedClauseLength (c : Logic.PL.Clause ℕ) : Fin 4

Inspect at most three list constructors to obtain the clause's bounded length tag.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.boundedClauseLength_eq (c : Logic.PL.Clause ℕ) : boundedClauseLength c = ⟨min (List.length c) 3, ⋯⟩

The bounded length tag is exactly the first three source positions' presence count.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_boundedClauseLength : Turing.MultiTapeTM.ComputableInPolyTime boundedClauseLength encClause (Turing.MultiTapeTM.encFinite (Fin 4))

Native computation of the bounded presence tag examines three list heads.

def Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.clauseTag (c : Logic.PL.Clause ℕ) : Fin 4 × Bool × Bool × Bool

The finite tag consisting of the bounded length and first three polarities.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_clauseProfile : Turing.MultiTapeTM.ComputableInPolyTime clauseProfile encClause (Turing.MultiTapeTM.encFinite ClauseProfile)

Selecting the actual polarity profile is native polynomial-time.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_directionSide : Turing.MultiTapeTM.ComputableInPolyTime directionSide Orthogonal.encPoint (Turing.MultiTapeTM.encFinite (Fin 4))

A cardinal-vector classifier uses only three binary-coordinate equality tests.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_choosePorts : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Fin 4 × Fin 4 × Fin 4 × Fin 4) => choosePorts p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite (Fin 4)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite (Fin 4)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite (Fin 4)) (Turing.MultiTapeTM.encFinite (Fin 4))))) (Turing.MultiTapeTM.encFinite PortAssignment)

Completing a partial source exit assignment is a fixed finite function.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_variablePositions : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ClauseProfile × PortAssignment) => (collaredPrefixGeometry (profilePrefixGeometry p.1) p.2).variablePositions) encProfilePorts Orthogonal.encRoute

A fixed profile/port pair computes its placed local variable-position list.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_clausePositions : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ClauseProfile × PortAssignment) => (collaredPrefixGeometry (profilePrefixGeometry p.1) p.2).clausePositions) encProfilePorts Orthogonal.encRoute

A fixed profile/port pair computes its placed local clause-position list.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_incidenceRoutes : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ClauseProfile × PortAssignment) => (collaredPrefixGeometry (profilePrefixGeometry p.1) p.2).incidenceRoutes) encProfilePorts (Turing.MultiTapeTM.encList encLocalIncidence)

A fixed profile/port pair computes its actual local incidence routes and indices.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_profileVariables : Turing.MultiTapeTM.ComputableInPolyTime profileVariables (Turing.MultiTapeTM.encFinite ClauseProfile) (Turing.MultiTapeTM.encList encRawVariable)

The source-variable list of a profile is a fixed finite lookup.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_profileFormula : Turing.MultiTapeTM.ComputableInPolyTime profileFormula (Turing.MultiTapeTM.encFinite ClauseProfile) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encRawVariable Turing.MultiTapeTM.encBool)))

The exact logical formula of a profile is a fixed finite lookup.

def Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.variableRole (v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ) : Option (Fin 3)

Classify a fixed profile variable, normalizing its source position to the three finite slots.

def Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.profileRole (p : ClauseProfile) (n : ℕ) : Option (Fin 3)

Source slot or internal-variable role of an indexed profile variable. Invalid indices follow the actual drawing compiler's default source slot zero.

def Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.profileRoleTable (p : ClauseProfile) : List (Option (Fin 3))

A fixed finite table of source-slot roles for the variables of each profile.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.profileRole_eq_getD (p : ClauseProfile) (n : ℕ) : profileRole p n = (profileRoleTable p).getD n (some 0)

The native role lookup agrees with the actual raw-variable classifier.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.profileVariables_source_bound (p : ClauseProfile) (v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ) : v ∈ profileVariables p → match v with | Sum.inl (Sum.inl j) => j < 3 | x => True

Every source-placeholder name occurring in a fixed profile is one of its three slots.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.profileRole_map_val (p : ClauseProfile) (n : ℕ) : Option.map Fin.val (profileRole p n) = match (profileVariables p).getD n (Sum.inl (Sum.inl 0)) with | Sum.inl (Sum.inl j) => some j | x => none

The finite role tag recovers the exact natural source index used by the drawing compiler.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_profileRoleTable : Turing.MultiTapeTM.ComputableInPolyTime profileRoleTable (Turing.MultiTapeTM.encFinite ClauseProfile) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encFinite (Option (Fin 3))))

The finite role table can be emitted in native polynomial time.

theorem Cslib.Complexity.SAT.ExactOne.DrawingFinitePolyTime.computableInPolyTime_profileRole : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ClauseProfile × ℕ) => profileRole p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite ClauseProfile) Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encFinite (Option (Fin 3)))

A role table lookup accepts any unary index, with no promise that it lies in the table.

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

Native computation of the selected collar follows from the three native source exits. The dynamic geometric computation is supplied by the caller, independently of finite dispatch.