Actual vertex geometry inside clause boxes

Private variables and clauses receive the common injective affine placement of their inner profile. Source placeholders instead occupy outer boundary ports and are omitted from the actual global vertex list.

Main results

• profileVariableIndex_lt, profileAuxiliaryIndex_not_terminal: actual local index scopes.
• clauseGeometry_auxiliary_point: affine placement of every private variable.
• prefix_variablePoint_injective, prefix_clausePoint_injective, prefix_variablePoint_ne_clausePoint: distinct inner vertices remain distinct.

References

These finite support and geometric indexing arguments are original.

theorem Cslib.Complexity.SAT.ExactOne.profileVariableIndex_lt (p : ClauseProfile) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables p) : List.idxOf v (profileVariables p) < (profilePrefixGeometry p).variablePositions.length

The logical first-occurrence index is a valid geometric variable index.

theorem Cslib.Complexity.SAT.ExactOne.profileAuxiliaryIndex_not_terminal (p : ClauseProfile) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables p) (ha : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) : List.idxOf v (profileVariables p) ∉ (profilePrefixGeometry p).terminalVariables

A private logical variable cannot be one of the exposed source placeholders.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_auxiliary_point (φ : 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)) : (clauseGeometry φ d i c).variablePosition (List.idxOf v (profileVariables (clauseProfile c))) = collarPoint (collarReflected (clausePorts φ d i)) ((profilePrefixGeometry (clauseProfile c)).variablePosition (List.idxOf v (profileVariables (clauseProfile c))))

Private variables receive the common affine placement of their actual inner points.

theorem Cslib.Complexity.SAT.ExactOne.prefix_variablePoint_injective {g : LocalGeometry} (h : g.PrefixCheck) {i j : ℕ} (hi : i < g.variablePositions.length) (hj : j < g.variablePositions.length) (he : g.variablePosition i = g.variablePosition j) : i = j

The coordinate lookup of an actual inner variable is injective.

theorem Cslib.Complexity.SAT.ExactOne.prefix_clausePoint_injective {g : LocalGeometry} (h : g.PrefixCheck) {i j : ℕ} (hi : i < g.clausePositions.length) (hj : j < g.clausePositions.length) (he : g.clausePosition i = g.clausePosition j) : i = j

The coordinate lookup of an actual inner clause is injective.

theorem Cslib.Complexity.SAT.ExactOne.prefix_variablePoint_ne_clausePoint {g : LocalGeometry} (h : g.PrefixCheck) {i j : ℕ} (hi : i < g.variablePositions.length) (hj : j < g.clausePositions.length) : g.variablePosition i ≠ g.clausePosition j

An actual inner variable and clause cannot occupy the same point.