Audit panel E: unified grand positive-basis theorem

Objective

Adversarially audit the unified Grand Positive-Basis Constraint Theorem in PR #128.

Current target

• branch: agent/bernstein-grand-unified-v3
• document: math/bernstein_obstacle/GRAND_THEOREM_V3_UNIFIED.md
• PR: #128

A frozen review commit will be posted only after the final Lean audit succeeds and any corrections are incorporated.

Four layers under review

1. Positive-basis Mosco convergence, translated cones, and moving obstacles.
2. Universal gradient-modulus/contact-measure rate for arbitrary interior contact topology and nonsymmetric coercive operators.
3. Minkowski/vanishing-order clipping law and quadratic-contact 3/2 saturation/sharpness.
4. Exact unilateral and bilateral box constraints, including nonpolynomial obstacles.

Required mathematical checks

1. Legitimacy of the affine nonpolynomial obstacle trial set psi + V_h.
2. Existence and uniqueness for the nonsymmetric continuous coercive variational inequality.
3. Positive Bernstein recovery, conformity, and homogeneous trace preservation.
4. The local gradient-modulus estimate.
5. Use of Poincare to control the full H1 norm.
6. Zero gradient at every interior contact point under the stated C1 assumptions.
7. The contact estimate B_h g(x) <= C h_T omega_T(h_T), including interior mesh-skeleton points.
8. Pairing with a multiplier in the variational dual that extends to a finite Radon measure on the open domain.
9. Every sign in the nonsymmetric Falk transfer.
10. The local estimate eta_h^2 + mu_h, global modulus corollary, and C^{1,beta} rate.
11. Correct interpretation of boundary-touching active sets: the closure may reach the boundary, but no boundary multiplier is claimed.
12. The Minkowski repair and VI exponent formulas.
13. The use of a=min(m,q) and the quadratic-contact saturation claim.
14. The phase-locked sharpness construction and what class it proves sharpness for.
15. The bilateral normalization theta=(u-psi)/(phi-psi) and affine trial space.
16. Lower/upper multiplier decomposition and box-rate signs.
17. One-dimensional and arbitrary-dimensional simplicial Lean box certificates.
18. Exact division between machine-checked algebra/endgames and analytical Sobolev/PDE inputs.

Required prior-art checks

Compare against classical Falk/Brezzi variational-inequality estimates, nonsymmetric and hp-adaptive obstacle FEM, higher-order and mixed methods, proximal/hierarchical hp Galerkin methods, bounds-constrained Bernstein approximation, positive-basis range certificates, and the 2026 GLL-constrained O(h/p) hp/spectral result.

Determine whether the local gradient-modulus/contact-measure criterion, the Minkowski saturation classification, or their combination with exact Bernstein certificates is genuinely new or already implicit in prior work.

Deliverable

Return PASS, PASS AFTER CORRECTION, or FAIL, with a numbered response to all checks and exact citations. Clearly separate validity, sharpness, scope, formal faithfulness, and novelty. Counterexamples, narrower corrected theorems, and prior-art collisions are valid successful outcomes.

Start with math/bernstein_obstacle/GRAND_THEOREM_V3_UNIFIED.md on branch agent/bernstein-grand-unified-v3 and compare it with PR #128. Work through the numbered mathematical, Lean, and prior-art checks, recording exact citations and separating validity, sharpness, scope, formal faithfulness, and novelty. Done means a numbered response covering every check with PASS, PASS AFTER CORRECTION, or FAIL.