Certificates for the actual positive exact-one replacement profiles

Each finite profile is checked against its full positive exact-one formula, rather than an unrelated graph. Every source placeholder has just one internal incidence, so it can be removed when that incidence is joined to the source drawing. Full continuous certificates for the actual extended incidence routes are in GeometryProfilesPrefix.

Main results

The continuous source-boundary certificates are in GeometryProfilesPrefix.

• profileGeometry_signature: incidence routes match the actual composed positive compiler.
• profileGeometry_terminals: exposed variables are exactly the source placeholders.

References

The logical gadgets are from [HuntMaratheRadhakrishnanStearns1998, Theorem 3.8]. The composed geometric certificates are original.

def Cslib.Complexity.SAT.ExactOne.profileSignature (p : ClauseProfile) : List (ℕ × ℕ)

The exact clause-variable incidence sequence of the positive compiled formula.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_variable_length (p : ClauseProfile) : (profileGeometry p).variablePositions.length = (profileVariables p).length

Geometry and logical variable lists have exactly corresponding positions.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_clause_length (p : ClauseProfile) : (profileGeometry p).clausePositions.length = List.length (profileFormula p)

There is one clause position for each actual emitted positive clause.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_signature (p : ClauseProfile) : List.map (fun (e : LocalIncidence) => (e.1, e.2.1)) (profileGeometry p).incidenceRoutes = profileSignature p

Every incidence appears once, in actual output-clause and literal-position order.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_terminals (p : ClauseProfile) : List.map (fun (v : ℕ) => (profileVariables p).getD v (Sum.inl (Sum.inl 0))) (profileGeometry p).terminalVariables = List.map (fun (v : ℕ) => Sum.inl (Sum.inl v)) (List.range (List.length (profileSource p)))

Exposed variables are precisely the source slots, in source literal order.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_terminal_degree (p : ClauseProfile) (v : ℕ) : v ∈ (profileGeometry p).terminalVariables → List.count v (List.map (fun (e : LocalIncidence) => e.2.1) (profileGeometry p).incidenceRoutes) = 1

Each source placeholder has a single internal incidence, ready for exterior splicing.

theorem Cslib.Complexity.SAT.ExactOne.profileGeometry_costs (p : ClauseProfile) : (profileGeometry p).clausePositions.length ≤ 22 ∧ (profileGeometry p).incidenceRoutes.length ≤ 66 ∧ (profileGeometry p).size = 180000

The actual composed gadgets have at most twenty-two clauses and sixty-six incidences.