Mathematical audit and formal coverage

Source: arXiv:2609.27634v1, 23 September 2026.

Status: complete for stated scope. The labeled mathematical results and quantitative claims mapped below are the declared scope. This revision determines two exact regions, (rho,nu) and (eta,nu), and derives the exact region of (nu(C), nu(C^T)) as a corollary. The (beta,nu)-region of the previous version is no longer part of the manuscript. No results from other manuscripts are in scope.

Notation: the manuscript's parametrization

The manuscript parametrizes its three extremal families so that every parameter increases with dependence. D_c runs from D_0 = W to D_1 = M, and its support has its kink at u = c. A_w pairs the leading fraction w of the first variable comonotonically and runs from A_0 = W to A_1 = M. B_b, for b in (0,1/2], splits the leading fraction b between two branches, with B_(1/2) = A_(1/2).

ExactBlestPaperParams.lean defines these families exactly as printed (paperD, paperA, paperB, with paperEtaB = e_b, paperNuB = nu(B_b), paperNB = n_b, paperUpsB = Upsilon(e_b), and paperR = R_b) and restates every family-dependent claim in this notation. The table below cites these restatements first, so the manuscript and the Lean statements can be read side by side without translation.

The underlying constructions in the other modules predate the current parametrization and use the reflected parameters: familyA w is A_(1-w), familyB a is B_(1-a), and rhoFullFamily c is D_(1-c). The bridging theorems Papers.Rockel2026ExactBlest.paperA_symm, Papers.Rockel2026ExactBlest.paperB_symm, and the definition of paperD make this explicit, and the paper-form theorems are derived from the internal ones.

Overall finding

No discrepancy was found in the formulas, constants, parameter ranges, or proof arguments of the revised manuscript. No mathematical correction was needed. Every labeled result has a formally checked counterpart, and so do the quantitative claims added in the revision:

• both set equalities of cor:nu-transpose, the boundary function Lambda with its two displayed branches, and unique attainment of the largest and smallest nu(C^T) at every value of nu(C), with the extremizers identified as A_w^T, B_b^T, W, and the upper extremizers themselves;
• the closed-form bound for nu(C) >= -7/8 stated in the introduction;
• the derivative facts used in the proof of the corollary, Upsilon'(e) in [-1/3,1/3] on [-3/4,1) and Upsilon'(e_b) = (2-3b)/(2-b);
• continuity of Upsilon, in particular at the regime change -3/4;
• the bound 1/2 obtained from Theorem 1.1 alone, and the statement that nu(C)-rho(C) and nu(C^T)-rho(C) cannot be extreme in opposite directions;
• central symmetry of the (rho,nu)-region and its failure for (eta,nu);
• the non-extremality of A_w for w < 1/2 and the shuffle description of the rho-eta extremizers in the final remark;
• the values quoted in the figure captions and printed above the figure panels;
• the dual-certificate lemma lem:dual-certificate for a general continuous cost.

This does not mean that every intermediate step in the printed proofs was translated literally. The formalization sometimes uses a different proof of the same statement, as recorded below.

The strict Lean check compiles all 592 local theorems and their transitive axiom audits. The separate SymPy script passes all 82 exact identity checks, stated in the manuscript's parametrization. Neither count should be read as a count of fully formalized paper results.

Claim-by-claim coverage

Retained checks for the removed discussion section

The previous version ended with a discussion section, which the manuscript no longer contains. Its numerical claims remain checked: Papers.Rockel2026ExactBlest.rho_zero_fibre proves that rho(C)=0 confines nu(C) exactly to [-1/4,1/4], Papers.Rockel2026ExactBlest.nu_zero_fibre identifies the nu^T-fibre at nu=0 as [Lambda^{-1}(0), Lambda(0)], Papers.Rockel2026ExactBlest.Lambda_zero_bounds and Papers.Rockel2026ExactBlest.LambdaInv_zero_bounds give 0.375 < Lambda(0) < 0.385 and -0.425 < Lambda^{-1}(0) < -0.415, and Papers.Rockel2026ExactBlest.transposition_fibre_longer checks that this fibre is longer than 1/2.

