Fixed local neighborhood estimates

This file contains the local predictor/corrector estimates that are considered fixed. It should be edited only when the mathematical local estimates themselves change.

Naming convention: this refactor uses YTM consistently. In this development, YTM refers to the Ye--Todd--Mizuno homogeneous LP / neighborhood framework used by the proof. Earlier mixed alternative abbreviations in comments and identifiers have been renamed to avoid two names for the same local-estimate layer.

Lean-reading hints for beginners:

• linarith proves goals from linear equalities/inequalities over ordered rings.
• nlinarith is the nonlinear version; it can use products and squares.
• ring proves polynomial identities such as rearrangements of sums/products.
• field_simp clears denominators after you provide nonzero-denominator proofs.

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 YTM local estimates, refactored

This file keeps only the active local estimates needed by the current skeleton. The imported core file contains the HLP block operator, Schur-complement complementarity arguments, and all warning-clean fixed lemmas.

Corrector-side algebra already derivable from the HSD equations

theorem HSDInteriorPointLP.corrector_mu_full_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) : mu (addStep w d 1) = mu w

A full corrector step preserves the homogenized complementarity gap, hence also preserves mu. This is only the gap algebra; the central-neighborhood estimate is handled separately below.

theorem HSDInteriorPointLP.corrector_component_product_full_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) (i : Fin n) : (addStep w d 1).x i * (addStep w d 1).s i = mu w + d.dx i * d.ds i

Product identity for the vector complementarity pairs after a full corrector step.

theorem HSDInteriorPointLP.corrector_scalar_product_full_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) : (addStep w d 1).tau * (addStep w d 1).kappa = mu w + d.dtau * d.dkappa

Product identity for the scalar complementarity pair after a full corrector step.

theorem HSDInteriorPointLP.corrector_centerSq_full_step_eq_cross_sq {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) : centerSq (addStep w d 1).x (addStep w d 1).tau (addStep w d 1).s (addStep w d 1).kappa (mu (addStep w d 1)) = ∑ i : Fin n, (d.dx i * d.ds i) ^ 2 + (d.dtau * d.dkappa) ^ 2

After a full corrector step, the new centrality residual is exactly the squared norm of the second-order complementarity products.

Elementary estimates for the corrector obligation

theorem HSDInteriorPointLP.hdim_pos (n : ℕ) : 0 < hdim n

The homogenized dimension n + 1 is strictly positive.

theorem HSDInteriorPointLP.gap_pos_of_interior {n : ℕ} (w : HSState n) (hinterior : Interior w) : 0 < gap w

Interior points have positive complementarity gap.

theorem HSDInteriorPointLP.mu_pos_of_interior {n : ℕ} (w : HSState n) (hinterior : Interior w) : 0 < mu w

Interior points have positive duality measure.

theorem HSDInteriorPointLP.corrector_second_order_sum_zero {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) : ∑ i : Fin n, d.dx i * d.ds i + d.dtau * d.dkappa = 0

The skew-orthogonality part of a step direction, written as the finite sum of second-order complementarity products.

theorem HSDInteriorPointLP.corrector_component_second_order_upper {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) (i : Fin n) : 4 * (w.x i * w.s i) * (d.dx i * d.ds i) ≤ (mu w - w.x i * w.s i) ^ 2

Componentwise quadratic estimate obtained from the corrector linearized complementarity equation. This is the elementary identity (x Δs - s Δx)^2 = (μ - xs)^2 - 4xs ΔxΔs together with nonnegativity of squares.

theorem HSDInteriorPointLP.corrector_scalar_second_order_upper {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 1) : 4 * (w.tau * w.kappa) * (d.dtau * d.dkappa) ≤ (mu w - w.tau * w.kappa) ^ 2

Scalar analogue of corrector_component_second_order_upper.

theorem HSDInteriorPointLP.neighborhood_centerSq_le {n : ℕ} (β : ℝ) (w : HSState n) (hneigh : HSDNeighborhood β w) : centerSq w.x w.tau w.s w.kappa (mu w) ≤ (β * mu w) ^ 2

Extract the centrality bound from an HSDNeighborhood. Keeping this as a separate lemma prevents later proofs from repeatedly destructing the nested And.

theorem HSDInteriorPointLP.mu_pos_of_neighborhood {n : ℕ} (β : ℝ) (w : HSState n) (hneigh : HSDNeighborhood β w) : 0 < mu w

