Continuous local and exterior routes of the positive drawing compiler

Local prefixes lie in their closed clause boxes. Their inherited exterior routes touch those boxes at the prescribed source ports only. These full-real-support facts justify the actual route concatenations, including shared source variables and parallel source incidences.

Main definitions

• positiveStem: the translated local part of an actual emitted incidence.

Main results

• positiveStem_in_box, positiveExterior_box_contact: clause-box support isolation.
• positiveIncidenceRoute_regular: proper orthogonality and continuous simplicity of actual routes.
• positiveIncidenceRoute_join_endpoints: exact endpoint identity for additive route costs.
• positiveStem_contacts: finite local prefixes meet only at their actual shared endpoints.

References

These finite drawing-composition and continuous-support proofs are original.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_incidence_points_bounds {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) (q : Orthogonal.Point) : q ∈ e.route → 0 ≤ q.1 ∧ q.1 ≤ 540000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 540000

All listed points of an actual collared local incidence lie in the common clause square.

theorem Cslib.Complexity.SAT.ExactOne.inPointBox_translate_iff (c v : Orthogonal.Point) (radius : ℕ) (p : ℝ × ℝ) : Orthogonal.inPointBox (c + v) radius (p + Orthogonal.realPoint v) ↔ Orthogonal.inPointBox c radius p

A common translation preserves membership in a closed local square.

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

The translated local prefix used by an actual output incidence.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_in_box {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (positiveStem φ d i e)) : Orthogonal.inPointBox (positiveBoxOrigin φ d i + positiveTranslation) positiveRadius p

Every real point of a local prefix lies in its source clause's closed replacement box.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_regular {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) : Orthogonal.IsOrthogonal (positiveExterior φ d i j) ∧ Orthogonal.IsSimple (positiveExterior φ d i j)

The normalized inherited route remains properly orthogonal and continuously simple.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_box_contact {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (j : Fin 3) (hj : ↑j < List.length φ[i]) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (positiveExterior φ d i ↑j)) (hb : Orthogonal.inPointBox (positiveBoxOrigin φ d i + positiveTranslation) positiveRadius p) : p = Orthogonal.realPoint (positiveBoxOrigin φ d i + collarOuterPort ((clausePorts φ d i).side j))

The actual translated exterior route meets its own closed clause box only at the selected local collar port.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_incidence_endpoints (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) : e.clauseIndex < (collaredPrefixGeometry (profilePrefixGeometry p) s).clausePositions.length ∧ e.variableIndex < (collaredPrefixGeometry (profilePrefixGeometry p) s).variablePositions.length ∧ List.head? e.route = some ((collaredPrefixGeometry (profilePrefixGeometry p) s).clausePosition e.clauseIndex) ∧ List.getLast? e.route = some ((collaredPrefixGeometry (profilePrefixGeometry p) s).variablePosition e.variableIndex)

A collared local incidence retains its clause endpoint and ends at its moved variable. The indices remain valid in the actual collared tables.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_regular {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) (h : (profilePrefixGeometry (clauseProfile c)).PrefixCheck) {e : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) : Orthogonal.IsOrthogonal (positiveStem φ d i e) ∧ Orthogonal.IsSimple (positiveStem φ d i e) ∧ List.head? (positiveStem φ d i e) = some (positiveBoxOrigin φ d i + (clauseGeometry φ d i c).clausePosition e.clauseIndex) ∧ List.getLast? (positiveStem φ d i e) = some (positiveBoxOrigin φ d i + (clauseGeometry φ d i c).variablePosition e.variableIndex)

The actual translated local incidence is proper and simple, with its prescribed endpoints.

theorem Cslib.Complexity.SAT.ExactOne.profile_source_lookup (p : ClauseProfile) {v j : ℕ} (hv : v < (profilePrefixGeometry p).variablePositions.length) (hget : (profileVariables p).getD v (Sum.inl (Sum.inl 0)) = Sum.inl (Sum.inl j)) : j < List.length (profileSource p) ∧ j < 3 ∧ v = List.idxOf (Sum.inl (Sum.inl j)) (profileVariables p) ∧ v ∈ (profilePrefixGeometry p).terminalVariables ∧ ↑(terminalIndex (profilePrefixGeometry p) v) = j

A local source-placeholder lookup identifies its unique terminal slot, including the actual unmodded source position.

theorem Cslib.Complexity.SAT.ExactOne.positiveIncidenceRoute_regular {φ : 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) : Orthogonal.IsOrthogonal (positiveIncidenceRoute φ d i φ[i] e) ∧ Orthogonal.IsSimple (positiveIncidenceRoute φ d i φ[i] e)

