Lit
plain-language theorem explainer
Literals over n variables are defined inductively as either a positive or negative occurrence of a variable index from Fin n. Researchers encoding SAT instances or proving properties of partial assignments in the Recognition Science complexity layer cite this definition when building CNF formulas. The construction is a direct inductive type with two constructors that derives decidable equality and representation.
Claim. A literal over $n$ variables is either a positive occurrence of a variable index $v$ from the finite set Fin $n$ or the negative occurrence of the same index.
background
Variable indices are taken from the finite set Fin n for a problem of fixed size n. The literal type is built directly on this indexing to represent positive and negative occurrences. The module sets the local convention that all SAT objects are parameterized by this n.
proof idea
The declaration is the inductive definition itself, introducing the two constructors pos and neg with no further lemmas or tactics applied.
why it matters
It supplies the basic data type for clauses as lists of literals and for evaluation functions such as evalLit. Downstream uses include valueOfLit in partial-assignment backpropagation and mentionsVarLit in the PC module. The definition supports the SAT encoding layer that sits inside the broader Recognition Science monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.