A point in a central neighborhood has positive mu.

theorem HSDInteriorPointLP.neighborhood_component_dev_sq_le_bound {n : ℕ} (β : ℝ) (w : HSState n) (hneigh : HSDNeighborhood β w) (i : Fin n) : (mu w - w.x i * w.s i) ^ 2 ≤ (β * mu w) ^ 2

Each vector complementarity product has squared deviation bounded by the whole centrality residual.

theorem HSDInteriorPointLP.neighborhood_scalar_dev_sq_le_bound {n : ℕ} (β : ℝ) (w : HSState n) (hneigh : HSDNeighborhood β w) : (mu w - w.tau * w.kappa) ^ 2 ≤ (β * mu w) ^ 2

The scalar complementarity product has squared deviation bounded by the whole centrality residual.

theorem HSDInteriorPointLP.neighborhood_component_product_lower_wide {n : ℕ} (w : HSState n) (hneigh : HSDNeighborhood ytmBetaWide w) (i : Fin n) : mu w / 2 ≤ w.x i * w.s i

In the wide neighborhood, every vector complementarity product is at least mu/2. This keeps the scalar τκ separate from the Fin n sum, as in the separated proof plan.

theorem HSDInteriorPointLP.neighborhood_scalar_product_lower_wide {n : ℕ} (w : HSState n) (hneigh : HSDNeighborhood ytmBetaWide w) : mu w / 2 ≤ w.tau * w.kappa

Scalar analogue of neighborhood_component_product_lower_wide.

noncomputable def HSDInteriorPointLP.posPart (a : ℝ) : ℝ

Positive part used in the YTM corrector estimate. It is deliberately kept as a small elementary definition instead of using an order-theory abstraction.

Equations

• HSDInteriorPointLP.posPart a = if 0 ≤ a then a else 0

theorem HSDInteriorPointLP.abs_eq_two_posPart_sub (a : ℝ) : |a| = 2 * posPart a - a

Absolute value expressed through the positive part. This identity is useful for turning the skew relation Σ δᵢ + η = 0 into an ℓ₁ bound.

theorem HSDInteriorPointLP.corrector_component_posPart_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) (i : Fin n) : posPart (d.dx i * d.ds i) ≤ (mu w - w.x i * w.s i) ^ 2 / (2 * mu w)

The positive part of each vector second-order complementarity product is bounded by the corresponding squared centrality deviation divided by 2 mu. This is the componentwise bridge from the corrector identity to the positive-part summation argument.

theorem HSDInteriorPointLP.corrector_scalar_posPart_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : posPart (d.dtau * d.dkappa) ≤ (mu w - w.tau * w.kappa) ^ 2 / (2 * mu w)

Scalar analogue of corrector_component_posPart_bound.

theorem HSDInteriorPointLP.corrector_positive_part_sum_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : ∑ i : Fin n, posPart (d.dx i * d.ds i) + posPart (d.dtau * d.dkappa) ≤ mu w / 8

Summed positive-part bound, still keeping the vector and scalar pieces separate. This is the key estimate needed before converting the zero-sum relation into an absolute-value bound.

theorem HSDInteriorPointLP.abs_sum_add_abs_eq_two_posPart_sum_of_sum_add_zero {n : ℕ} (a : Fin n → ℝ) (η : ℝ) (hzero : ∑ i : Fin n, a i + η = 0) : ∑ i : Fin n, |a i| + |η| = 2 * (∑ i : Fin n, posPart (a i) + posPart η)

If a finite family together with one scalar has zero total sum, then the sum of absolute values is twice the sum of positive parts.

theorem HSDInteriorPointLP.corrector_cross_l1_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : ∑ i : Fin n, |d.dx i * d.ds i| + |d.dtau * d.dkappa| ≤ mu w / 4

The positive-part bound plus zero-sum relation gives an ℓ₁ bound for the second-order complementarity products.

theorem HSDInteriorPointLP.sum_sq_add_sq_le_l1_sq {n : ℕ} (a : Fin n → ℝ) (η : ℝ) : ∑ i : Fin n, a i ^ 2 + η ^ 2 ≤ (∑ i : Fin n, |a i| + |η|) ^ 2

A square-sum is bounded by the square of the corresponding ℓ₁ norm. The scalar term is kept separate from the Fin n sum to match the HSDE notation.

