Primal-dual LP data and HSDE notation

This file is intended to be a stable foundation. It contains the LP data, homogeneous self-dual variables, complementarity/gap notation, and the neighborhood definitions used later in the proof.

Lean-reading hints for beginners:

• structure is a record type. Its fields become named assumptions/data.
• def introduces a definition; theorem introduces a proved proposition.
• namespace HSDInteriorPointLP prevents names from clashing with Mathlib.
• simp only [...] rewrites only by the listed rules. It is safer than bare simp in a long proof because the simplification set does not change silently.

HSDE-LP proof skeleton with separated (x, τ) and (s, κ) variables

This version keeps the homogenizing variables explicit:

• primal-side variables: x : Vec n and tau : ℝ;
• dual/complementarity-side variables: s : Vec n and kappa : ℝ.

This is closer to the Ye--Todd--Mizuno HLP notation and is easier to compare with Clarabel-style homogeneous embedding variables. It is mathematically equivalent to bundling (x,τ) and (s,κ) into vectors of dimension n+1, but the separated form makes the special scalar complementarity term τκ visible.

The remaining YTM predictor/corrector neighborhood estimates are kept only in the fixed-parameter YTM form: tight neighborhood 1/4, wide neighborhood 1/2, and predictor step constant 8^{-2.5}.

Short Lean proof-command guide

The file is written for readers who know the interior-point algebra but may be new to Lean.

• intro introduces an assumption or quantified variable from the current goal.
• have h : P := by ... proves and names an intermediate claim.
• rcases h with ⟨...⟩ unpacks conjunctions, existentials, and structures.
• simp only [...] performs controlled rewriting using only the listed facts.
• simpa [defs] using h simplifies the goal and the type of h, then applies h.
• linarith closes linear real-arithmetic goals from the available hypotheses.
• nlinarith is the same idea for nonlinear arithmetic such as products/squares.
• ring proves polynomial identities over rings such as ℝ.

@[reducible, inline]

abbrev HSDInteriorPointLP.Vec (n : ℕ) : Type

Real coordinate vectors indexed by Fin n.

Equations

• HSDInteriorPointLP.Vec n = (Fin n → ℝ)

structure HSDInteriorPointLP.LPData (m n : ℕ) : Type

Standard-form LP data for the Ye--Todd--Mizuno HLP construction: min cᵀx subject to Ax = b, x ≥ 0.

• A : Matrix (Fin m) (Fin n) ℝ

  Constraint matrix.

• b : Vec m

  Right-hand side vector.

• c : Vec n

  Objective vector.

def HSDInteriorPointLP.FullRowRank {m n : ℕ} (P : LPData m n) : Prop

Full row rank of A, written without importing a separate linear-independence API. This says that the only linear combination of the rows of A equal to zero is the trivial one. This is the standard full-row-rank assumption used in primal-dual IPM analyses.

Equations

• HSDInteriorPointLP.FullRowRank P = ∀ (y : HSDInteriorPointLP.Vec m), (∀ (j : Fin n), ∑ i : Fin m, y i * P.A i j = 0) → ∀ (i : Fin m), y i = 0

structure HSDInteriorPointLP.LPStandardAssumptions {m n : ℕ} (P : LPData m n) : Prop

Standard assumptions for the LP-level HLP skeleton. For the current LP proof skeleton we only record full row rank explicitly. Interior/nonemptiness assumptions belong to the neighborhood and local-theory statements below.

• full_row_rank : FullRowRank P

def HSDInteriorPointLP.hdim (n : ℕ) : ℝ

Homogeneous complementarity dimension n + 1.

Equations

• HSDInteriorPointLP.hdim n = ↑n + 1

def HSDInteriorPointLP.dot {n : ℕ} (u v : Vec n) : ℝ

Euclidean dot product on finite real vectors.

Equations

• HSDInteriorPointLP.dot u v = ∑ i : Fin n, u i * v i

def HSDInteriorPointLP.hdot {n : ℕ} (x : Vec n) (tau : ℝ) (s : Vec n) (kappa : ℝ) : ℝ

