Uniquely indexed actual variable positions

The finite position table contains each shared source variable once and each private auxiliary in exactly one clause box. The private signed-clause intervals use the actual compiler's prefix offsets. Thus table lookup returns the intended position without any auxiliary-name collision.

Main results

• positivePositionTable_keys_nodup: every actual variable has a unique table key.
• positiveVariablePoint_auxiliary: actual auxiliary positions resolve to their local boxes.

References

These support and index arguments are original.

def Cslib.Complexity.SAT.ExactOne.isAuxiliaryVariable : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ → Bool

Whether a structured variable is private to a clause box.

theorem Cslib.Complexity.SAT.ExactOne.isAuxiliaryVariable_iff (v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ) : isAuxiliaryVariable v = true ↔ ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)

The auxiliary role excludes all inherited source-variable names.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryBlock_keys (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : List.map Prod.fst (positiveAuxiliaryBlock φ d i c) = List.map (profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c) (List.filter isAuxiliaryVariable (profileVariables (clauseProfile c)))

The actual fresh-position table lists exactly the mapped private profile variables.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryBlock_keys_nodup (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {i : ℕ} (hi : i < List.length φ) : (List.map Prod.fst (positiveAuxiliaryBlock φ d i φ[i])).Nodup

A single actual clause block never repeats a fresh-variable key.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryBlock_keys_disjoint (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hij : i ≠ j) : (List.map Prod.fst (positiveAuxiliaryBlock φ d i φ[i])).Disjoint (List.map Prod.fst (positiveAuxiliaryBlock φ d j φ[j]))

Different original clause boxes have disjoint fresh-variable key lists.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryPositions_keys_nodup (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (List.map Prod.fst (positiveAuxiliaryPositions φ d)).Nodup

The global fresh-variable position table has no repeated key.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryPositions_ne_source (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ List.map Prod.fst (positiveAuxiliaryPositions φ d)) (n : ℕ) : v ≠ Sum.inl (Sum.inl n)

No fresh position-table key can be an inherited source-variable name.

theorem Cslib.Complexity.SAT.ExactOne.positivePositionTable_keys_nodup (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (List.map Prod.fst (positivePositionTable φ d)).Nodup

Every actual variable position has a unique finite-table key.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_auxiliary (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p : Orthogonal.Point} (hm : (v, p) ∈ positiveAuxiliaryPositions φ d) : positiveVariablePoint φ d v = p

An actual auxiliary entry resolves to its own displayed clause-box point.

theorem Cslib.Complexity.SAT.ExactOne.rawVariable_profile (φ : Logic.PL.CNF ℕ) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).vars) : ∃ (c : Logic.PL.Clause ℕ) (i : ℕ), (c, i) ∈ List.zipIdx φ ∧ ∃ w ∈ profileVariables (clauseProfile c), profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c w = v

Every actual output variable belongs to a source-clause profile with the exact global name.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryBlock_entry (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hw : w ∈ profileVariables (clauseProfile c)) (ha : ∀ (n : ℕ), w ≠ Sum.inl (Sum.inl n)) : ∃ (p : Orthogonal.Point), (profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c w, p) ∈ positiveAuxiliaryBlock φ d i c

Every private profile variable contributes its prescribed fresh-position entry.

theorem Cslib.Complexity.SAT.ExactOne.positivePositionTable_covers (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).vars) : ∃ (p : Orthogonal.Point), (v, p) ∈ positivePositionTable φ d

Every occurring actual output variable has a finite position-table entry.

theorem Cslib.Complexity.SAT.ExactOne.positiveAuxiliaryPositions_origin (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {p : Orthogonal.Point} (hp : (v, p) ∈ positiveAuxiliaryPositions φ d) : ∃ (c : Logic.PL.Clause ℕ) (i : ℕ), (c, i) ∈ List.zipIdx φ ∧ ∃ w ∈ profileVariables (clauseProfile c), (∀ (n : ℕ), w ≠ Sum.inl (Sum.inl n)) ∧ v = profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c w ∧ p = positiveBoxOrigin φ d i + (clauseGeometry φ d i c).variablePosition (List.idxOf w (profileVariables (clauseProfile c)))

Every fresh-position record has an actual original-clause owner and a unique local profile index. Private source placeholders are excluded from these records.