theorem HSDInteriorPointLP.corrector_cross_sq_sum_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : ∑ i : Fin n, (d.dx i * d.ds i) ^ 2 + (d.dtau * d.dkappa) ^ 2 ≤ (mu w / 4) ^ 2

The ℓ₁ bound implies the YTM square-sum bound for the corrector products.

theorem HSDInteriorPointLP.corrector_component_cross_abs_le_quarter_mu {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) (i : Fin n) : |d.dx i * d.ds i| ≤ mu w / 4

Each vector second-order product is individually bounded by mu/4 in absolute value.

theorem HSDInteriorPointLP.corrector_scalar_cross_abs_le_quarter_mu {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : |d.dtau * d.dkappa| ≤ mu w / 4

The scalar second-order product is individually bounded by mu/4 in absolute value.

theorem HSDInteriorPointLP.factors_pos_of_mul_pos_and_weighted_sum_pos {a b wa wb : ℝ} (hwa : 0 < wa) (hwb : 0 < wb) (hmul : 0 < a * b) (hsum : 0 < wb * a + wa * b) : 0 < a ∧ 0 < b

If two factors have positive product and a positive weighted sum with positive weights, then both factors are positive.

theorem HSDInteriorPointLP.corrector_component_pair_pos_full_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) (i : Fin n) : 0 < (addStep w d 1).x i ∧ 0 < (addStep w d 1).s i

Positivity of each vector pair after the full corrector step.

theorem HSDInteriorPointLP.corrector_scalar_pair_pos_full_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : 0 < (addStep w d 1).tau ∧ 0 < (addStep w d 1).kappa

Positivity of the scalar pair after the full corrector step.

theorem HSDInteriorPointLP.corrector_full_step_interior {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : Interior (addStep w d 1)

The full corrector step remains in the positive orthant.

theorem HSDInteriorPointLP.YTM_corrector_scaled_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaWide w → HSDStepDirection w d 1 → Interior (addStep w d 1) ∧ ∑ i : Fin n, (d.dx i * d.ds i) ^ 2 + (d.dtau * d.dkappa) ^ 2 ≤ (ytmBetaTight * mu w) ^ 2

Scaled YTM corrector estimate for the second-order complementarity products.

This is the single genuinely analytic ingredient in the corrector half. In the usual notation put

• u = (x, τ), v = (s, κ),
• Δu = (dx, dτ), Δv = (ds, dκ),
• zᵢ = uᵢ vᵢ, μ = (Σ zᵢ)/(n+1).

For a corrector direction, the linearized complementarity equations give

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

and skew orthogonality gives

Σ Δuᵢ Δvᵢ = 0.

The standard YTM argument sets pᵢ = Δuᵢ/uᵢ and qᵢ = Δvᵢ/vᵢ. Then pᵢ + qᵢ = μ/zᵢ - 1, while Σ zᵢ pᵢqᵢ = 0. Since w ∈ N(1/2), each zᵢ is within μ/2 of μ; this bounds the positive part of zᵢ pᵢqᵢ by the squared centrality residual. Hence all full-step products stay positive and

Σ (Δuᵢ Δvᵢ)^2 ≤ (μ/4)^2.

The rest of the Lean file has already reduced the corrector theorem to exactly this statement. This lemma is intentionally isolated so that the remaining paper estimate is no longer mixed with the bookkeeping around centerSq and mu.

theorem HSDInteriorPointLP.YTM_corrector_interior_and_center_bound {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaWide w → HSDStepDirection w d 1 → Interior (addStep w d 1) ∧ centerSq (addStep w d 1).x (addStep w d 1).tau (addStep w d 1).s (addStep w d 1).kappa (mu (addStep w d 1)) ≤ (ytmBetaTight * mu (addStep w d 1)) ^ 2

The corrector-side local bound, reduced to the isolated scaled YTM estimate.

Unlike the previous version, this theorem itself no longer contains the paper-level analytic obligation: after YTM_corrector_scaled_estimate, the proof is just the algebraic identities already established above.

theorem HSDInteriorPointLP.YTM_corrector_full_step_local_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaWide w → HSDStepDirection w d 1 → Interior (addStep w d 1) ∧ HSDNeighborhood ytmBetaTight (addStep w d 1)

Corrector full-step local estimate, now reduced to the explicit analytic bound YTM_corrector_interior_and_center_bound; no placeholder remains in this wrapper.

Predictor-side elementary step-size and product identities

theorem HSDInteriorPointLP.ytmStepConstant_pos : 0 < ytmStepConstant

The fixed YTM predictor step constant is positive.

theorem HSDInteriorPointLP.ytmStepConstant_le_one : ytmStepConstant ≤ 1

The fixed YTM predictor step constant is at most one.

theorem HSDInteriorPointLP.one_le_hdim (n : ℕ) : 1 ≤ hdim n

The homogenized dimension is at least one.

theorem HSDInteriorPointLP.sqrt_hdim_pos (n : ℕ) : 0 < √(hdim n)

The square root of the homogenized dimension is positive.

theorem HSDInteriorPointLP.one_le_sqrt_hdim (n : ℕ) : 1 ≤ √(hdim n)

The square root of the homogenized dimension is at least one.

theorem HSDInteriorPointLP.predictor_alpha_fixed_pos (n : ℕ) : 0 < ytmStepConstant / √(hdim n)

Positivity of the fixed predictor step length.

theorem HSDInteriorPointLP.predictor_alpha_fixed_le_one (n : ℕ) : ytmStepConstant / √(hdim n) ≤ 1

The fixed predictor step length is at most one.

theorem HSDInteriorPointLP.predictor_mu_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) : mu (addStep w d α) = (1 - α) * mu w

Predictor step formula for mu. For γ = 0, the homogenized gap and hence mu are multiplied by 1 - α.

theorem HSDInteriorPointLP.predictor_component_product_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) (i : Fin n) : (addStep w d α).x i * (addStep w d α).s i = (1 - α) * (w.x i * w.s i) + α ^ 2 * (d.dx i * d.ds i)