Pairing of (x,τ) and (s,κ): xᵀs + τκ.

Equations

• HSDInteriorPointLP.hdot x tau s kappa = HSDInteriorPointLP.dot x s + tau * kappa

def HSDInteriorPointLP.centerSq {n : ℕ} (x : Vec n) (tau : ℝ) (s : Vec n) (kappa μ : ℝ) : ℝ

Squared centrality deviation for (xᵢsᵢ, τκ) from μe.

Equations

• HSDInteriorPointLP.centerSq x tau s kappa μ = ∑ i : Fin n, (x i * s i - μ) ^ 2 + (tau * kappa - μ) ^ 2

structure HSDInteriorPointLP.HSState (n : ℕ) : Type

Homogeneous self-dual state with primal and dual/complementarity variables.

• x : Vec n

  Primal vector.

• tau : ℝ

  Primal homogenizing scalar.

• s : Vec n

  Dual slack vector.

• kappa : ℝ

  Dual homogenizing scalar.

structure HSDInteriorPointLP.HSDirection (n : ℕ) : Type

Homogeneous self-dual search direction.

• dx : Vec n

  Primal-vector direction.

• dtau : ℝ

  Primal homogenizing scalar direction.

• ds : Vec n

  Dual-slack direction.

• dkappa : ℝ

  Dual homogenizing scalar direction.

def HSDInteriorPointLP.Interior {n : ℕ} (w : HSState n) : Prop

Strict positivity of every HSD state component.

Equations

• HSDInteriorPointLP.Interior w = ((∀ (i : Fin n), 0 < w.x i) ∧ 0 < w.tau ∧ (∀ (i : Fin n), 0 < w.s i) ∧ 0 < w.kappa)

def HSDInteriorPointLP.gap {n : ℕ} (w : HSState n) : ℝ

Complementarity gap of an HSD state.

Equations

• HSDInteriorPointLP.gap w = HSDInteriorPointLP.hdot w.x w.tau w.s w.kappa

noncomputable def HSDInteriorPointLP.mu {n : ℕ} (w : HSState n) : ℝ

Average complementarity measure.

Equations

• HSDInteriorPointLP.mu w = HSDInteriorPointLP.gap w / HSDInteriorPointLP.hdim n

def HSDInteriorPointLP.HSDNeighborhood {n : ℕ} (β : ℝ) (w : HSState n) : Prop

HSDE central neighborhood corresponding to the YTM neighborhood ‖(Xs, τκ) - μe‖ ≤ β μ, written with squared Euclidean norm.

Equations

• One or more equations did not get rendered due to their size.

def HSDInteriorPointLP.addStep {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) : HSState n

Apply a scalar step along an HSD search direction.

Equations

• HSDInteriorPointLP.addStep w d α = { x := fun (i : Fin n) => w.x i + α * d.dx i, tau := w.tau + α * d.dtau, s := fun (i : Fin n) => w.s i + α * d.ds i, kappa := w.kappa + α * d.dkappa }

structure HSDInteriorPointLP.HLPNullDirection {n : ℕ} (d : HSDirection n) : Prop

Direction lies in the HLP nullspace, recorded through the skew-symmetry consequence used in the complementarity-gap calculation.

In the full HLP formulation this identity is obtained by multiplying the four linearized HLP equality equations by the corresponding direction components and adding them. See HLPNullDirection_from_full_nullspace below for the concrete calculation from the separated full equations.

• cross_zero : hdot d.dx d.dtau d.ds d.dkappa = 0

structure HSDInteriorPointLP.HSDSkewOrthogonal {n : ℕ} (d : HSDirection n) : Prop

Skew-symmetry of the HLP constraint matrix gives this orthogonality.

• cross_zero : hdot d.dx d.dtau d.ds d.dkappa = 0

structure HSDInteriorPointLP.HSDComplementarityDirection {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) : Prop

