quadratic_neumann_middle_index_distinct_centered_coefficients_from_kernel_square_base_bounds_min_dim_shifted

This is a formal Lean bridge, not a theorem stated verbatim in Candes--Recht. It connects the source-backed pointwise centered-tail theorem quadratic_neumann_middle_index_distinct_centered_coefficient_pointwise_tail_from_kernel_square_base_bounds_min_dim with the source-backed shifted union-bound theorem quadratic_neumann_middle_index_distinct_centered_coefficients_uniform_from_shifted_pointwise_tails for the middle-index-distinct quadratic Neumann term. Source location: Candes--Recht, Exact matrix completion via convex optimization, Section 6.3, proof of Lemma 4.6, PDF p. 30 equation (6.20) for the partition of the cubic Neumann sum, and PDF pp. 32--33 for the third term omega_1 = omega_3 != omega_2; the scalar Bernstein and coordinate-union pattern follows the same Section 6.2 mechanism, PDF p. 29 after equation (6.17).

Let M be an n_1 x n_2 rank-r matrix with SVD data S satisfying the incoherence hypotheses A0(S, mu_0) and A1(S, mu_1). Here mu_0 controls the singular-vector coherence, mu_1 controls the entry size of the sign matrix, n = max(n_1,n_2), and p = m/(n_1 n_2). In the Bernoulli model, Omega_2 includes each coordinate independently with probability p, and bernoulliEventProb(p, E) is the probability of event E under this product model. The parameter beta > 2 controls the polynomial failure rate n^{-beta}, and lambda >= 1 is the density slack parameter.

Assume the centered coefficient identity for every coordinate w_1, and assume the corrected min-dimension kernel-square base bounds

and

This bridge deliberately requires both the usual density floor

and the strengthened shifted density floor

The strengthened beta+2 hypothesis is essential for this formal route: the pointwise tail is applied with parameter beta+2, producing per-coordinate failure of order n^{-(beta+2)}, and the shifted uniformization theorem then pays the n_1 n_2 <= n^2 union-bound loss to obtain a uniform n^{-beta} bound.

Under these hypotheses, there exist positive universal constants Ccoef and ccoef, depending only on the supplied base-bound constants, such that

where Q(Omega_2) is the centered conditional coefficient matrix quadraticMiddleIndexDistinctCenteredCoefficientMatrix Omega2 S p, and the Lean event is QuadraticMiddleIndexDistinctCenteredCoefficientBound Omega2 S p (Ccoef * lambda^{-1}). This node should not be cited as removing the beta+2 sample-density requirement; it is exactly the formal bridge that records that strengthened hypothesis.