theorem CentralSymmetricRoundingMethod.logdet_growth_lower_bound_upto {n : ℕ} (method : CentralSymmetricRoundingMethod n) {T : ℕ} {c : ℝ} (hstep : ∀ k < T, c ≤ Real.log (method.matrix (k + 1)).det - Real.log (method.matrix k).det) : c * ↑T ≤ Real.log (method.matrix T).det - Real.log (method.matrix 0).det

Helper for Theorem 7.6: telescoping a uniform lower bound on the logarithmic determinant increments gives a linear lower bound on the total growth up to time T.

theorem CentralSymmetricRoundingMethod.unit_ellipsoid_subset_at_stoppingIndex {n : ℕ} (method : CentralSymmetricRoundingMethod n) (hTerminate : method.Terminates) {R : ℝ} (hInitial : IsBetaRounding (↑method.body) R (method.matrix 0) 0) (hinner : ∀ k < stoppingIndex hTerminate, centeredMatrixEllipsoid (method.matrix (k + 1)) 1 ⊆ ↑method.body) : centeredMatrixEllipsoid (method.matrix (stoppingIndex hTerminate)) 1 ⊆ ↑method.body

Helper for Theorem 7.6: the terminal iterate still contains the unit centered ellipsoid at the canonical stopping index.

theorem CentralSymmetricRoundingMethod.centered_matrixEllipsoid_volume_toReal {n : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (hG : G.PosDef) {r : ℝ} (hr : 0 ≤ r) : (MeasureTheory.volume (centeredMatrixEllipsoid G r)).toReal = √G.det * (MeasureTheory.volume (Metric.closedBall 0 r)).toReal

Helper for Theorem 7.6: the centered ellipsoid volume identity in real-valued form.

theorem CentralSymmetricRoundingMethod.terminal_logdet_upper_bound_of_rounding_containment {n : ℕ} (method : CentralSymmetricRoundingMethod n) {R : ℝ} {T : ℕ} (hInitial : IsBetaRounding (↑method.body) R (method.matrix 0) 0) (hFinal : centeredMatrixEllipsoid (method.matrix T) 1 ⊆ ↑method.body) : Real.log (method.matrix T).det - Real.log (method.matrix 0).det ≤ 2 * ↑n * Real.log R

Helper for Theorem 7.6: the initial centered rounding and the terminal inner containment bound the total logarithmic determinant growth by 2 n log R.

theorem CentralSymmetricRoundingMethod.gamma_step_gain_lower_bound {γ : ℝ} (hγ : 1 < γ) : (γ - 1) ^ 2 / γ ^ 2 ≤ 2 * Real.log γ - (γ ^ 2 - 1) / γ ^ 2

Helper for Theorem 7.6: the simpler coefficient (γ - 1)^2 / γ^2 is bounded by the exact per-step logarithmic determinant gain.

theorem CentralSymmetricRoundingMethod.stoppingIndex_le {n : ℕ} (method : CentralSymmetricRoundingMethod n) (hTerminate : method.Terminates) {R : ℝ} (hInitial : IsBetaRounding (↑method.body) R (method.matrix 0) 0) (hinner : ∀ k < stoppingIndex hTerminate, centeredMatrixEllipsoid (method.matrix (k + 1)) 1 ⊆ ↑method.body) (hlogDet : ∀ k < stoppingIndex hTerminate, Real.log (method.matrix (k + 1)).det ≥ Real.log (method.matrix k).det + (2 * Real.log method.gamma - (method.gamma ^ 2 - 1) / method.gamma ^ 2)) : ↑(stoppingIndex hTerminate) ≤ 2 * ↑n * method.gamma ^ 2 / (method.gamma - 1) ^ 2 * Real.log R

Theorem 7.6: if an Algorithm 7.5 run starts from the centered R-rounding W₁(G₀) ⊆ C ⊆ W_R(G₀), if every post-update iterate before the first stopping index still satisfies W₁(Gₖ) ⊆ C, and if every genuinely continuing step k < s gains at least 2 log γ - (γ² - 1) / γ² in log det Gₖ, then the canonical first stopping index s is bounded by 2 n γ² / (γ - 1)² * log R.