Retained checks for the removed (beta,nu)-region

The previous version of the manuscript also determined the (beta,nu)-region. Its modules stay in the build because other modules import them, and they still check the earlier results: Papers.Rockel2026ExactBlest.local_frechet_bounds, Papers.Rockel2026ExactBlest.beta_upper_cdf, Papers.Rockel2026ExactBlest.beta_lower_cdf, Papers.Rockel2026ExactBlest.beta_nu_region, Papers.Rockel2026ExactBlest.beta_upper_exists_unique, Papers.Rockel2026ExactBlest.beta_lower_exists_unique, Papers.Rockel2026ExactBlest.nu_beta_bound, Papers.Rockel2026ExactBlest.nu_beta_eq_iff, Papers.Rockel2026ExactBlest.beta_width, and Papers.Rockel2026ExactBlest.beta_rho_region. None of these statements appears in the current manuscript.

Proof route for the (nu,nu^T)-corollary

The map L(e,n) = (n, 2e-n) turns the (eta,nu)-region into the (nu,nu^T)-region, which gives the first set equality directly (Papers.Rockel2026ExactBlest.nu_transpose_fibre_gap). For the second, Lean first proves that Lambda is a strictly increasing bijection of [-1,1]. On the closed branch it writes n = 2s^4-1 with s = ((1+n)/2)^(1/4), so that Lambda(n) = 4s^3-2s^4-1, and uses the factorization (t-s)(4ts+2(t^2+s^2)(2-t-s)) of the difference. On the parametric branch it uses strict monotonicity of n_b and nu(B_b) in the parameter, and it joins the branches at -7/8. Then Lambda(e-Upsilon(e)) = e+Upsilon(e) for every e (Papers.Rockel2026ExactBlest.Lambda_curve), checked separately on the graph regime, the randomized regime, and at e=-1. With e = (n+m)/2, monotonicity of Lambda alone shows that |n-m| <= 2*Upsilon(e) holds exactly when Lambda^{-1}(n) <= m <= Lambda(n) (Papers.Rockel2026ExactBlest.gap_band_iff). This replaces the convexity-and-boundary argument of the printed proof and needs no continuity of Upsilon.

The same identity also gives the printed monotonicity claim: if e-Upsilon(e) failed to increase, applying Lambda and adding would contradict 2e < 2e'. A copula attaining m = Lambda(n) must lie on the lower (eta,nu)-boundary, so uniqueness follows from Papers.Rockel2026ExactBlest.eta_lower_unique, and Papers.Rockel2026ExactBlest.upper_extremizer_cases classifies the upper extremizers as A_w, B_b, or W. Continuity of Upsilon then follows from continuity of the monotone bijection e -> e-Upsilon(e) inside (-1,1), and from the squeeze 0 <= Upsilon(e) <= min(1+e, 1-e) at the endpoints.

For the derivative on the randomized branch, the inverse parameter e -> b is monotone with an interval image, hence continuous. The inverse function theorem for one-dimensional derivatives then differentiates it, and the chain rule gives Upsilon'(e_b) = (2-3b)/(2-b).

Proof routes for the two regions

For rho, the internal parameter is t = 2(1-c) on the nonnegative-rho half. The dual potentials are piecewise cubic (one piece uses an absolute value). Their four rectangle slacks are nonnegative, and their integrals give nu-t*rho <= 1-t+t^4/4. An ordinal sum built from the half-width two-strip copula has rho=1-t^3 and nu=1-3*t^4/4. Reflection supplies the negative-rho half; survival supplies the lower boundary. The real-power identity is checked in Lean, not assumed.

For equality, the integrated nonnegative slack must vanish almost everywhere. The checked contact identity forces the rank map zeta_c, and Papers.Rockel2026ExactBlest.copula_eq_of_graph proves that the uniform first marginal determines the resulting law. Reflection and survival extend uniqueness to every rho and both boundaries.

For eta, stripCopula glues two probability measures into adjacent horizontal strips and proves both marginals uniform. The B_b construction uses this law inside an ordinal sum and then reflects it. The pointwise B-certificate is integrated exactly; its moments, unique parameter, attainment, and mixtures fill the entire randomized regime. The endpoint fibre is treated separately. A final module connects both parameterizations to the displayed Upsilon formulas.

