Executable rational linear solving with module-valued right-hand sides

Gaussian elimination and back-substitution for A x = b, where A has rational entries and b and x take values in any ℚ-module M with decidable equality. Declaration checking needs this generality: the coefficients (exponents of base units) are rational, but the right-hand sides are logarithms of declared factors. DeclSolver.solve takes M to be LogFactor, whose equality is decided in exact rational arithmetic; DeclSolver.factorCoefficients and DeclarationComplete.checkSpan take M = ℚ.

Pivot selection is a finite search for a nonzero rational coefficient. A row whose coefficients are all zero after reduction is a rigid residual: the system has no solution if its right-hand side is nonzero, and that is the only equality test performed in M. Variables never chosen as pivots are set to 0. No basis choice, real equality test, or noncomputable data occurs.

The entry point is solve. solve_sound shows that every returned assignment satisfies the system, and solve_isSome_iff that solve succeeds exactly when a solution exists in M. solve_map and solvable_map_iff transfer solvability along an injective ℚ-linear map; DeclSolver.solve_isSome_iff uses them with LogFactor.interpret to pass from exact logarithms to real valuations.

structure LambdaS.RationalSolver.Row (n : ℕ) (M : Type u_2) : Type u_2

One row of a rational system with a module-valued right-hand side.

• coeff : Fin n → ℚ
• rhs : M

def LambdaS.RationalSolver.Row.eval {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r : Row n M) (x : Fin n → M) : M

Evaluate a row's left-hand side.

Equations

• r.eval x = ∑ j : Fin n, r.coeff j • x j

def LambdaS.RationalSolver.Row.pivot {n : ℕ} {M : Type u_1} (r : Row n M) : Option (Fin n)

The first nonzero coefficient, or no pivot for a zero row.

Equations

• r.pivot = List.find? (fun (j : Fin n) => decide (r.coeff j ≠ 0)) (List.finRange n)

theorem LambdaS.RationalSolver.Row.pivot_none {n : ℕ} {M : Type u_1} {r : Row n M} (h : r.pivot = none) (j : Fin n) : r.coeff j = 0

theorem LambdaS.RationalSolver.Row.pivot_some {n : ℕ} {M : Type u_1} {r : Row n M} {j : Fin n} (h : r.pivot = some j) : r.coeff j ≠ 0

def LambdaS.RationalSolver.Row.reduce {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r p : Row n M) (j : Fin n) : Row n M

Row subtraction eliminates a chosen pivot coefficient.

Equations

• r.reduce p j = { coeff := fun (i : Fin n) => r.coeff i - r.coeff j / p.coeff j * p.coeff i, rhs := r.rhs - (r.coeff j / p.coeff j) • p.rhs }

theorem LambdaS.RationalSolver.Row.reduce_pivot {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r p : Row n M) (j : Fin n) (hp : p.coeff j ≠ 0) : (r.reduce p j).coeff j = 0

theorem LambdaS.RationalSolver.Row.eval_reduce {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r p : Row n M) (j : Fin n) (x : Fin n → M) : (r.reduce p j).eval x = r.eval x - (r.coeff j / p.coeff j) • p.eval x

theorem LambdaS.RationalSolver.Row.reduce_satisfied_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r p : Row n M) (j : Fin n) (x : Fin n → M) (hp : p.eval x = p.rhs) : (r.reduce p j).eval x = (r.reduce p j).rhs ↔ r.eval x = r.rhs

