Unique ownership of local drawing auxiliaries

The original-clause index distinguishes signed auxiliaries; disjoint signed-clause prefix intervals distinguish positive auxiliaries. Source placeholders may coincide when source variables are repeated, and are deliberately excluded from these injectivity statements.

Main results

• profileVariableMap_aux_injective: an actual auxiliary identifies its unique source block and local profile variable.
• profileVariableMap_aux_ne_source: private auxiliary names cannot be source names.

References

These are original support and prefix-index arguments for the actual drawing compiler.

theorem Cslib.Complexity.SAT.ExactOne.profile_signed_length (i : ℕ) (c : Logic.PL.Clause ℕ) : List.length (Logic.PL.CNF.FromSAT.clause 0 (profileSource (clauseProfile c))) = List.length (Logic.PL.CNF.FromSAT.clause i c)

Signed block length depends on the clause length, independently of source variable names and polarities. The selected profile has exactly the actual signed block length.

theorem Cslib.Complexity.SAT.ExactOne.profileVariableMap_aux_ne_source {i offset : ℕ} {c : Logic.PL.Clause ℕ} {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) (n : ℕ) : profileVariableMap i offset c v ≠ Sum.inl (Sum.inl n)

A private auxiliary never becomes an inherited source-variable name.

theorem Cslib.Complexity.SAT.ExactOne.profileVariableMap_aux_injective (φ : Logic.PL.CNF ℕ) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) {v w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables (clauseProfile φ[i])) (hw : w ∈ profileVariables (clauseProfile φ[j])) (hvs : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) (hws : ∀ (n : ℕ), w ≠ Sum.inl (Sum.inl n)) (he : profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) φ[i] v = profileVariableMap j (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ j) φ[j] w) : i = j ∧ v = w

The actual global name of an auxiliary determines its source block and its local profile name. Source placeholders, whose variables can coincide, are excluded explicitly.