Actual variable names of local positive exact-one profiles

The finite geometric profiles use source literal positions as placeholder variable names. Relabelling restores source labels, original clause indices, and the exact signed-clause prefix offsets of the positive compiler. Repeated source variables may identify distinct placeholders; their displayed vertices are omitted when the local incidences are spliced to source routes.

Main definitions

• clauseProfile: select the finite profile from source length and polarities.
• profileVariableMap: restore actual labels and both families of auxiliary indices.

Main results

• profileFormula_relabel: the relabelled profile is the actual positive output block.
• rawFormula_eq_profiles: the profile list has exactly the actual compiler's clause order.

References

These are original indexing identities for the existing parsimonious compiler.

def Cslib.Complexity.SAT.ExactOne.clauseProfile : Logic.PL.Clause ℕ → ClauseProfile

Select one of the fifteen profiles from the first three source literal polarities.

def Cslib.Complexity.SAT.ExactOne.profileVariableMap (i offset : ℕ) (c : Logic.PL.Clause ℕ) : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ → Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ

Restore actual source labels, the original clause index, and the global signed-clause offset. The source-slot fallback is irrelevant to every occurring profile variable.

theorem Cslib.Complexity.SAT.ExactOne.profileFormula_relabel (i offset : ℕ) (c : Logic.PL.Clause ℕ) : Logic.PL.CNF.relabel (profileVariableMap i offset c) (profileFormula (clauseProfile c)) = Logic.PL.CNF.relabel (Logic.PL.CNF.PositiveExactOne.shift offset) (Logic.PL.CNF.PositiveExactOne.formula (Logic.PL.CNF.FromSAT.clause i c))

A finite profile has exactly the actual compiler's literals after restoring all indices.

theorem Cslib.Complexity.SAT.ExactOne.rawFormula_eq_profiles (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ = List.flatMap (fun (c : Logic.PL.Clause ℕ × ℕ) => Logic.PL.CNF.relabel (profileVariableMap c.2 (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ c.2) c.1) (profileFormula (clauseProfile c.1))) (List.zipIdx φ)

The profile partition retains the actual output formula, clause order, and variable names.

theorem Cslib.Complexity.SAT.ExactOne.profileFormula_length_le (p : ClauseProfile) : List.length (profileFormula p) ≤ 22

Every actual positive replacement profile has at most twenty-two clauses.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_incidence_count (p : ClauseProfile) (i : Fin 22) : (List.filter (fun (e : LocalIncidence) => e.clauseIndex == ↑i) (profileGeometry p).incidenceRoutes).length = List.length (List.getD (profileFormula p) ↑i [])

The local incidence table has one route per literal, in each actual profile clause.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_literal_indices (p : ClauseProfile) (i : Fin 22) {l : Logic.PL.Literal (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} {e : LocalIncidence} (he : (l, e) ∈ List.zip (List.getD (profileFormula p) ↑i []) (List.filter (fun (e : LocalIncidence) => e.clauseIndex == ↑i) (profileGeometry p).incidenceRoutes)) : e.variableIndex = List.idxOf l.1 (profileVariables p)

Filtering the incidence table by clause retains the actual local literal order and names.

theorem Cslib.Complexity.SAT.ExactOne.profileVariables_scope (p : ClauseProfile) (v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ) : v ∈ profileVariables p → match v with | Sum.inl (Sum.inl j) => j < List.length (profileSource p) | Sum.inl (Sum.inr (i, snd)) => i = 0 | Sum.inr ((i, snd), snd_1) => i < List.length (Logic.PL.CNF.FromSAT.clause 0 (profileSource p))

Every profile variable has exactly its indicated source, original-clause, or signed-clause scope. These finite bounds identify the private auxiliary intervals used by global assembly.

theorem Cslib.Complexity.SAT.ExactOne.profileSource_terminal_index (p : ClauseProfile) (j : Fin 3) (hj : ↑j < List.length (profileSource p)) : have v := List.idxOf (Sum.inl (Sum.inl ↑j)) (profileVariables p); v < (profileGeometry p).variablePositions.length ∧ v ∈ (profileGeometry p).terminalVariables ∧ List.idxOf v (profileGeometry p).terminalVariables = ↑j

Every present source placeholder has a valid local variable index and its prescribed position in the ordered terminal list.

theorem Cslib.Complexity.SAT.ExactOne.profileSource_length (c : Logic.PL.Clause ℕ) (hc : List.length c ≤ 3) : List.length (profileSource (clauseProfile c)) = List.length c

Selecting a profile preserves the source width when the source has width at most three.

theorem Cslib.Complexity.SAT.ExactOne.profileSource_length_le (c : Logic.PL.Clause ℕ) : List.length (profileSource (clauseProfile c)) ≤ List.length c

Profiles retain at most the first three original positions.