Predictor product identity for each vector complementarity pair.

theorem HSDInteriorPointLP.predictor_scalar_product_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) : (addStep w d α).tau * (addStep w d α).kappa = (1 - α) * (w.tau * w.kappa) + α ^ 2 * (d.dtau * d.dkappa)

Predictor product identity for the scalar complementarity pair.

Predictor positivity bookkeeping

theorem HSDInteriorPointLP.predictor_component_weighted_sum_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) (i : Fin n) : w.s i * (addStep w d α).x i + w.x i * (addStep w d α).s i = (2 - α) * (w.x i * w.s i)

Predictor weighted-sum identity for each vector pair.

Together with positivity of the product after the step, this identity lets us recover positivity of each individual factor. This is useful because the remaining YTM estimate naturally controls the products.

theorem HSDInteriorPointLP.predictor_scalar_weighted_sum_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) : w.kappa * (addStep w d α).tau + w.tau * (addStep w d α).kappa = (2 - α) * (w.tau * w.kappa)

Predictor weighted-sum identity for the scalar pair.

theorem HSDInteriorPointLP.predictor_component_pair_pos_of_product_pos {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) (hαle : α ≤ 1) (i : Fin n) (hprod : 0 < (addStep w d α).x i * (addStep w d α).s i) : 0 < (addStep w d α).x i ∧ 0 < (addStep w d α).s i

If the predictor step keeps the product of one vector complementarity pair positive, then the two factors themselves are positive.

theorem HSDInteriorPointLP.predictor_scalar_pair_pos_of_product_pos {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) (hαle : α ≤ 1) (hprod : 0 < (addStep w d α).tau * (addStep w d α).kappa) : 0 < (addStep w d α).tau ∧ 0 < (addStep w d α).kappa

Scalar analogue of predictor_component_pair_pos_of_product_pos.

theorem HSDInteriorPointLP.predictor_step_interior_of_product_pos {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) (hαle : α ≤ 1) (hprod_vec : ∀ (i : Fin n), 0 < (addStep w d α).x i * (addStep w d α).s i) (hprod_scalar : 0 < (addStep w d α).tau * (addStep w d α).kappa) : Interior (addStep w d α)

Product positivity for all complementarity pairs implies that the predictor step stays in the interior.

theorem HSDInteriorPointLP.predictor_component_center_residual_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) (i : Fin n) : (addStep w d α).x i * (addStep w d α).s i - mu (addStep w d α) = (1 - α) * (w.x i * w.s i - mu w) + α ^ 2 * (d.dx i * d.ds i)

