Generated predictor-corrector algorithm and final convergence theorem

This is the main file to edit when the algorithmic proof changes. The iterate sequence is generated recursively from the initial point, so the dependency on the fixed YTM theory is explicit and there is no hidden import of an old numbered file.

Lean-reading hints for beginners:

• induction k with | zero => ... | succ k ih => ... proves a statement for all natural numbers by proving the base case and the successor case.
• calc ... is a readable chain of equalities/inequalities.
• omega solves arithmetic goals over natural numbers and integers.

Lean comments for readers who know interior-point methods

This file is the final iteration-count layer. The mathematical objects are the predictor point, the corrector point, and the contraction estimate for the homogenized gap. A few Lean proof commands occur repeatedly.

• intro k introduces the iteration index in a theorem whose conclusion starts with ∀ k, ....
• induction k with ... proves a statement for all natural numbers by showing the base case 0 and then the step from k to k+1.
• have h := ... records an intermediate estimate, such as one-step contraction.
• rw [lemma] rewrites the current goal using an equality.
• simpa [name₁, name₂] using h unfolds the listed definitions, simplifies both sides, and then applies the already-proved fact h.
• simp is used only in very small base cases, such as c^0 = 1.
• ring closes purely algebraic real-number identities.
• linarith and nlinarith are used in imported files for linear and nonlinear real inequalities; here most inequalities are chained explicitly with calc.

structure HSDInteriorPointLP.HSDGeneratedAlgorithm (n : ℕ) : Type

A generated predictor-corrector algorithm: the iterate sequence is no longer a field. It is obtained recursively from the initial point by applying the canonical Newton predictor step and the canonical Newton corrector step.

• m : ℕ

  Number of equality constraints in the LP data.

• P : LPData self.m n

  Linear-programming data.

• std : LPStandardAssumptions self.P

  Standard assumptions on the LP data.

• w0 : HSState n

  Initial HSD state.

• initial_neigh : HSDNeighborhood ytmBetaTight self.w0

  Initial tight-neighborhood certificate.

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.predictorStep {n : ℕ} (alg : HSDGeneratedAlgorithm n) (w : HSState n) (h : HSDNeighborhood ytmBetaTight w) : HSState n

Canonical fixed predictor step from a tight-neighborhood point.

Equations

• alg.predictorStep w h = HSDInteriorPointLP.addStep w (HSDInteriorPointLP.HSDNewtonDirection alg.P ⋯ w ⋯ 0) (HSDInteriorPointLP.ytmPredictorAlpha n)

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.correctorStep {n : ℕ} (alg : HSDGeneratedAlgorithm n) (w : HSState n) (h : HSDNeighborhood ytmBetaWide w) : HSState n

Canonical full corrector step from a wide-neighborhood point.

Equations

• alg.correctorStep w h = HSDInteriorPointLP.addStep w (HSDInteriorPointLP.HSDNewtonDirection alg.P ⋯ w ⋯ 1) 1

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.predictorStep_wide {n : ℕ} (alg : HSDGeneratedAlgorithm n) (w : HSState n) (h : HSDNeighborhood ytmBetaTight w) : HSDNeighborhood ytmBetaWide (alg.predictorStep w h)

The generated predictor step stays in the wide neighborhood.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.correctorStep_tight {n : ℕ} (alg : HSDGeneratedAlgorithm n) (w : HSState n) (h : HSDNeighborhood ytmBetaWide w) : HSDNeighborhood ytmBetaTight (alg.correctorStep w h)

