Newton-system layer

This file connects the HSDE/HLP equations with the Newton direction used in the interior-point proof. Conceptually, this is the linear-algebra layer: the later algorithm file should not need to know the details of the Newton matrix.

Lean-reading hints for beginners:

• intro h proves an implication or a universal statement by introducing its premise/variable as the local name h.
• have h : P := by ... creates an intermediate lemma named h.
• rcases h with ⟨a, b, c⟩ decomposes a conjunction/existential proof into its components.
• simpa [defs] using h means: simplify the goal and the type of h using defs, then close the goal by h.

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 ℝ.

Active HLP/YTM proof layer

This file contains the parts that are still under active proof engineering:

• the full Newton block operator and its finite-dimensional solvability proof;
• Schur-complement complementarity arguments;
• the remaining YTM predictor/corrector local estimates.

The stable definitions and elementary lemmas are imported from HSDInteriorPointLP.PrimalDualData.

theorem HSDInteriorPointLP.finset_sum_smul_simple {ι : Type u_1} [Fintype ι] (a : ℝ) (f : ι → ℝ) : ∑ x : ι, a * f x = a * ∑ x : ι, f x

Pull a scalar out of a finite sum. This is the only finite-sum scalar rule used below; the block-operator proof invokes it through matVec, tMatVec, and dot scalar-multiplication lemmas, rather than by broad rewriting inside the large product goal.

theorem HSDInteriorPointLP.matVec_smul_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : ℝ) (x : Vec n) (i : Fin m) : matVec A (fun (j : Fin n) => a * x j) i = a * matVec A x i

Scalar multiplication in the vector argument of matVec.

theorem HSDInteriorPointLP.tMatVec_smul_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : ℝ) (y : Vec m) (j : Fin n) : tMatVec A (fun (i : Fin m) => a * y i) j = a * tMatVec A y j

Scalar multiplication in the vector argument of tMatVec.

theorem HSDInteriorPointLP.dot_smul_right {n : ℕ} (u v : Vec n) (a : ℝ) : (dot u fun (i : Fin n) => a * v i) = a * dot u v

Scalar multiplication in the second argument of dot.

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_dy {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) (i : Fin m) : (a • u).1 i = a * u.1 i

Component projections for scalar multiplication on the HLP block product space. These lemmas keep the Newton-block linearity proof away from broad simp.

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_dx {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) (j : Fin n) : (a • u).2.1 j = a * u.2.1 j

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_dtau {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) : (a • u).2.2.1 = a * u.2.2.1

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_dtheta {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) : (a • u).2.2.2.1 = a * u.2.2.2.1

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_ds {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) (j : Fin n) : (a • u).2.2.2.2.1 j = a * u.2.2.2.2.1 j

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_smul_dkappa {m n : ℕ} (a : ℝ) (u : HLPBlockSpace m n) : (a • u).2.2.2.2.2 = a * u.2.2.2.2.2

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_dy {m n : ℕ} (u v : HLPBlockSpace m n) (i : Fin m) : (u + v).1 i = u.1 i + v.1 i

Component projections for addition on the HLP block product space.

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_dx {m n : ℕ} (u v : HLPBlockSpace m n) (j : Fin n) : (u + v).2.1 j = u.2.1 j + v.2.1 j

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_dtau {m n : ℕ} (u v : HLPBlockSpace m n) : (u + v).2.2.1 = u.2.2.1 + v.2.2.1

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_dtheta {m n : ℕ} (u v : HLPBlockSpace m n) : (u + v).2.2.2.1 = u.2.2.2.1 + v.2.2.2.1

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_ds {m n : ℕ} (u v : HLPBlockSpace m n) (j : Fin n) : (u + v).2.2.2.2.1 j = u.2.2.2.2.1 j + v.2.2.2.2.1 j

@[simp]

theorem HSDInteriorPointLP.HLPBlockSpace_add_dkappa {m n : ℕ} (u v : HLPBlockSpace m n) : (u + v).2.2.2.2.2 = u.2.2.2.2.2 + v.2.2.2.2.2

def HSDInteriorPointLP.HLPNewtonBlockOperator {m n : ℕ} (P : LPData m n) (w : HSState n) : HLPBlockSpace m n →ₗ[ℝ] HLPBlockSpace m n

