Assignment
plain-language theorem explainer
Assignment n is the type of all maps from n indices to Boolean values, serving as the evaluation domain for clauses and J-cost in the R̂ SAT encoding. Researchers analyzing recognition-time bounds for SAT cite it when separating R̂ polytime certification from circuit evaluation. The definition is a direct type abbreviation that immediately enables the satisfiedBy predicates and isSAT/isUNSAT propositions.
Claim. An assignment for $n$ variables is any function $a : {0,1,…,n-1} → {true,false}$.
background
The RSAT encoding module models SAT via J-cost on assignments, where zero J-cost signals a satisfying assignment and positive J-cost counts unsatisfied clauses. This sits inside the Recognition Science claim that R̂ supplies a non-natural polytime certifier: satisfiable k-CNF instances reach zero cost in O(n) steps while unsatisfiable instances carry a topological obstruction (positive Betti-1). The module imports the CNF layer, where Assignment was previously an abbreviation Var n → Bool; the present definition switches to Fin n → Bool for direct indexing into literals.
proof idea
One-line definition that sets Assignment n to the function type Fin n → Bool. No lemmas or tactics are invoked; the declaration simply introduces the type used by all downstream satisfaction and cost functions.
why it matters
The definition supplies the domain for CircuitLedger structures including BooleanCircuitWithEval, CircuitDecides, CircuitLedgerCert and CircuitSeparation. These establish that R̂ decides SAT in ≤ n recognition steps while any deciding circuit must read all n inputs. It anchors the module's core claim that recognition-time complexity separates from Turing time, linking to the T0-T8 forcing chain and the Recognition Composition Law. The declaration touches the open natural-proof-barrier hypothesis listed in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.