Assignment
plain-language theorem explainer
An assignment for n variables is a map from the first n naturals to Boolean values. Researchers formalizing the Recognition Science SAT encoding cite this when defining the domain for clause evaluation and J-cost. The definition is introduced as a direct type abbreviation with no additional structure or lemmas.
Claim. For each natural number $n$, an assignment is a function from the finite set of size $n$ to the two-element set of truth values.
background
The module develops the R̂ SAT encoding inside Recognition Science. It encodes CNF formulas so that the recognition operator reaches zero J-cost in O(n) steps on satisfiable instances while unsatisfiable instances carry a non-contractible topological obstruction. The supplied module documentation states that this separates recognition-time complexity from Turing computation time and does not prove P ≠ NP for Turing machines.
proof idea
Direct type abbreviation equating the name with the function type Fin n → Bool. No lemmas or tactics are invoked.
why it matters
The definition supplies the domain type used throughout the CircuitLedger module in BooleanCircuitWithEval, CircuitDecides, CircuitLedgerCert and CircuitSeparation. Those results establish the O(n) recognition bound for SAT formulas and the defect moat for UNSAT formulas. It completes the SATLedger encoding component listed in the module documentation and supports the claimed distinction between recognition steps and circuit input reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.