Complementarity equation used in the predictor/corrector system. For γ = 0 this is the predictor equation. For γ = 1 this is the corrector equation.

• component_eq (i : Fin n) : w.x i * d.ds i + w.s i * d.dx i = γ * mu w - w.x i * w.s i
• scalar_eq : w.tau * d.dkappa + w.kappa * d.dtau = γ * mu w - w.tau * w.kappa
• aggregate_eq : hdot w.x w.tau d.ds d.dkappa + hdot d.dx d.dtau w.s w.kappa = -(1 - γ) * gap w

structure HSDInteriorPointLP.HSDStepDirection {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) : Prop

A single YTM-type linearized step direction for the HLP.

• null_dir : HLPNullDirection d
• skew : HSDSkewOrthogonal d
• compl : HSDComplementarityDirection w d γ

structure HSDInteriorPointLP.HSDDirectionEquation {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) : Prop

The linear system that defines a YTM-type search direction.

The first field represents membership in the HLP nullspace, i.e., the linearized HLP equalities. The last two fields are the linearized complementarity equations for (x,s) and (τ,κ). The parameter γ distinguishes the predictor (γ = 0) from the corrector (γ = 1).

• null_dir : HLPNullDirection d
• component_eq (i : Fin n) : w.x i * d.ds i + w.s i * d.dx i = γ * mu w - w.x i * w.s i
• scalar_eq : w.tau * d.dkappa + w.kappa * d.dtau = γ * mu w - w.tau * w.kappa

Concrete YTM/HLP full-direction layer

The earlier HSDirectionEquation works only with the reduced variables (dx,dτ,ds,dκ). The actual Ye--Todd--Mizuno HLP Newton system also contains dy and dθ. The following definitions expose that full search-direction layer.