Predictor residual identity for each vector complementarity pair. This is the main bookkeeping formula needed for the remaining neighborhood estimate: the new centrality residual is the old residual contracted by 1 - α, plus the second-order predictor product.

theorem HSDInteriorPointLP.predictor_scalar_center_residual_step {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) : (addStep w d α).tau * (addStep w d α).kappa - mu (addStep w d α) = (1 - α) * (w.tau * w.kappa - mu w) + α ^ 2 * (d.dtau * d.dkappa)

Scalar version of the predictor residual identity.

theorem HSDInteriorPointLP.predictor_centerSq_step_eq {n : ℕ} (w : HSState n) (d : HSDirection n) (α : ℝ) (hdir : HSDStepDirection w d 0) : centerSq (addStep w d α).x (addStep w d α).tau (addStep w d α).s (addStep w d α).kappa (mu (addStep w d α)) = ∑ i : Fin n, ((1 - α) * (w.x i * w.s i - mu w) + α ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - α) * (w.tau * w.kappa - mu w) + α ^ 2 * (d.dtau * d.dkappa)) ^ 2

Exact expansion of the predictor centrality residual after an arbitrary predictor step. No estimate is used here; this only isolates the expression that has to be bounded in the remaining YTM predictor argument.

theorem HSDInteriorPointLP.predictor_fixed_mu_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) : mu (addStep w d (ytmStepConstant / √(hdim n))) = (1 - ytmStepConstant / √(hdim n)) * mu w

Fixed-step specialization of predictor_mu_step.

theorem HSDInteriorPointLP.predictor_fixed_component_product_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) (i : Fin n) : (addStep w d (ytmStepConstant / √(hdim n))).x i * (addStep w d (ytmStepConstant / √(hdim n))).s i = (1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)

Fixed-step specialization of the vector predictor product identity.

theorem HSDInteriorPointLP.predictor_fixed_scalar_product_step {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) : (addStep w d (ytmStepConstant / √(hdim n))).tau * (addStep w d (ytmStepConstant / √(hdim n))).kappa = (1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)

Fixed-step specialization of the scalar predictor product identity.