The eta equality proofs integrate the nonnegative slack and use its almost-everywhere vanishing. In the A regime, four rectangle factorizations force Z=T_w(X) away from two coordinate lines. Uniform marginals make those lines null, even when w=1/2 creates an additional horizontal contact segment. In the B regime, six factorizations instead force X=R_b(Z) off null cut lines; the uniform second marginal fixes the whole law. These arguments identify the actual ordinal-sum/glued constructions with the manuscript's graph measures, not just with their coefficient pairs. Transposition gives the lower boundary. The eta -1 endpoint follows from Blest-minimum uniqueness, itself obtained by reflection from the rho support certificate at parameter zero. At w=3/4, the supporting functional is proportional to nu-eta, so the same uniqueness proof gives the full sharp asymmetry cases.

Points checked carefully in the manual audit

• All moment computations use the reflected variables X=1-U, Z=1-V. The direction of the quadratic weight matters. The Lean moment bridge fixes this convention rather than assuming it.
• For B_b, the map is read as X=R_b(Z). Its two inverse branches have probabilities 1/(2(1-b)) and (1-2b)/(2(1-b)). Their densities add to one on (1-b,1], while the final branch covers [0,1-b) with unit density.
• At b=1/2, the middle interval is empty, so its displayed denominator 1-2b is never used. The remaining map and coefficients match A_(1/2).
• At w=1/2, the graph-regime dual acquires an extra horizontal contact segment. Uniform marginals rule out mass on that segment and on the breakpoint's vertical line. This is essential to the paper's uniqueness argument, and is not implied by nonnegativity alone.
• In the two-branch certificate, the factors at z=z_b reduce to (1-2b)(1-x). Their additional zero is the branch junction (1,z_b), not an additional positive-mass support component.
• The paper handles the eta endpoints by a strict positive-weight CDF argument. The formal proof also supplies them: the A certificate covers +1, and the rho-certificate/reflection argument above handles -1.
• The maximum graph-regime gap is 27/128 at w=3/4; the two-branch gap increases to 1/8 as b -> 1/2. The transition, figure value -2257/2304 for B_(1/4), and all stated sharp constants agree with independent exact integration.
• In cor:nu-transpose, the parameter of the maximizer is w = ((1+n)/2)^(1/4) in terms of n = nu(C), while the proof uses w = ((1+e)/2)^(1/3) in terms of e = eta. Both are consistent: nu(A_w^T) = 2w^4-1 and eta(A_w) = 2w^3-1.
• The two formulas for Lambda agree at -7/8 with value -5/8, and the interval (-1,-7/8) of the parametric branch is exactly the image of b in (0,1/2), so Lambda is well defined on [-1,1].
• The shuffle in the final remark is the ordinal sum of W on [0,3/4] and M on [3/4,1]. It is symmetric, has rho = 5/32 and nu = eta = -7/128, and so attains rho-eta = 27/128.

Completion and scope

All labeled results of the revised manuscript and the quantitative claims listed above are proved. The four modules added in the revision are:

• ExactBlestTranspose.lean: the parameter n_b (internally in the reflected parameter), the two branches of Lambda, their junction, and the monotone bijection.
• ExactBlestTransposeRegion.lean: both descriptions of the (nu,nu^T)-region, the boundary curves, unique extremizers and their identification, the closed-form bound, and continuity of Upsilon.
• ExactBlestClaims.lean: the dual-certificate lemma, derivative facts, symmetries, the bound 1/2, numerical fibres, and the final remark.
• ExactBlestPaperParams.lean: the families D_c, A_w, and B_b in the manuscript's parametrization, with every family-dependent statement and all figure values restated in that notation.

Historical motivation, references, and literal proof prose are not Lean statements. Some printed intermediate steps are replaced by the alternative proof routes documented above. There are no proof placeholders, custom axioms, or hypotheses equal to unproved paper conclusions. The integrated supplement uses the root Lake project and its pinned dependencies; see README.md for reproduction.