Dense Gaussian elimination over the Boolean ring

Each equation consists of a Boolean coefficient row and a Boolean right-hand side. A column step selects a row whose leading coefficient is one, adds it to all other rows with leading coefficient one, and drops the column. The selected row becomes 0 = 0; retaining it keeps the number of equations fixed. If the column is zero, the step simply drops it. Repeating once per column leaves only constant equations. This is the elimination argument following Theorem 4.3 of [Che06], printed p. 16 (arXiv version 1).

The native multi-tape certificate composes the library's list operations and bounded iteration. Every step weakly decreases the complete encoded state length, including on malformed rows. The explicit width is unary; coefficient words and right-hand sides use their ordinary binary encodings. Inputs with a row of a different width are rejected.

Main definitions

• Cslib.Complexity.XORSAT.Dense.Row: Boolean coefficient word and right-hand side.
• Cslib.Complexity.XORSAT.Dense.Input: declared variable width and dense equation rows.
• Cslib.Complexity.XORSAT.Dense.step: one elimination column.
• Cslib.Complexity.XORSAT.Dense.decide: the dense-system decision algorithm.

structure Cslib.Complexity.XORSAT.Dense.Row : Type

A dense parity equation row with a Boolean coefficient word and Boolean right-hand side.

• coeffs : List Bool

  The Boolean coefficient word, one entry per declared variable column.

• rhs : Bool

  The Boolean right-hand side of the parity equation.

theorem Cslib.Complexity.XORSAT.Dense.Row.ext {x y : Row} (coeffs : x.coeffs = y.coeffs) (rhs : x.rhs = y.rhs) : x = y

theorem Cslib.Complexity.XORSAT.Dense.Row.ext_iff {x y : Row} : x = y ↔ x.coeffs = y.coeffs ∧ x.rhs = y.rhs

@[instance_reducible]

instance Cslib.Complexity.XORSAT.Dense.instDecidableEqRow : DecidableEq Row

def Cslib.Complexity.XORSAT.Dense.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev Cslib.Complexity.XORSAT.Dense.System : Type

A list of dense equations.

structure Cslib.Complexity.XORSAT.Dense.Input : Type

A dense XOR-SAT instance with a unary declared width and a list of equation rows.

• width : ℕ

  The unary-encoded declared number of variable columns.

• rows : System

  The list of dense equation rows.

theorem Cslib.Complexity.XORSAT.Dense.Input.ext_iff {x y : Input} : x = y ↔ x.width = y.width ∧ x.rows = y.rows

theorem Cslib.Complexity.XORSAT.Dense.Input.ext {x y : Input} (width : x.width = y.width) (rows : x.rows = y.rows) : x = y

@[instance_reducible]

instance Cslib.Complexity.XORSAT.Dense.instDecidableEqInput : DecidableEq Input

def Cslib.Complexity.XORSAT.Dense.instDecidableEqInput.decEq (x✝ x✝¹ : Input) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.XORSAT.Dense.dot : List Bool → List Bool → Bool

Dot product over the Boolean ring; missing coordinates have value zero.

def Cslib.Complexity.XORSAT.Dense.Width (n : ℕ) (F : System) : Prop

Every row has the declared number of coefficients.

def Cslib.Complexity.XORSAT.Dense.Holds (F : System) (a : List Bool) : Prop

An assignment satisfies every equation.

def Cslib.Complexity.XORSAT.Dense.Satisfiable (n : ℕ) (F : System) : Prop

A solution has exactly the declared width.

def Cslib.Complexity.XORSAT.Dense.clear (p e : Row) : Row

Substitute the first variable using a pivot equation, then drop that variable.

def Cslib.Complexity.XORSAT.Dense.step (F : System) : System

One column of Gaussian elimination. A missing pivot means that the column is zero.

@[simp]

theorem Cslib.Complexity.XORSAT.Dense.encRow_apply (a : Row) : encRow a = encRowFields (a.coeffs, a.rhs)

@[reducible, inline]