theorem HSDInteriorPointLP.predictor_fixed_centerSq_step_eq {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) : centerSq (addStep w d (ytmStepConstant / √(hdim n))).x (addStep w d (ytmStepConstant / √(hdim n))).tau (addStep w d (ytmStepConstant / √(hdim n))).s (addStep w d (ytmStepConstant / √(hdim n))).kappa (mu (addStep w d (ytmStepConstant / √(hdim n)))) = ∑ i : Fin n, ((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) ^ 2

Fixed-step specialization of the exact predictor centrality-residual expansion.

structure HSDInteriorPointLP.YTMFixedLocalTheory (n : ℕ) : Prop

Fixed-parameter YTM local theory.

This version matches the proof in Ye--Todd--Mizuno: predictor moves from the 1/4 neighborhood to the 1/2 neighborhood with a step of order 8^{-2.5}/sqrt(n+1), while corrector moves from the 1/2 neighborhood back to 1/4 using the full step.

• predictor_estimate_fixed (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → ∃ (α : ℝ), PredictorStepGuarantee ytmBetaWide ytmStepConstant w d α
• corrector_estimate_fixed (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaWide w → HSDStepDirection w d 1 → CorrectorStepGuarantee ytmBetaTight w d

structure HSDInteriorPointLP.YTMPredictorEstimate (n : ℕ) : Prop

Predictor estimate used in the YTM proof.

This packages the two ingredients of the predictor half of Theorem 6: starting from the tight neighborhood N(1/4), the predictor direction with γ = 0 has a step of length at least ytmStepConstant / sqrt(n+1) and the resulting point remains in the wide neighborhood N(1/2) with the corresponding gap decrease.

• estimate (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → ∃ (α : ℝ), PredictorStepGuarantee ytmBetaWide ytmStepConstant w d α

theorem HSDInteriorPointLP.predictor_fixed_component_product_pos_of_cross_lower {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) (hcross : ∀ (i : Fin n), -((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) (i : Fin n) : 0 < (addStep w d (ytmStepConstant / √(hdim n))).x i * (addStep w d (ytmStepConstant / √(hdim n))).s i

A lower bound on the second-order predictor products implies positivity of all fixed-step vector complementarity products. This is purely algebraic: the product identity says x⁺ᵢs⁺ᵢ = (1 - α) xᵢsᵢ + α² ΔxᵢΔsᵢ.

theorem HSDInteriorPointLP.predictor_fixed_scalar_product_pos_of_cross_lower {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) (hcross : -((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) : 0 < (addStep w d (ytmStepConstant / √(hdim n))).tau * (addStep w d (ytmStepConstant / √(hdim n))).kappa

Scalar analogue of predictor_fixed_component_product_pos_of_cross_lower.

theorem HSDInteriorPointLP.predictor_fixed_component_cross_lower_of_step_product_pos {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) (i : Fin n) (hprod : 0 < (addStep w d (ytmStepConstant / √(hdim n))).x i * (addStep w d (ytmStepConstant / √(hdim n))).s i) : -((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)

If the fixed predictor step keeps both factors of a vector pair positive, then its second-order product cannot cancel the first-order complementarity product.

theorem HSDInteriorPointLP.predictor_fixed_scalar_cross_lower_of_step_product_pos {n : ℕ} (w : HSState n) (d : HSDirection n) (hdir : HSDStepDirection w d 0) (hprod : 0 < (addStep w d (ytmStepConstant / √(hdim n))).tau * (addStep w d (ytmStepConstant / √(hdim n))).kappa) : -((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)

Scalar analogue of predictor_fixed_component_cross_lower_of_step_product_pos.

theorem HSDInteriorPointLP.predictor_fixed_component_product_pos_of_relative_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (i : Fin n) (hxrel : |ytmStepConstant / √(hdim n) * d.dx i| < w.x i) (hsrel : |ytmStepConstant / √(hdim n) * d.ds i| < w.s i) : 0 < (addStep w d (ytmStepConstant / √(hdim n))).x i * (addStep w d (ytmStepConstant / √(hdim n))).s i

Relative componentwise bounds imply positivity of a vector complementarity product after the fixed predictor step.

theorem HSDInteriorPointLP.predictor_fixed_scalar_product_pos_of_relative_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (htrel : |ytmStepConstant / √(hdim n) * d.dtau| < w.tau) (hkrel : |ytmStepConstant / √(hdim n) * d.dkappa| < w.kappa) : 0 < (addStep w d (ytmStepConstant / √(hdim n))).tau * (addStep w d (ytmStepConstant / √(hdim n))).kappa

Scalar analogue of predictor_fixed_component_product_pos_of_relative_bounds.

theorem HSDInteriorPointLP.abs_step_lt_of_scaled_abs_lt_one (x a α : ℝ) (hx : 0 < x) (hscaled : |α * (a / x)| < 1) : |α * a| < x

Elementary conversion from a scaled relative bound to an unscaled relative bound.

Fixed predictor scaled residual notation

The last remaining predictor estimate is easier to read if the fixed step length, the scaled direction components, and the explicit post-predictor centrality residual are named. These definitions do not add new assumptions; they are just abbreviations for the formulas already used in PredictorFixedScaledNormBounds.

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorFixedAlpha (n : ℕ) : ℝ

The fixed predictor step length used in the YTM local analysis.

Equations

• HSDInteriorPointLP.predictorFixedAlpha n = HSDInteriorPointLP.ytmStepConstant / √(HSDInteriorPointLP.hdim n)

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorScaledDx {n : ℕ} (w : HSState n) (d : HSDirection n) (i : Fin n) : ℝ

Scaled x-direction component multiplied by the fixed predictor step.

Equations

• HSDInteriorPointLP.predictorScaledDx w d i = HSDInteriorPointLP.predictorFixedAlpha n * (d.dx i / w.x i)

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorScaledDs {n : ℕ} (w : HSState n) (d : HSDirection n) (i : Fin n) : ℝ

Scaled s-direction component multiplied by the fixed predictor step.

Equations

• HSDInteriorPointLP.predictorScaledDs w d i = HSDInteriorPointLP.predictorFixedAlpha n * (d.ds i / w.s i)

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorScaledDtau {n : ℕ} (w : HSState n) (d : HSDirection n) : ℝ

Scaled tau-direction component multiplied by the fixed predictor step.

Equations

• HSDInteriorPointLP.predictorScaledDtau w d = HSDInteriorPointLP.predictorFixedAlpha n * (d.dtau / w.tau)

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorScaledDkappa {n : ℕ} (w : HSState n) (d : HSDirection n) : ℝ

Scaled kappa-direction component multiplied by the fixed predictor step.

Equations

• HSDInteriorPointLP.predictorScaledDkappa w d = HSDInteriorPointLP.predictorFixedAlpha n * (d.dkappa / w.kappa)

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorVecResidualAfter {n : ℕ} (w : HSState n) (d : HSDirection n) (i : Fin n) : ℝ

Explicit vector residual after substituting the predictor product identity.

Equations

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

@[reducible, inline]

noncomputable abbrev HSDInteriorPointLP.predictorScalarResidualAfter {n : ℕ} (w : HSState n) (d : HSDirection n) : ℝ

Explicit scalar residual after substituting the predictor product identity.

Equations

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

structure HSDInteriorPointLP.PredictorFixedScaledCoreBounds {n : ℕ} (w : HSState n) (d : HSDirection n) : Prop

Core form of the remaining fixed-step YTM estimate.

Compared with PredictorFixedScaledNormBounds, this version uses named scaled variables and named residuals. Thus the final predictor obligation is precisely the mathematical YTM estimate, rather than a long expanded expression.

• scaled_vec (i : Fin n) : |predictorScaledDx w d i| < 1 ∧ |predictorScaledDs w d i| < 1
• scaled_tau : |predictorScaledDtau w d| < 1
• scaled_kappa : |predictorScaledDkappa w d| < 1
• center : ∑ i : Fin n, predictorVecResidualAfter w d i ^ 2 + predictorScalarResidualAfter w d ^ 2 ≤ (ytmBetaWide * ((1 - predictorFixedAlpha n) * mu w)) ^ 2

structure HSDInteriorPointLP.PredictorFixedScaledNormBounds {n : ℕ} (w : HSState n) (d : HSDirection n) : Prop

Fixed-step scaled-norm bounds for the predictor direction.

This is the same analytic information as the relative-step formulation below, but written in the natural YTM scaled variables dx/x, ds/s, dtau/tau, and dkappa/kappa. The surrounding lemmas convert these scaled bounds into the unscaled relative inequalities needed for positivity of the step.

• scaled_vec (i : Fin n) : |ytmStepConstant / √(hdim n) * (d.dx i / w.x i)| < 1 ∧ |ytmStepConstant / √(hdim n) * (d.ds i / w.s i)| < 1
• scaled_tau : |ytmStepConstant / √(hdim n) * (d.dtau / w.tau)| < 1
• scaled_kappa : |ytmStepConstant / √(hdim n) * (d.dkappa / w.kappa)| < 1
• center : ∑ i : Fin n, ((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) ^ 2 ≤ (ytmBetaWide * ((1 - ytmStepConstant / √(hdim n)) * mu w)) ^ 2

structure HSDInteriorPointLP.PredictorFixedScaledDirectionBounds {n : ℕ} (w : HSState n) (d : HSDirection n) : Prop

Fixed-step scaled-direction bounds needed in the predictor half of the YTM proof.

This record isolates the genuinely analytic estimate from the surrounding Lean bookkeeping. Its first three fields say that the fixed predictor step is componentwise small relative to the current interior point. The last field is the explicit N(1/2) centrality estimate after substituting the predictor product identities.

• rel_vec (i : Fin n) : |ytmStepConstant / √(hdim n) * d.dx i| < w.x i ∧ |ytmStepConstant / √(hdim n) * d.ds i| < w.s i
• rel_tau : |ytmStepConstant / √(hdim n) * d.dtau| < w.tau
• rel_kappa : |ytmStepConstant / √(hdim n) * d.dkappa| < w.kappa
• center : ∑ i : Fin n, ((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) ^ 2 ≤ (ytmBetaWide * ((1 - ytmStepConstant / √(hdim n)) * mu w)) ^ 2

theorem HSDInteriorPointLP.predictor_fixed_scaled_norm_bounds_to_direction_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hbounds : PredictorFixedScaledNormBounds w d) : PredictorFixedScaledDirectionBounds w d

Convert the natural scaled-norm bounds into the relative-step bounds used in the positivity bookkeeping.

theorem HSDInteriorPointLP.predictor_fixed_scaled_core_to_norm_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (hcore : PredictorFixedScaledCoreBounds w d) : PredictorFixedScaledNormBounds w d

Convert the named core estimate back to the expanded scaled-norm package.