def LambdaS.RationalSolver.Row.backsub {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (p : Row n M) (j : Fin n) (x : Fin n → M) : Fin n → M

Solve one pivot variable with the remaining coordinates held fixed.

Equations

• p.backsub j x = Function.update x j ((p.coeff j)⁻¹ • (p.rhs - ∑ i ∈ Finset.univ.erase j, p.coeff i • x i))

theorem LambdaS.RationalSolver.Row.backsub_satisfies {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (p : Row n M) (j : Fin n) (hp : p.coeff j ≠ 0) (x : Fin n → M) : p.eval (p.backsub j x) = p.rhs

theorem LambdaS.RationalSolver.Row.eval_backsub_of_zero {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r p : Row n M) (j : Fin n) (hj : r.coeff j = 0) (x : Fin n → M) : r.eval (p.backsub j x) = r.eval x

def LambdaS.RationalSolver.Solves {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (rows : List (Row n M)) (x : Fin n → M) : Prop

A concrete assignment satisfies every equation in a row list.

Equations

• LambdaS.RationalSolver.Solves rows x = ∀ r ∈ rows, r.eval x = r.rhs

@[simp]

theorem LambdaS.RationalSolver.solves_nil {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (x : Fin n → M) : Solves [] x

@[simp]

theorem LambdaS.RationalSolver.solves_cons {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (r : Row n M) (rows : List (Row n M)) (x : Fin n → M) : Solves (r :: rows) x ↔ r.eval x = r.rhs ∧ Solves rows x

def LambdaS.RationalSolver.reduceRows {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (rows : List (Row n M)) (p : Row n M) (j : Fin n) : List (Row n M)

Reduce all remaining rows against one pivot.

Equations

• LambdaS.RationalSolver.reduceRows rows p j = List.map (fun (r : LambdaS.RationalSolver.Row n M) => r.reduce p j) rows

@[simp]

theorem LambdaS.RationalSolver.length_reduceRows {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (rows : List (Row n M)) (p : Row n M) (j : Fin n) : (reduceRows rows p j).length = rows.length

theorem LambdaS.RationalSolver.solves_reduceRows_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (rows : List (Row n M)) (p : Row n M) (j : Fin n) (x : Fin n → M) (hp : p.eval x = p.rhs) : Solves (reduceRows rows p j) x ↔ Solves rows x

theorem LambdaS.RationalSolver.backsub_solves {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] (rows : List (Row n M)) (p : Row n M) (j : Fin n) (hp : p.coeff j ≠ 0) (x : Fin n → M) (hx : Solves (reduceRows rows p j) x) : Solves (p :: rows) (p.backsub j x)

@[irreducible]

def LambdaS.RationalSolver.solveRows {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] : List (Row n M) → Option (Fin n → M)

Gaussian elimination with executable pivot search and back-substitution. Each call consumes the head row. A row with a pivot eliminates that variable from the remaining rows, and back-substitution solves for it after the recursive call. A row with no pivot is dropped when its right-hand side is 0 and makes the result none otherwise. Variables never chosen as pivots are set to 0.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.RationalSolver.solveRows [] = some fun (x : Fin n) => 0

theorem LambdaS.RationalSolver.solveRows_sound {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] (rows : List (Row n M)) (x : Fin n → M) : solveRows rows = some x → Solves rows x

Every assignment the executable solver returns satisfies the system.

theorem LambdaS.RationalSolver.solveRows_complete {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] (rows : List (Row n M)) (x : Fin n → M) : Solves rows x → (solveRows rows).isSome = true

A satisfying assignment guarantees that executable solving succeeds.

theorem LambdaS.RationalSolver.solveRows_isSome_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] (rows : List (Row n M)) : (solveRows rows).isSome = true ↔ ∃ (x : Fin n → M), Solves rows x

def LambdaS.RationalSolver.matrixRows {n : ℕ} {M : Type u_1} {m : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : List (Row n M)

Turn a matrix and right-hand side into executable rows.

Equations

• LambdaS.RationalSolver.matrixRows A b = List.ofFn fun (i : Fin m) => { coeff := A i, rhs := b i }

def LambdaS.RationalSolver.solve {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {m : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : Option (Fin n → M)

Solve A x = b, where coefficients are rational and values lie in M.

Equations

• LambdaS.RationalSolver.solve A b = LambdaS.RationalSolver.solveRows (LambdaS.RationalSolver.matrixRows A b)

theorem LambdaS.RationalSolver.solves_matrixRows_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] {m : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) (x : Fin n → M) : Solves (matrixRows A b) x ↔ ∀ (i : Fin m), ∑ j : Fin n, A i j • x j = b i

theorem LambdaS.RationalSolver.solve_sound {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {m : ℕ} {A : Matrix (Fin m) (Fin n) ℚ} {b : Fin m → M} {x : Fin n → M} (h : solve A b = some x) (i : Fin m) : ∑ j : Fin n, A i j • x j = b i

Soundness of the matrix interface.

theorem LambdaS.RationalSolver.solve_isSome_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {m : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : (solve A b).isSome = true ↔ ∃ (x : Fin n → M), ∀ (i : Fin m), ∑ j : Fin n, A i j • x j = b i

Success decides solvability over the supplied decidable ℚ-module.

def LambdaS.RationalSolver.Row.map {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] (L : M →ₗ[ℚ] N) (r : Row n M) : Row n N

Apply a linear map to the right-hand side, leaving coefficients untouched.

Equations

• LambdaS.RationalSolver.Row.map L r = { coeff := r.coeff, rhs := L r.rhs }

@[simp]

theorem LambdaS.RationalSolver.Row.pivot_map {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] (L : M →ₗ[ℚ] N) (r : Row n M) : (map L r).pivot = r.pivot

@[simp]

theorem LambdaS.RationalSolver.Row.map_reduce {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] (L : M →ₗ[ℚ] N) (r p : Row n M) (j : Fin n) : map L (r.reduce p j) = (map L r).reduce (map L p) j

theorem LambdaS.RationalSolver.Row.map_backsub {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] (L : M →ₗ[ℚ] N) (p : Row n M) (j : Fin n) (x : Fin n → M) : (fun (i : Fin n) => L (p.backsub j x i)) = (map L p).backsub j fun (i : Fin n) => L (x i)

theorem LambdaS.RationalSolver.solveRows_map {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] [DecidableEq N] (L : M →ₗ[ℚ] N) (hL : Function.Injective ⇑L) (rows : List (Row n M)) : solveRows (List.map (Row.map L) rows) = Option.map (fun (x : Fin n → M) (i : Fin n) => L (x i)) (solveRows rows)

Executable solving commutes with an injective linear change of value carrier. Injectivity ensures the same rigid-residual zero tests in both.

theorem LambdaS.RationalSolver.solve_map {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] [DecidableEq N] {m : ℕ} (L : M →ₗ[ℚ] N) (hL : Function.Injective ⇑L) (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : (solve A fun (i : Fin m) => L (b i)) = Option.map (fun (x : Fin n → M) (i : Fin n) => L (x i)) (solve A b)

The matrix solver commutes with an injective linear embedding.

theorem LambdaS.RationalSolver.solvable_map_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {N : Type u_2} [AddCommGroup N] [Module ℚ N] {m : ℕ} (L : M →ₗ[ℚ] N) (hL : Function.Injective ⇑L) (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : (∃ (x : Fin n → N), ∀ (i : Fin m), ∑ j : Fin n, A i j • x j = L (b i)) ↔ ∃ (x : Fin n → M), ∀ (i : Fin m), ∑ j : Fin n, A i j • x j = b i

Solvability reflects along an injective linear embedding, even if equality in the larger carrier is not executable. Classical equality is used only in this proof, never in the solver that computes over the smaller carrier.

theorem LambdaS.RationalSolver.solve_eq_none_iff {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℚ M] [DecidableEq M] {m : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (b : Fin m → M) : solve A b = none ↔ ¬∃ (x : Fin n → M), ∀ (i : Fin m), ∑ j : Fin n, A i j • x j = b i

Failure decides absence of any solution, rather than an algorithmic inability to select pivots.

Executable boundary checks. Soundness and completeness above are kernel proofs; these guards also exercise the actual finite-search implementation.