def HSDInteriorPointLP.matVec {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (x : Vec n) : Vec m

Matrix-vector multiplication for the row-indexed constraint matrix.

Equations

• HSDInteriorPointLP.matVec A x i = ∑ j : Fin n, A i j * x j

def HSDInteriorPointLP.tMatVec {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (y : Vec m) : Vec n

Transposed matrix-vector multiplication.

Equations

• HSDInteriorPointLP.tMatVec A y j = ∑ i : Fin m, A i j * y i

theorem HSDInteriorPointLP.dot_tMatVec_eq_dot_matVec {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (y : Vec m) (x : Vec n) : dot x (tMatVec A y) = dot y (matVec A x)

Finite-dimensional adjointness of matVec and tMatVec.

def HSDInteriorPointLP.ones {n : ℕ} : Vec n

All-ones vector.

Equations

• HSDInteriorPointLP.ones x✝ = 1

def HSDInteriorPointLP.bbar {m n : ℕ} (P : LPData m n) : Vec m

The YTM simplified HLP uses bbar = b - A e.

Equations

• HSDInteriorPointLP.bbar P i = P.b i - HSDInteriorPointLP.matVec P.A HSDInteriorPointLP.ones i

def HSDInteriorPointLP.cbar {m n : ℕ} (P : LPData m n) : Vec n

The YTM simplified HLP uses cbar = c - e.

Equations

• HSDInteriorPointLP.cbar P j = P.c j - 1

def HSDInteriorPointLP.zbar {m n : ℕ} (P : LPData m n) : ℝ

The YTM simplified HLP uses zbar = cᵀe + 1.

Equations

• HSDInteriorPointLP.zbar P = HSDInteriorPointLP.dot P.c HSDInteriorPointLP.ones + 1

structure HSDInteriorPointLP.HLPFullDirection (m n : ℕ) : Type

Full HLP direction, including the equality-multiplier direction dy and the free homogenizing direction dθ.

• dy : Vec m

  Equality-multiplier direction.

• dx : Vec n

  Primal-vector direction.

• dtau : ℝ

  Primal homogenizing scalar direction.

• dtheta : ℝ

  Free homogenizing direction.

• ds : Vec n

  Dual-slack direction.

• dkappa : ℝ

  Dual homogenizing scalar direction.

def HSDInteriorPointLP.HLPFullDirection.toHSDirection {m n : ℕ} (D : HLPFullDirection m n) : HSDirection n

Forget the free/equality components and retain the reduced complementarity variables.

Equations

• D.toHSDirection = { dx := D.dx, dtau := D.dtau, ds := D.ds, dkappa := D.dkappa }

structure HSDInteriorPointLP.HLPNullspaceEquations {m n : ℕ} (P : LPData m n) (D : HLPFullDirection m n) : Prop

Linearized HLP equalities in the simplified YTM HLP form.

These equations are the full analogue of membership in the HLP nullspace. They correspond to the four displayed equations in Theorem 5(ii) of Ye--Todd--Mizuno, after adding the slack directions ds and dκ and keeping the free direction dθ.

• primal_eq (i : Fin m) : matVec P.A D.dx i - P.b i * D.dtau + bbar P i * D.dtheta = 0
• dual_eq (j : Fin n) : -tMatVec P.A D.dy j + P.c j * D.dtau - cbar P j * D.dtheta - D.ds j = 0
• gap_eq : dot P.b D.dy - dot P.c D.dx + zbar P * D.dtheta - D.dkappa = 0
• normalizing_eq : -dot (bbar P) D.dy + dot (cbar P) D.dx - zbar P * D.dtau = 0

structure HSDInteriorPointLP.HLPFullDirectionEquation {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (γ : ℝ) : Prop

Full YTM search-direction equations: HLP nullspace plus the linearized complementarity equations.

• null_eqs : HLPNullspaceEquations P D
• component_eq (i : Fin n) : w.x i * D.ds i + w.s i * D.dx i = γ * mu w - w.x i * w.s i
• scalar_eq : w.tau * D.dkappa + w.kappa * D.dtau = γ * mu w - w.tau * w.kappa

noncomputable def HSDInteriorPointLP.complRhs {n : ℕ} (w : HSState n) (γ : ℝ) : Vec n

Right-hand side of the complementarity part of the YTM Newton system.

Equations

• HSDInteriorPointLP.complRhs w γ i = γ * HSDInteriorPointLP.mu w - w.x i * w.s i

noncomputable def HSDInteriorPointLP.scalarComplRhs {n : ℕ} (w : HSState n) (γ : ℝ) : ℝ

Right-hand side of the scalar complementarity equation.

Equations

• HSDInteriorPointLP.scalarComplRhs w γ = γ * HSDInteriorPointLP.mu w - w.tau * w.kappa

structure HSDInteriorPointLP.HLPNewtonBlockSystem {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (γ : ℝ) : Prop

The full HLP Newton block operator, written as equations rather than as a single matrix. The output consists of the four HLP nullspace residuals and the n+1 complementarity residuals. Thus solving the Newton system means finding D such that this operator equals the right-hand side encoded below.

For the homogeneous self-dual LP of Ye--Todd--Mizuno, the first four blocks are the linearized HLP equalities, while the last two blocks are the linearized complementarity equations.

• primal_block (i : Fin m) : matVec P.A D.dx i - P.b i * D.dtau + bbar P i * D.dtheta = 0
• dual_block (j : Fin n) : -tMatVec P.A D.dy j + P.c j * D.dtau - cbar P j * D.dtheta - D.ds j = 0
• gap_block : dot P.b D.dy - dot P.c D.dx + zbar P * D.dtheta - D.dkappa = 0
• normalizing_block : -dot (bbar P) D.dy + dot (cbar P) D.dx - zbar P * D.dtau = 0
• complementarity_block (i : Fin n) : w.x i * D.ds i + w.s i * D.dx i = complRhs w γ i
• scalar_complementarity_block : w.tau * D.dkappa + w.kappa * D.dtau = scalarComplRhs w γ

theorem HSDInteriorPointLP.full_direction_equation_iff_block_system {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (γ : ℝ) : HLPFullDirectionEquation P w D γ ↔ HLPNewtonBlockSystem P w D γ

The block-system formulation is equivalent to the previous bundled full direction equation. This direction is useful because the block system exposes the Newton matrix whose nonsingularity must be proved from full row rank and interiority.

structure HSDInteriorPointLP.HLPNewtonHomogeneousBlockSystem {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) : Prop

Homogeneous version of the full Newton block system.

This is the kernel system obtained by replacing the complementarity right-hand side by zero. Proving that its only solution is zero is the standard injectivity step in the finite-dimensional solvability proof of the HLP Newton equations.

• primal_block (i : Fin m) : matVec P.A D.dx i - P.b i * D.dtau + bbar P i * D.dtheta = 0
• dual_block (j : Fin n) : -tMatVec P.A D.dy j + P.c j * D.dtau - cbar P j * D.dtheta - D.ds j = 0
• gap_block : dot P.b D.dy - dot P.c D.dx + zbar P * D.dtheta - D.dkappa = 0
• normalizing_block : -dot (bbar P) D.dy + dot (cbar P) D.dx - zbar P * D.dtau = 0
• complementarity_block (i : Fin n) : w.x i * D.ds i + w.s i * D.dx i = 0
• scalar_complementarity_block : w.tau * D.dkappa + w.kappa * D.dtau = 0

Finite-dimensional solvability of the full Newton block

The solvability step is a purely finite-dimensional linear-algebra argument. We encode the unknowns (dy,dx,dτ,dθ,ds,dκ) and the six residual blocks in the same product vector space. The concrete Newton block is then a linear self-map on this space. Since the homogeneous block has only the zero solution, the self-map is injective; in finite dimension, injectivity of a self-map implies surjectivity.

@[reducible, inline]

abbrev HSDInteriorPointLP.HLPBlockSpace (m n : ℕ) : Type

Product vector space used for the full HLP Newton unknowns and residuals.

Equations

• HSDInteriorPointLP.HLPBlockSpace m n = (HSDInteriorPointLP.Vec m × HSDInteriorPointLP.Vec n × ℝ × ℝ × HSDInteriorPointLP.Vec n × ℝ)

def HSDInteriorPointLP.HLPFullDirection.toBlockVector {m n : ℕ} (D : HLPFullDirection m n) : HLPBlockSpace m n

Encode a full HLP direction as a vector in the product block space.

Equations

• D.toBlockVector = (D.dy, D.dx, D.dtau, D.dtheta, D.ds, D.dkappa)

def HSDInteriorPointLP.HLPFullDirection.ofBlockVector {m n : ℕ} (u : HLPBlockSpace m n) : HLPFullDirection m n

Decode a product block vector as a full HLP direction.

Equations

• HSDInteriorPointLP.HLPFullDirection.ofBlockVector u = { dy := u.1, dx := u.2.1, dtau := u.2.2.1, dtheta := u.2.2.2.1, ds := u.2.2.2.2.1, dkappa := u.2.2.2.2.2 }

@[simp]

theorem HSDInteriorPointLP.HLPFullDirection.of_toBlockVector {m n : ℕ} (D : HLPFullDirection m n) : ofBlockVector D.toBlockVector = D

@[simp]

theorem HSDInteriorPointLP.HLPFullDirection.to_ofBlockVector {m n : ℕ} (u : HLPBlockSpace m n) : (ofBlockVector u).toBlockVector = u

noncomputable def HSDInteriorPointLP.HLPNewtonBlockRhs {n : ℕ} (w : HSState n) (γ : ℝ) (m : ℕ) : HLPBlockSpace m n

Right-hand side of the full Newton block system in the same block space.

Equations

• HSDInteriorPointLP.HLPNewtonBlockRhs w γ m = (0, 0, 0, 0, HSDInteriorPointLP.complRhs w γ, HSDInteriorPointLP.scalarComplRhs w γ)

This file contains the stable foundation: data structures, elementary HSDE/HLP definitions, and basic algebraic identities used by the work file. It intentionally stops before HLPNewtonBlockOperator, where the current active proof engineering is happening.