29.3 Slack-form dictionaries

This module defines the fixed-slot dictionary representation used by the Chapter 29 SIMPLEX development. Basic and nonbasic slots keep fixed matrix dimensions while an equivalence records which original or slack variable currently occupies each slot.

Main declarations:

LPVar: original and slack variable names.
Dictionary: CLRS slack-form coefficients and variable labels.
Dictionary.Satisfies: the represented row equations.
Dictionary.IsBasicFeasible: nonnegative basic right-hand sides.

Downstream layers:

Basic solutions, initial dictionaries, and PIVOT are proved in later modules.

              namespace CLRSnamespace Chapter29open Matrixopen scoped BigOperators

Variable names for an LP with n original variables and m slack variables.

abbrev LPVar (m n : ℕ) := Fin n ⊕ Fin m

A CLRS slack-form dictionary with fixed basic/nonbasic slots.

The equivalence labels carries stable variable identities across pivots; the matrices remain indexed by the fixed row and column slots.

Variable occupying each basic (inl) or nonbasic (inr) slot.

Constant term for each basic row.

Row coefficients in x_B = b - A x_N.

Constant term of the objective expression.

Coefficients in z = v + cᵀx_N.

              structure Dictionary (m n : ℕ) where  labels : (Fin m ⊕ Fin n) ≃ LPVar m n  b : Fin m → ℝ  a : Matrix (Fin m) (Fin n) ℝ  v : ℝ  c : Fin n → ℝ

namespace Dictionary

The variable occupying basic row i.

def basicVar (D : Dictionary m n) (i : Fin m) : LPVar m n :=
  D.labels (.inl i)

The variable occupying nonbasic column j.

def nonbasicVar (D : Dictionary m n) (j : Fin n) : LPVar m n :=
  D.labels (.inr j)

The right-hand side bᵢ - Σⱼ aᵢⱼxⱼ of one dictionary row.

def rowRhs (D : Dictionary m n) (x : LPVar m n → ℝ) (i : Fin m) : ℝ :=
  D.b i - ∑ j, D.a i j * x (D.nonbasicVar j)

The objective expression v + Σⱼ cⱼxⱼ represented by a dictionary.

def objectiveRhs (D : Dictionary m n) (x : LPVar m n → ℝ) : ℝ :=
  D.v + ∑ j, D.c j * x (D.nonbasicVar j)

A complete assignment satisfies a dictionary when every basic variable equals its represented row expression.

def Satisfies (D : Dictionary m n) (x : LPVar m n → ℝ) : Prop :=
  ∀ i, x (D.basicVar i) = D.rowRhs x i

A dictionary's basic solution is feasible exactly when every row constant is nonnegative.

def IsBasicFeasible (D : Dictionary m n) : Prop :=
  ∀ i, 0 ≤ D.b i

              end Dictionaryend Chapter29end CLRS