Fixed-width binary-reference lookup formulas -- proof internals

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.eval_wordEqual_internal {width : ℕ} (word : Fin width → BoolFormula) (value : BitString width) (assignment : ℕ → Bool) : BoolFormula.eval assignment (wordEqual word value) = decide (evaluatedWord word assignment = value)

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.eval_select_internal {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (assignment : ℕ → Bool) (hcount : count ≤ 2 ^ width) : BoolFormula.eval assignment (select word values) = if hvalue : (evaluatedWord word assignment).unsignedValue < count then BoolFormula.eval assignment (values ⟨(evaluatedWord word assignment).unsignedValue, hvalue⟩) else false

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.size_wordEqual_internal {width : ℕ} (word : Fin width → BoolFormula) (value : BitString width) (hword : ∀ (coordinate : Fin width), (word coordinate).size = 1) : (wordEqual word value).size = 30 * width + 3

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.size_select_internal {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (hword : ∀ (coordinate : Fin width), (word coordinate).size = 1) (hvalues : ∀ (index : Fin count), (values index).size = 1) : (select word values).size = selectSize width count

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.vars_select_lt_internal {width count available : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (hword : ∀ (coordinate : Fin width), ∀ wire ∈ (word coordinate).vars, wire < available) (hvalues : ∀ (index : Fin count), ∀ wire ∈ (values index).vars, wire < available) (wire : ℕ) : wire ∈ (select word values).vars → wire < available