The full Newton block operator as a linear self-map on the product block space.

Equations

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

theorem HSDInteriorPointLP.HLPNewtonBlockOperator_eq_zero_iff_homogeneous {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) : (HLPNewtonBlockOperator P w) D.toBlockVector = 0 ↔ HLPNewtonHomogeneousBlockSystem P w D

Zero residual of the block operator is exactly the homogeneous Newton block.

theorem HSDInteriorPointLP.HLPNewtonBlockOperator_eq_rhs_iff_block_system {m n : ℕ} (P : LPData m n) (w : HSState n) (γ : ℝ) (D : HLPFullDirection m n) : (HLPNewtonBlockOperator P w) D.toBlockVector = HLPNewtonBlockRhs w γ m ↔ HLPNewtonBlockSystem P w D γ

Hitting the inhomogeneous right-hand side is exactly solving the Newton block.

theorem HSDInteriorPointLP.finiteDimensional_surjective_of_injective_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (L : V →ₗ[ℝ] V) (hinj : Function.Injective ⇑L) : Function.Surjective ⇑L

In a finite-dimensional vector space, an injective linear self-map is surjective.

theorem HSDInteriorPointLP.HLPNullDirection_from_full_nullspace {m n : ℕ} (P : LPData m n) (D : HLPFullDirection m n) (hnull : HLPNullspaceEquations P D) : HLPNullDirection D.toHSDirection

The concrete HLP nullspace equations imply the reduced skew-operator nullspace condition. This is the explicit place where the skew-symmetry of the YTM HLP coefficient matrix must be formalized.

Schur-complement form of the homogeneous Newton-kernel proof

The following small definitions and lemmas make the proof of HLP_newton_block_kernel_trivial_from_full_row_rank follow the standard Newton matrix argument: eliminate (ds, dκ) by the positive diagonal complementarity block, form the Schur complement in (dy, dτ, dθ), first prove the Schur residual and dτ vanish, and only then remove the remaining multiplier variables.

def HSDInteriorPointLP.HLPSchurResidual {m n : ℕ} (P : LPData m n) (D : HLPFullDirection m n) : Vec n

The Schur-complement residual r = Aᵀ dy - c dτ + cbar dθ. In the homogeneous dual block we have ds = -r.

Equations

• HSDInteriorPointLP.HLPSchurResidual P D j = HSDInteriorPointLP.tMatVec P.A D.dy j - P.c j * D.dtau + HSDInteriorPointLP.cbar P j * D.dtheta

noncomputable def HSDInteriorPointLP.HLPThetaDiag {n : ℕ} (w : HSState n) : Vec n

The positive diagonal ratio Θ = S^{-1}X, written componentwise.

Equations

• HSDInteriorPointLP.HLPThetaDiag w j = w.x j / w.s j

theorem HSDInteriorPointLP.HLPHomogeneous.ds_eq_neg_schurResidual {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hD : HLPNewtonHomogeneousBlockSystem P w D) (j : Fin n) : D.ds j = -HLPSchurResidual P D j

The homogeneous dual block gives ds = -r.

theorem HSDInteriorPointLP.HLPHomogeneous.dkappa_eq_neg_ratio_dtau {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hw : Interior w) (hD : HLPNewtonHomogeneousBlockSystem P w D) : D.dkappa = -(w.kappa / w.tau) * D.dtau

The scalar complementarity block eliminates dκ.

theorem HSDInteriorPointLP.HLPHomogeneous.dx_eq_theta_mul_schurResidual {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hw : Interior w) (hD : HLPNewtonHomogeneousBlockSystem P w D) (j : Fin n) : D.dx j = HLPThetaDiag w j * HLPSchurResidual P D j

The complementarity block and the eliminated dual slack give dx = Θ r, the usual first step in forming the Schur complement.

theorem HSDInteriorPointLP.HLPHomogeneous.schur_complementarity_identity {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hw : Interior w) (hD : HLPNewtonHomogeneousBlockSystem P w D) : ∑ j : Fin n, HLPThetaDiag w j * HLPSchurResidual P D j ^ 2 + w.kappa / w.tau * D.dtau ^ 2 = 0