abbrev Cslib.Complexity.XORSAT.Dense.encRowFields : List Bool × Bool ↪ List Bool

The tuple of the fields of encRow.

theorem Cslib.Complexity.XORSAT.Dense.encRow_rhs_deg : Turing.MultiTapeTM.ComputableInDegree Row.rhs encRow Turing.MultiTapeTM.encBool 1 1

theorem Cslib.Complexity.XORSAT.Dense.encRow_coeffs_deg : Turing.MultiTapeTM.ComputableInDegree Row.coeffs encRow Turing.MultiTapeTM.encBits 1 1

theorem Cslib.Complexity.XORSAT.Dense.encRow_rhs_inO : Turing.MultiTapeTM.ComputableInO Row.rhs encRow Turing.MultiTapeTM.encBool (fun (a : Row) => (encRow a).length) fun (a : Row) => (encRow a).length

theorem Cslib.Complexity.XORSAT.Dense.encRow_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Row) => (a.coeffs, a.rhs)) encRow encRowFields 1 1

theorem Cslib.Complexity.XORSAT.Dense.encRow_coeffs_inO : Turing.MultiTapeTM.ComputableInO Row.coeffs encRow Turing.MultiTapeTM.encBits (fun (a : Row) => (encRow a).length) fun (a : Row) => (encRow a).length

theorem Cslib.Complexity.XORSAT.Dense.encRow_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List Bool} {x1 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encBits budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encBool budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encRow budget

theorem Cslib.Complexity.XORSAT.Dense.encRow_rhs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Row} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encRow S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).rhs) encIn✝ Turing.MultiTapeTM.encBool S✝

theorem Cslib.Complexity.XORSAT.Dense.encRow_coeffs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Row} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRow → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).coeffs) encIn✝ Turing.MultiTapeTM.encBits

theorem Cslib.Complexity.XORSAT.Dense.encRow_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List Bool × Bool) => { coeffs := p.1, rhs := p.2 }) encRowFields encRow 1 1

theorem Cslib.Complexity.XORSAT.Dense.encRow_coeffs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Row} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encRow S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).coeffs) encIn✝ Turing.MultiTapeTM.encBits S✝

theorem Cslib.Complexity.XORSAT.Dense.encRow_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List Bool} {T0 S0 : γ → ℕ} {x1 : γ → Bool} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encBits T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encBool T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encRow (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

def Cslib.Complexity.XORSAT.Dense.encRow : Row ↪ List Bool

Framed rows with raw binary coefficient words.

theorem Cslib.Complexity.XORSAT.Dense.encRow_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List Bool} {x1 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encBits) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encRow

theorem Cslib.Complexity.XORSAT.Dense.encRow_rhs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Row} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRow → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).rhs) encIn✝ Turing.MultiTapeTM.encBool

@[reducible, inline]

abbrev Cslib.Complexity.XORSAT.Dense.encSystem : System ↪ List Bool

A framed list of rows.

@[simp]

theorem Cslib.Complexity.XORSAT.Dense.encInput_apply (a : Input) : encInput a = encInputFields (a.width, a.rows)

theorem Cslib.Complexity.XORSAT.Dense.encInput_rows_inO : Turing.MultiTapeTM.ComputableInO Input.rows encInput encSystem (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.XORSAT.Dense.encInput_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × System) => { width := p.1, rows := p.2 }) encInputFields encInput 1 1

theorem Cslib.Complexity.XORSAT.Dense.encInput_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Input) => (a.width, a.rows)) encInput encInputFields 1 1

theorem Cslib.Complexity.XORSAT.Dense.encInput_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → System} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encUnary budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn encSystem budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { width := x0 x, rows := x1 x }) encIn encInput budget

theorem Cslib.Complexity.XORSAT.Dense.encInput_rows_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).rows) encIn✝ encSystem

theorem Cslib.Complexity.XORSAT.Dense.encInput_rows_deg : Turing.MultiTapeTM.ComputableInDegree Input.rows encInput encSystem 1 1

