Reciprocal estimates retain the exact leading coefficients when solving the normalized determinant inequality, even when its bracket is negative.

theorem CCDN.auxiliary_reciprocal_bound {r d M X a : ℝ} (hr : 0 ≤ r) (hd : 1 ≤ d) (hM : 2 * d ≤ M) (hX : 0 < X) (ha : X * (M - d) / ((r + 1) * M) ≤ a) : 0 < a ∧ 1 / a ≤ (r + 1) / X * (1 + 2 * d / M)

If a ≥ X (M - d) / ((r + 1) M) with X > 0, d ≥ 1 and M ≥ 2 d, then a is positive and 1 / a ≤ (r + 1) / X * (1 + 2 d / M).

theorem CCDN.auxiliary_kernel_quotient_bound {r d M X a k : ℝ} (hr : 0 ≤ r) (hd : 1 ≤ d) (hM : 0 < M) (hX : 0 < X) (ha : 0 < a) (hk : 0 ≤ k) (hupper : a ≤ X * (M + r) / ((r + 1) * M)) (hlower : 1 / (d * (r + 1)) - 1 / M ≤ k) : 1 / (d * X) - (2 * r + 1) / (X * M) ≤ k / a

If 0 < a ≤ X (M + r) / ((r + 1) M) and k ≥ 1 / (d (r + 1)) - 1 / M is nonnegative, then k / a ≥ 1 / (d X) - (2 r + 1) / (X M).

theorem CCDN.auxiliary_small_height_bracket_bound {r d M X a k u b l : ℝ} (hr : 0 ≤ r) (hd : 1 ≤ d) (hM : 2 * d ≤ M) (hX : 0 < X) (halow : X * (M - d) / ((r + 1) * M) ≤ a) (haup : a ≤ X * (M + r) / ((r + 1) * M)) (hk : 0 ≤ k) (hklow : 1 / (d * (r + 1)) - 1 / M ≤ k) (hb : 0 ≤ b) (hl : 0 ≤ l) (hheight : l ≤ 2 * d * (r + 1) * b) (hscale : d * b ≤ X * M) (hcomparison : a * u ≤ b - k * l) : u ≤ (r + 1) / X * b - l / (d * X) + 4 * (r + 1) ^ 2

Solve the normalized inequality without imposing a sign on its bracket. The small-height assumptions absorb both reciprocal errors into C(r).