The generated corrector step returns to the tight neighborhood.

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.evenState {n : ℕ} (alg : HSDGeneratedAlgorithm n) : ℕ → { w : HSState n // HSDNeighborhood ytmBetaTight w }

Even iterates, carrying the proof that they are in the tight neighborhood.

Equations

• alg.evenState 0 = ⟨alg.w0, ⋯⟩
• alg.evenState k.succ = ⟨alg.correctorStep (alg.predictorStep ↑(alg.evenState k) ⋯) ⋯, ⋯⟩

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.even {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : HSState n

The even iterate at predictor-corrector pair k.

Equations

• alg.even k = ↑(alg.evenState k)

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.even_tight {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : HSDNeighborhood ytmBetaTight (alg.even k)

Tight-neighborhood proof for generated even iterates.

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.odd {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : HSState n

The odd iterate obtained after the predictor step from even k.

Equations

• alg.odd k = alg.predictorStep (alg.even k) ⋯

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.odd_wide {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : HSDNeighborhood ytmBetaWide (alg.odd k)

Wide-neighborhood proof for generated odd iterates.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.predictor_gap_decrease {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : gap (alg.odd k) ≤ ytmContraction n * gap (alg.even k)

Predictor gap decrease for generated odd iterates.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.corrector_gap_preserve {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : gap (alg.even (k + 1)) = gap (alg.odd k)

Corrector gap preservation for generated even iterates.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.two_step_gap_contracts {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : gap (alg.even (k + 1)) ≤ ytmContraction n * gap (alg.even k)

One generated predictor-corrector pair contracts the gap.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.initial_gap_pos {n : ℕ} (alg : HSDGeneratedAlgorithm n) : 0 < gap (alg.even 0)

Initial gap positivity is derived from the initial neighborhood.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.even_gap_contracts_pow {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : gap (alg.even k) ≤ ytmContraction n ^ k * gap (alg.even 0)

Generated even iterates satisfy the exponential power bound.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.odd_gap_contracts_pow {n : ℕ} (alg : HSDGeneratedAlgorithm n) (k : ℕ) : gap (alg.odd k) ≤ ytmContraction n ^ (k + 1) * gap (alg.even 0)

Generated odd iterates satisfy the corresponding one-predictor-shifted bound.

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.logL {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) : ℝ

Logarithmic pair bound for the generated algorithm, using L = log(gap0 / ε) as in the paper-style iteration estimate.

Equations

• alg.logL ε = Real.log (HSDInteriorPointLP.gap (alg.even 0) / ε)

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) : ℕ

Pair-count ceiling bound computed from the generated algorithm's initial gap.

Equations

• alg.logPairBound ε = HSDInteriorPointLP.ytmLogPairBoundL n (alg.logL ε)

noncomputable def HSDInteriorPointLP.HSDGeneratedAlgorithm.logIterationBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) : ℕ

Ordinary iteration-count bound, twice the pair-count bound.

Equations

• alg.logIterationBound ε = 2 * alg.logPairBound ε

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.power_condition_of_logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) (hε : 0 < ε) : ytmContraction n ^ alg.logPairBound ε * gap (alg.even 0) ≤ ε

The generated pair bound implies the required power condition.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.gap_stop_even_at_logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) (hε : 0 < ε) : YTMGapStop ε (alg.even (alg.logPairBound ε))

Gap stopping at the generated logarithmic pair bound.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.gap_stop_odd_at_logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) (hε : 0 < ε) : YTMGapStop ε (alg.odd (alg.logPairBound ε))

The predictor point at the same pair index also satisfies the gap test.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.mu_stop_even_at_logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) (hε : 0 < ε) : YTMMuStop ε (alg.even (alg.logPairBound (hdim n * ε)))

Generated even iterate satisfies the μ ≤ ε test at the log bound.

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.mu_stop_odd_at_logPairBound {n : ℕ} (alg : HSDGeneratedAlgorithm n) (ε : ℝ) (hε : 0 < ε) : YTMMuStop ε (alg.odd (alg.logPairBound (hdim n * ε)))

Generated odd iterate satisfies the μ ≤ ε test at the log bound.

structure HSDInteriorPointLP.HSDGeneratedAlgorithm.PaperStyleStop {n : ℕ} (PrimalResidualStop DualResidualStop : HSState n → Prop) (ε : ℝ) (w : HSState n) : Prop

Abstract paper-style stopping condition: the residual predicates are parameters, because the current HLP skeleton has not yet introduced concrete primal and dual residual maps.

• mu_stop : YTMMuStop ε w
• primal_stop : PrimalResidualStop w
• dual_stop : DualResidualStop w

theorem HSDInteriorPointLP.HSDGeneratedAlgorithm.PaperStyleStop.of_mu_and_residuals {n : ℕ} {PrimalResidualStop DualResidualStop : HSState n → Prop} {ε : ℝ} {w : HSState n} (hmu : YTMMuStop ε w) (hp : PrimalResidualStop w) (hd : DualResidualStop w) : PaperStyleStop PrimalResidualStop DualResidualStop ε w

Once residual estimates are available, this packages them with μ ≤ ε.