Exactly one true literal, clause by clause

DescriptiveComplexity.OneInProper asks every clause to have exactly one true literal. A reduction into 1-in-SAT knows the literals of each clause it builds: a short explicit list of distinct elements with their signs. The lemmas here turn “exactly one true literal of this clause” (DescriptiveComplexity.SatOcc.OneInAt) into the propositional statement about the truth values of those literals, for clauses of zero to four literals, so that a correctness proof is left with propositional reasoning only.