noncomputable def centralSymmetryRoundingObjective (n : ℕ) (σ α : ℝ) : ℝ

The scalar objective V(α) on [0, 1) used in the centrally symmetric rounding estimate.

noncomputable def centralSymmetryRoundingAlphaStar (n : ℕ) (σ : ℝ) : ℝ

The explicit critical point α* = σ / (n (1 + σ) - 1) of the scalar objective.

theorem centralSymmetryRoundingObjective_log_arguments_pos {n : ℕ} {σ α : ℝ} (hn : 1 ≤ n) (hσ : -1 ≤ σ) (hα : α ∈ Set.Ico 0 1) : 0 < 1 - α ∧ 0 < 1 + α * (↑n * (1 + σ) - 1)

Helper for Proposition 7.8: on [0, 1), both logarithmic arguments in the scalar objective are strictly positive.

theorem centralSymmetryRoundingObjective_hasDerivAt {n : ℕ} {σ α : ℝ} (hα : α ∈ Set.Ico 0 1) (hlog : 0 < 1 + α * (↑n * (1 + σ) - 1)) : HasDerivAt (centralSymmetryRoundingObjective n σ) ((↑n * (1 + σ) - 1) / (1 + α * (↑n * (1 + σ) - 1)) - (↑n - 1) / (1 - α)) α

Helper for Proposition 7.8: the scalar objective has the expected first derivative on the open interval (0, 1).

theorem centralSymmetryRoundingObjective_deriv_formula {n : ℕ} {σ α : ℝ} (hn : 1 ≤ n) (hσ : -1 ≤ σ) (hα : α ∈ Set.Ioo 0 1) : deriv (centralSymmetryRoundingObjective n σ) α = (↑n * (1 + σ) - 1) / (1 + α * (↑n * (1 + σ) - 1)) - (↑n - 1) / (1 - α)

Helper for Proposition 7.8: the derivative formula is available as a reusable rewrite lemma.

theorem centralSymmetryRoundingAlphaStar_log_argument {n : ℕ} {σ : ℝ} (hcoeff : ↑n * (1 + σ) - 1 ≠ 0) : 1 + centralSymmetryRoundingAlphaStar n σ * (↑n * (1 + σ) - 1) = 1 + σ

Helper for Proposition 7.8: at the explicit critical point, the first logarithmic argument simplifies to 1 + σ.

theorem centralSymmetryRoundingAlphaStar_mul_coeff {n : ℕ} {σ : ℝ} (hcoeff : ↑n * (1 + σ) - 1 ≠ 0) : centralSymmetryRoundingAlphaStar n σ * (↑n * (1 + σ) - 1) = σ

Helper for Proposition 7.8: multiplying the closed form for α* by the scalar coefficient recovers σ.

theorem centralSymmetryRoundingAlphaStar_mem_Ico {n : ℕ} {σ : ℝ} (hn : 2 ≤ n) (hσ : 0 ≤ σ) : centralSymmetryRoundingAlphaStar n σ ∈ Set.Ico 0 1

The explicit critical point α* lies in the interval [0, 1).

theorem centralSymmetryRoundingObjective_deriv_sub_deriv_factorization {n : ℕ} {σ x y : ℝ} (hn : 1 ≤ n) (hσ : -1 ≤ σ) (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo 0 1) : deriv (centralSymmetryRoundingObjective n σ) x - deriv (centralSymmetryRoundingObjective n σ) y = (y - x) * ((↑n * (1 + σ) - 1) ^ 2 / ((1 + x * (↑n * (1 + σ) - 1)) * (1 + y * (↑n * (1 + σ) - 1))) + (↑n - 1) / ((1 - x) * (1 - y)))

Helper for Proposition 7.8: subtracting two derivative values factors through y - x with a manifestly nonnegative bracket.

theorem centralSymmetryRoundingObjective_deriv_strictAntiOn {n : ℕ} {σ : ℝ} (hn : 1 ≤ n) (hσ : -1 ≤ σ) (hstrict : ↑n * (1 + σ) - 1 ≠ 0 ∨ 1 < n) : StrictAntiOn (deriv (centralSymmetryRoundingObjective n σ)) (Set.Ioo 0 1)

Helper for Proposition 7.8: the derivative of the scalar objective is strictly antitone on (0, 1) once at least one logarithmic summand is genuinely nonconstant.

theorem centralSymmetryRoundingObjective_deriv_eq_zero_at_alphaStar {n : ℕ} {σ : ℝ} (hn : 2 ≤ n) (hσ : 0 ≤ σ) : deriv (centralSymmetryRoundingObjective n σ) (centralSymmetryRoundingAlphaStar n σ) = 0

Helper for Proposition 7.8: the derivative vanishes at the explicit critical point.

theorem centralSymmetryRoundingObjective_isMaxOn_alphaStar {n : ℕ} {σ : ℝ} (hn : 2 ≤ n) (hσ : 0 ≤ σ) : IsMaxOn (centralSymmetryRoundingObjective n σ) (Set.Ico 0 1) (centralSymmetryRoundingAlphaStar n σ)

Helper for Proposition 7.8: the explicit critical point is a maximizer on [0, 1).

theorem centralSymmetryRoundingObjective_strictConcaveOn {n : ℕ} {σ : ℝ} (hn : 1 ≤ n) (hσ : -1 ≤ σ) (hstrict : ↑n * (1 + σ) - 1 ≠ 0 ∨ 1 < n) : StrictConcaveOn ℝ (Set.Ico 0 1) (centralSymmetryRoundingObjective n σ)

The objective V is strictly concave on [0, 1) once both logarithmic terms are well defined and at least one of them is genuinely nonconstant.

theorem centralSymmetryRoundingObjective_firstOrderCondition_iff {n : ℕ} {σ : ℝ} (hn : 1 ≤ n) (hcoeff : ↑n * (1 + σ) - 1 ≠ 0) {α : ℝ} (hα : α ∈ Set.Ico 0 1) (hlog : 0 < 1 + α * (↑n * (1 + σ) - 1)) : (↑n - 1) / (1 - α) = (↑n * (1 + σ) - 1) / (1 + α * (↑n * (1 + σ) - 1)) ↔ α = centralSymmetryRoundingAlphaStar n σ

On the genuine logarithmic domain inside [0, 1), the first-order condition for V is equivalent to α = α*.

theorem centralSymmetryRoundingObjective_isMaxOn_iff {n : ℕ} {σ : ℝ} (hn : 2 ≤ n) (hσ : 0 ≤ σ) {α : ℝ} (hα : α ∈ Set.Ico 0 1) : IsMaxOn (centralSymmetryRoundingObjective n σ) (Set.Ico 0 1) α ↔ α = centralSymmetryRoundingAlphaStar n σ

Proposition 7.8: among feasible points α ∈ [0, 1), the scalar objective V is maximized exactly at α* = σ / (n (1 + σ) - 1).

theorem centralSymmetryRoundingObjective_alphaStar_value {n : ℕ} {σ : ℝ} (hcoeff : ↑n * (1 + σ) - 1 ≠ 0) : centralSymmetryRoundingObjective n σ (centralSymmetryRoundingAlphaStar n σ) = Real.log (1 + σ) + (↑n - 1) * Real.log ((↑n - 1) * (1 + σ) / (↑n * (1 + σ) - 1))

The scalar objective evaluated at α* has the closed form stated in the proposition.