Schur-complement complementarity identity.

After eliminating ds, dx, and dκ through the positive diagonal complementarity block, the homogeneous HLP orthogonality relation becomes ∑ᵢ (xᵢ/sᵢ) rᵢ² + (κ/τ) dτ² = 0. This is the finite-dimensional inner-product identity used in the standard interior-point nonsingularity argument.

theorem HSDInteriorPointLP.finite_sum_pos_sq_plus_pos_sq_eq_zero {n : ℕ} (theta r : Vec n) (eta t : ℝ) (htheta : ∀ (j : Fin n), 0 < theta j) (heta : 0 < eta) (h : ∑ j : Fin n, theta j * r j ^ 2 + eta * t ^ 2 = 0) : (∀ (j : Fin n), r j = 0) ∧ t = 0

A finite-dimensional positivity lemma for the reduced complementarity form.

If all diagonal Schur weights are strictly positive and eta > 0, then the identity ∑ᵢ thetaᵢ rᵢ² + eta t² = 0 forces every residual component rᵢ and the scalar t to vanish. This is the positive-diagonal part of the interior-point nonsingularity argument, rather than positive-definiteness of the whole (dy, dτ, dθ) Schur matrix.

theorem HSDInteriorPointLP.HLPHomogeneous.schur_residual_zero_and_dtau_zero {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hw : Interior w) (hD : HLPNewtonHomogeneousBlockSystem P w D) : (∀ (j : Fin n), HLPSchurResidual P D j = 0) ∧ D.dtau = 0

The reduced complementarity identity forces the Schur residual and dτ to be zero.