theorem Cslib.Complexity.XORSAT.Dense.encInput_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → System} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encUnary) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn encSystem) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { width := x0 x, rows := x1 x }) encIn encInput

theorem Cslib.Complexity.XORSAT.Dense.encInput_width_deg : Turing.MultiTapeTM.ComputableInDegree Input.width encInput Turing.MultiTapeTM.encUnary 1 1

theorem Cslib.Complexity.XORSAT.Dense.encInput_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → System} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encUnary T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn encSystem T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { width := x0 x, rows := x1 x }) encIn encInput (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

def Cslib.Complexity.XORSAT.Dense.encInput : Input ↪ List Bool

Unary declared width and a framed list of rows.

theorem Cslib.Complexity.XORSAT.Dense.encInput_rows_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).rows) encIn✝ encSystem S✝

theorem Cslib.Complexity.XORSAT.Dense.encInput_width_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).width) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.XORSAT.Dense.encInput_width_inO : Turing.MultiTapeTM.ComputableInO Input.width encInput Turing.MultiTapeTM.encUnary (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.XORSAT.Dense.encInput_width_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).width) encIn✝ Turing.MultiTapeTM.encUnary S✝

@[reducible, inline]

abbrev Cslib.Complexity.XORSAT.Dense.encInputFields : ℕ × System ↪ List Bool

The tuple of the fields of encInput.

def Cslib.Complexity.XORSAT.Dense.decide (q : Input) : Bool

Check the row widths, eliminate all columns, then reject a remaining equation 0 = 1.

theorem Cslib.Complexity.XORSAT.Dense.clear_holds_iff (p e : Row) (h : e.coeffs.length = p.coeffs.length) (b : Bool) (a : List Bool) (hp : p.coeffs.headD false = true) (hpa : dot p.coeffs (b :: a) = p.rhs) : dot (clear p e).coeffs a = (clear p e).rhs ↔ dot e.coeffs (b :: a) = e.rhs

Clearing a row preserves its equation whenever the pivot equation holds.

theorem Cslib.Complexity.XORSAT.Dense.width_step {n : ℕ} {F : System} (hF : Width (n + 1) F) : Width n (step F)

The residual system has one fewer column.

theorem Cslib.Complexity.XORSAT.Dense.satisfiable_step_iff {n : ℕ} {F : System} (hF : Width (n + 1) F) : Satisfiable n (step F) ↔ Satisfiable (n + 1) F

One elimination column preserves existence of a solution.

theorem Cslib.Complexity.XORSAT.Dense.elimination_correct {n : ℕ} {F : System} (hF : Width n F) : (List.all (step^[n] F) fun (e : Row) => !e.rhs) = true ↔ Satisfiable n F

Elimination decides dense systems of the declared width.

theorem Cslib.Complexity.XORSAT.Dense.decide_eq_true_iff (q : Input) : decide q = true ↔ Width q.width q.rows ∧ Satisfiable q.width q.rows

The Boolean decider rejects malformed row widths and otherwise decides satisfiability.

theorem Cslib.Complexity.XORSAT.Dense.length_clear_le (p e : Row) : (clear p e).coeffs.length ≤ e.coeffs.length

A column operation never lengthens an individual coefficient word.

theorem Cslib.Complexity.XORSAT.Dense.length_step_le (F : System) : (encSystem (step F)).length ≤ (encSystem F).length

The complete encoded state weakly decreases at every iteration; there is no growth hidden in repeated substitution or in the framing of rows.

theorem Cslib.Complexity.XORSAT.Dense.computableInPolyTime_decide : Turing.MultiTapeTM.ComputableInPolyTime decide encInput Turing.MultiTapeTM.encBool

The actual Gaussian-elimination decider is computable in polynomial time on native multi-tape Turing machines, with unary width and raw binary coefficient words.

theorem Cslib.Complexity.XORSAT.Dense.satisfiable_mem_P : {q : Input | Width q.width q.rows ∧ Satisfiable q.width q.rows} ∈ P encInput

Dense XOR-SAT is in the native Turing-machine class P.