Every actual emitted incidence is properly orthogonal and continuously simple. Source placeholders are spliced at the sole contact of their clause box with the inherited route; auxiliary incidences retain their finite prefix.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_routes_contact (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e f : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (hf : f ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (hne : e ≠ f) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support e.route) (hw : z ∈ Orthogonal.support f.route) : ∃ q ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).commonEndpoints e f, z = Orthogonal.realPoint q

Collaring preserves exactly the allowed local clause and auxiliary endpoint contacts. Distinct incidences never share one of the removed source placeholders.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_contacts {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) (h : (profilePrefixGeometry (clauseProfile c)).PrefixCheck) {e f : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) (hf : f ∈ (clauseGeometry φ d i c).incidenceRoutes) (hne : e ≠ f) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support (positiveStem φ d i e)) (hw : z ∈ Orthogonal.support (positiveStem φ d i f)) : ∃ q ∈ (clauseGeometry φ d i c).commonEndpoints e f, z = Orthogonal.realPoint (positiveBoxOrigin φ d i + q)

Different local prefixes in one clause box meet only at their common actual endpoints.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_variable_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (v : Fin (profilePrefixGeometry p).variablePositions.length) (hv : ↑v ≠ e.variableIndex) : Orthogonal.realPoint ((collaredPrefixGeometry (profilePrefixGeometry p) s).variablePosition ↑v) ∉ Orthogonal.support e.route

Actual collared routes avoid every other local variable, including exposed source ports.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_clause_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (j : Fin (profilePrefixGeometry p).clausePositions.length) (hj : ↑j ≠ e.clauseIndex) : Orthogonal.realPoint ((collaredPrefixGeometry (profilePrefixGeometry p) s).clausePosition ↑j) ∉ Orthogonal.support e.route

Actual collared routes avoid every other local clause vertex.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_other_terminal_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e f : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (hf : f ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) (hne : e ≠ f) (ht : f.variableIndex ∈ (profilePrefixGeometry p).terminalVariables) : Orthogonal.realPoint ((collaredPrefixGeometry (profilePrefixGeometry p) s).variablePosition f.variableIndex) ∉ Orthogonal.support e.route

Distinct local incidences cannot contact the source port of one another.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_other_terminal_not_mem_support {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) (h : (profilePrefixGeometry (clauseProfile c)).PrefixCheck) {e f : LocalIncidence} (he : e ∈ (clauseGeometry φ d i c).incidenceRoutes) (hf : f ∈ (clauseGeometry φ d i c).incidenceRoutes) (hne : e ≠ f) (ht : f.variableIndex ∈ (profilePrefixGeometry (clauseProfile c)).terminalVariables) : Orthogonal.realPoint (positiveBoxOrigin φ d i + (clauseGeometry φ d i c).variablePosition f.variableIndex) ∉ Orthogonal.support (positiveStem φ d i e)

A translated local incidence avoids the exposed endpoint of every other incidence.

theorem Cslib.Complexity.SAT.ExactOne.positiveStem_other_exterior_disjoint {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (h : (profilePrefixGeometry (clauseProfile φ[i])).PrefixCheck) {e f : LocalIncidence} (he : e ∈ (clauseGeometry φ d i φ[i]).incidenceRoutes) (hf : f ∈ (clauseGeometry φ d i φ[i]).incidenceRoutes) (hne : e ≠ f) {j : ℕ} (hget : (profileVariables (clauseProfile φ[i])).getD f.variableIndex (Sum.inl (Sum.inl 0)) = Sum.inl (Sum.inl j)) : Disjoint (Orthogonal.support (positiveStem φ d i e)) (Orthogonal.support (positiveExterior φ d i j))

Inside one clause box, an inherited exterior is disjoint from every other local prefix. The shared clause center has already been cut away.

theorem Cslib.Complexity.SAT.ExactOne.positiveIncidenceRoute_join_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) {j : ℕ} (hget : (profileVariables (clauseProfile φ[i])).getD e.variableIndex (Sum.inl (Sum.inl 0)) = Sum.inl (Sum.inl j)) : ∃ (q : Orthogonal.Point), List.getLast? (positiveStem φ d i e) = some q ∧ List.head? (positiveExterior φ d i j) = some q

A source incidence's finite stem and inherited exterior have the same actual integer endpoint. This identity also supports exact wire-length and segment-count bookkeeping.