theorem HSDInteriorPointLP.HLPHomogeneous.dx_dkappa_ds_zero_from_schur_core {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (hw : Interior w) (hD : HLPNewtonHomogeneousBlockSystem P w D) (hr : ∀ (j : Fin n), HLPSchurResidual P D j = 0) (hdtau : D.dtau = 0) : (∀ (j : Fin n), D.dx j = 0) ∧ (∀ (j : Fin n), D.ds j = 0) ∧ D.dkappa = 0

Once the Schur residual and dτ vanish, the reduced primal and scalar directions vanish.

theorem HSDInteriorPointLP.HLPHomogeneous.dtheta_dy_zero_from_schur_core {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (w : HSState n) (D : HLPFullDirection m n) (hD : HLPNewtonHomogeneousBlockSystem P w D) (hr : ∀ (j : Fin n), HLPSchurResidual P D j = 0) (hdtau : D.dtau = 0) (hdx : ∀ (j : Fin n), D.dx j = 0) (hdkappa : D.dkappa = 0) : D.dtheta = 0 ∧ ∀ (i : Fin m), D.dy i = 0

Final algebra after the Schur core has vanished: the definitions of bbar, cbar, and zbar imply dθ = 0; then full row rank gives dy = 0.

theorem HSDInteriorPointLP.HLP_newton_block_kernel_trivial_from_full_row_rank {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (w : HSState n) (hw : Interior w) (D : HLPFullDirection m n) : HLPNewtonHomogeneousBlockSystem P w D → (∀ (i : Fin n), D.dx i = 0) ∧ D.dtau = 0 ∧ (∀ (i : Fin n), D.ds i = 0) ∧ D.dkappa = 0 ∧ (∀ (i : Fin m), D.dy i = 0) ∧ D.dtheta = 0

Kernel triviality of the full HLP Newton block operator.

This is the part where the proof should use:

• full row rank of A,
• strict positivity of x, tau, s, and kappa,
• the skew-symmetric HLP block identities.

Mathematically, one first eliminates ds and dκ using the complementarity blocks. With r = Aᵀdy - c dτ + cbar dθ, this gives dx = Θ r, where Θ = S^{-1}X is positive diagonal. The Schur-complement identity is then ∑ᵢ Θᵢ rᵢ² + (κ/τ)dτ² = 0, so r = 0 and dτ = 0. The remaining HLP equations, together with the definitions of bbar, cbar, and zbar, give dθ = 0, and full row rank removes dy.

theorem HSDInteriorPointLP.HLP_newton_block_system_solvable_from_kernel_trivial {m n : ℕ} (P : LPData m n) (w : HSState n) (γ : ℝ) (hker : ∀ (D : HLPFullDirection m n), HLPNewtonHomogeneousBlockSystem P w D → (∀ (i : Fin n), D.dx i = 0) ∧ D.dtau = 0 ∧ (∀ (i : Fin n), D.ds i = 0) ∧ D.dkappa = 0 ∧ (∀ (i : Fin m), D.dy i = 0) ∧ D.dtheta = 0) : ∃ (D : HLPFullDirection m n), HLPNewtonBlockSystem P w D γ

Finite-dimensional square linear systems: zero kernel implies solvability.

The HLP Newton block system is square. Once the homogeneous block operator has trivial kernel, finite-dimensional linear algebra gives surjectivity, hence existence of a solution for the inhomogeneous Newton right-hand side.

theorem HSDInteriorPointLP.HLP_newton_block_system_solvable_from_full_row_rank {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (w : HSState n) (hw : Interior w) (γ : ℝ) : ∃ (D : HLPFullDirection m n), HLPNewtonBlockSystem P w D γ

Concrete nonsingularity/surjectivity statement for the full HLP Newton block system. This is now the only finite-dimensional linear-algebra theorem that remains for search-direction existence.

Mathematically, this is proved by eliminating ds and dκ with the positive diagonal coefficients xᵢ and τ, and then using full row rank of A together with the self-dual/skew-symmetric HLP block structure.

theorem HSDInteriorPointLP.reduced_direction_equation_from_full {m n : ℕ} (P : LPData m n) (w : HSState n) (D : HLPFullDirection m n) (γ : ℝ) (hD : HLPFullDirectionEquation P w D γ) : HSDDirectionEquation w D.toHSDirection γ

A full HLP direction equation gives the reduced direction equation used by the rest of the proof skeleton.

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

Concrete full HLP Newton linear-algebra theorem.

This is stronger and more explicit than the reduced HLPNewtonLinearAlgebra: it states solvability of the full YTM direction system containing dy and dθ. The proof should use the full-row-rank assumption on A and the positive diagonal terms from the interior iterate.

• full_direction_system_solvable : LPStandardAssumptions P → ∀ (w : HSState n), Interior w → ∀ (γ : ℝ), ∃ (D : HLPFullDirection m n), HLPFullDirectionEquation P w D γ

theorem HSDInteriorPointLP.HLP_full_newton_linear_algebra_from_full_row_rank {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) : HLPFullNewtonLinearAlgebra P

Main concrete Newton solvability obligation for the YTM HLP system.

theorem HSDInteriorPointLP.aggregate_eq_from_component_eq {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) (hcomp : ∀ (i : Fin n), w.x i * d.ds i + w.s i * d.dx i = γ * mu w - w.x i * w.s i) (hscalar : w.tau * d.dkappa + w.kappa * d.dtau = γ * mu w - w.tau * w.kappa) : hdot w.x w.tau d.ds d.dkappa + hdot d.dx d.dtau w.s w.kappa = -(1 - γ) * gap w

Summing the componentwise complementarity equations, including the scalar τκ equation, gives the aggregate first-order gap identity.

theorem HSDInteriorPointLP.skew_orthogonal_from_HLP_nullspace {n : ℕ} (d : HSDirection n) (hQ : HLPNullDirection d) : HSDSkewOrthogonal d

The skew-symmetry consequence is derived from the bundled HLP nullspace relation. This is the separated-variable version of Theorem 5(ii) in YTM.

theorem HSDInteriorPointLP.complementarity_direction_from_equation {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) (heq : HSDDirectionEquation w d γ) : HSDComplementarityDirection w d γ

The componentwise search-direction equation implies the aggregate complementarity equation.

theorem HSDInteriorPointLP.step_direction_from_direction_equation {n : ℕ} (w : HSState n) (d : HSDirection n) (γ : ℝ) (heq : HSDDirectionEquation w d γ) : HSDStepDirection w d γ

A solution of the HLP search-direction system gives a valid step direction.

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

Linear-algebra theorem needed for the YTM/HLP Newton system.

This packages the remaining finite-dimensional linear-algebra task: from the concrete HLP Newton matrix and the full-row-rank assumption on A, one proves that the predictor/corrector direction equations are solvable at every interior iterate.

The theorem is kept as an explicit field rather than hidden inside the algorithm. In a later file, this should be replaced by an actual matrix nonsingularity proof.

• direction_system_solvable : LPStandardAssumptions P → ∀ (w : HSState n), Interior w → ∀ (γ : ℝ), ∃ (d : HSDirection n), HSDDirectionEquation w d γ

theorem HSDInteriorPointLP.reduced_newton_linear_algebra_from_full {m n : ℕ} (P : LPData m n) (fullAlg : HLPFullNewtonLinearAlgebra P) : HLPNewtonLinearAlgebra P

The concrete full Newton linear algebra induces the reduced linear algebra used by the existing convergence skeleton.

theorem HSDInteriorPointLP.HLP_newton_linear_algebra_from_full_row_rank {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) : HLPNewtonLinearAlgebra P

Main finite-dimensional linear-algebra obligation for the HLP Newton system.

This is the place where the full-row-rank assumption on A should be used to prove that the concrete Ye--Todd--Mizuno Newton system has a solution at each interior iterate. The current skeleton routes this obligation through the explicit full-system solvability statement above.

structure HSDInteriorPointLP.HLPDirectionSystemSolvable {n : ℕ} (w : HSState n) (γ : ℝ) : Prop

Solvability of the YTM/HLP Newton system at a given point and parameter.

• exists_direction : ∃ (d : HSDirection n), HSDDirectionEquation w d γ

theorem HSDInteriorPointLP.direction_system_solvable_from_full_row_rank {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (linAlg : HLPNewtonLinearAlgebra P) (w : HSState n) (hw : Interior w) (γ : ℝ) : HLPDirectionSystemSolvable w γ

Full-row-rank linear algebra supplies a solution of the search-direction system.

theorem HSDInteriorPointLP.search_direction_exists_from_HLP_solvability {n : ℕ} (w : HSState n) (γ : ℝ) (hsolv : HLPDirectionSystemSolvable w γ) : ∃ (d : HSDirection n), HSDDirectionEquation w d γ

Once solvability of the HLP Newton system is available, existence of a search direction is immediate.

noncomputable def HSDInteriorPointLP.chooseSearchDirection {n : ℕ} (w : HSState n) (γ : ℝ) (hex : ∃ (d : HSDirection n), HSDDirectionEquation w d γ) : HSDirection n

A noncomputable selector for the search direction once existence is known.

Equations

• HSDInteriorPointLP.chooseSearchDirection w γ hex = Classical.choose hex

theorem HSDInteriorPointLP.chooseSearchDirection_spec {n : ℕ} (w : HSState n) (γ : ℝ) (hex : ∃ (d : HSDirection n), HSDDirectionEquation w d γ) : HSDDirectionEquation w (chooseSearchDirection w γ hex) γ

The selected search direction satisfies the search-direction equations.

theorem HSDInteriorPointLP.chosen_step_direction {n : ℕ} (w : HSState n) (γ : ℝ) (hex : ∃ (d : HSDirection n), HSDDirectionEquation w d γ) : HSDStepDirection w (chooseSearchDirection w γ hex) γ

The selected search direction is a valid step direction.

theorem HSDInteriorPointLP.sum_mul_add_smul {n : ℕ} (u v dv : Vec n) (α : ℝ) : ∑ i : Fin n, u i * (v i + α * dv i) = ∑ i : Fin n, u i * v i + α * ∑ i : Fin n, u i * dv i

Linearity of a finite sum with respect to the update v + α dv.

theorem HSDInteriorPointLP.dot_add_smul {n : ℕ} (u v dv : Vec n) (α : ℝ) : (dot u fun (i : Fin n) => v i + α * dv i) = dot u v + α * dot u dv

Linearity of the second argument of dot for the update v + α dv.

theorem HSDInteriorPointLP.dot_comm {n : ℕ} (u v : Vec n) : dot u v = dot v u

theorem HSDInteriorPointLP.dot_add_smul_left {n : ℕ} (u du v : Vec n) (α : ℝ) : dot (fun (i : Fin n) => u i + α * du i) v = dot u v + α * dot du v

Linearity of the first argument of dot for the update u + α du.

theorem HSDInteriorPointLP.dot_pair_add_smul {n : ℕ} (u v du dv : Vec n) (α : ℝ) : (dot (fun (i : Fin n) => u i + α * du i) fun (i : Fin n) => v i + α * dv i) = dot u v + α * (dot du v + dot u dv) + α ^ 2 * dot du dv

Expansion of dot (u + α du) (v + α dv).

theorem HSDInteriorPointLP.gap_addStep_expansion {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) : gap (addStep w d α) = gap w + α * (hdot w.x w.tau d.ds d.dkappa + hdot d.dx d.dtau w.s w.kappa) + α ^ 2 * hdot d.dx d.dtau d.ds d.dkappa

Algebraic expansion of the complementarity gap under a line step.

theorem HSDInteriorPointLP.gap_addStep_of_HSDStepDirection {n : ℕ} (w : HSState n) (d : HSDirection n) (α γ : ℝ) (hdir : HSDStepDirection w d γ) : gap (addStep w d α) = (1 - α * (1 - γ)) * gap w

Gap update for a direction satisfying the HLP nullspace and complementarity equations.

structure HSDInteriorPointLP.PredictorStepGuarantee {n : ℕ} (βwide c : ℝ) (w : HSState n) (d : HSDirection n) (α : ℝ) : Prop

Predictor step guarantee from the Mizuno--Todd--Ye local analysis.

• alpha_pos : 0 < α
• alpha_le_one : α ≤ 1
• interior_next : Interior (addStep w d α)
• neighborhood_next : HSDNeighborhood βwide (addStep w d α)
• gap_decrease : gap (addStep w d α) ≤ (1 - c / √(hdim n)) * gap w

structure HSDInteriorPointLP.CorrectorStepGuarantee {n : ℕ} (βtight : ℝ) (w : HSState n) (d : HSDirection n) : Prop

Corrector step guarantee from the Mizuno--Todd--Ye local analysis.

• interior_next : Interior (addStep w d 1)
• neighborhood_next : HSDNeighborhood βtight (addStep w d 1)
• gap_preserve : gap (addStep w d 1) = gap w

noncomputable def HSDInteriorPointLP.ytmBetaTight : ℝ

The tight neighborhood parameter used in the YTM proof.

Equations

• HSDInteriorPointLP.ytmBetaTight = 1 / 4

noncomputable def HSDInteriorPointLP.ytmBetaWide : ℝ

The wide neighborhood parameter used in the YTM proof.

Equations

• HSDInteriorPointLP.ytmBetaWide = 1 / 2

noncomputable def HSDInteriorPointLP.ytmStepConstant : ℝ

The predictor step-size constant appearing in YTM Theorem 6. Mathematically this is 8^{-2.5}.

Equations

• HSDInteriorPointLP.ytmStepConstant = 1 / (8 ^ 2 * √8)

Corrector local estimate

The corrector half of the YTM local analysis is a componentwise estimate for the full step. In the usual notation, set

• u = (x, τ) and v = (s, κ),
• Δu = (dx, dτ) and Δv = (ds, dκ),
• N = n + 1 and μ = gap w / N.

For a corrector direction (γ = 1), the linearized complementarity equations give

uᵢ Δvᵢ + vᵢ Δuᵢ = μ - uᵢ vᵢ,

and skew orthogonality gives Σ Δuᵢ Δvᵢ = 0. The Mizuno--Todd--Ye componentwise estimate proves that, if w ∈ N(1/2), then the full corrector step w + d is positive and lies in N(1/4). The proof is the standard scaled estimate

‖Δu ∘ Δv‖ ≤ μ / 4,

obtained by writing pᵢ = Δuᵢ/uᵢ, qᵢ = Δvᵢ/vᵢ, aᵢ = sqrt(uᵢvᵢ) pᵢ, and bᵢ = sqrt(uᵢvᵢ) qᵢ. This lemma is stated separately so that the top-level corrector theorem has exactly the same shape as the IPM proof: local positivity/centrality estimate plus the already-formalized gap identity.