Audit panel B: Mosco convergence and finite-element recovery

Objective

Independently audit the general analytical theorem at the corrected immutable target:

K_h^B -> K in the Mosco sense for fixed-degree conforming simplicial Bernstein coefficient cones, followed by strong convergence of symmetric coercive obstacle minimizers.

Frozen target

• branch: review/bernstein-obstacle-v4-final
• commit: 61594952ad880d2b61759cfa93a19df979183c09
• analytical integration PR: #114
• parent audit: #96

Earlier targets remain available only for provenance.

Required checks

1. Exact inclusion K_h^B subset K under global shared-face coefficients.
2. Density of nonnegative smooth compactly supported functions in H_0^1(Omega) ∩ {v >= 0}.
3. Conformity and boundary-trace preservation of the sampled Bernstein recovery operator.
4. Dimension-safe local approximation estimate in the smooth recovery class; no illicit unrestricted point evaluation on H^2.
5. Threshold-form recovery estimates and the constructive scheduled diagonal sequence.
6. Weak closure of the continuous cone.
7. Strong minimizer convergence by Mosco/projection and direct energy arguments.
8. Dependence of constants on degree, dimension, shape regularity, continuity, and coercivity.
9. Exact scope of smooth-obstacle shifting and exclusion of arbitrary inexact obstacle approximation.
10. Whether ThresholdSobolevFEMRecoveryData faithfully packages, rather than proves, the concrete analytical FEM inputs.

Deliverable

A numbered PASS, PASS AFTER CORRECTION, or FAIL report with derivations or precise references. State the strongest theorem that is actually valid if the submitted wording is too broad.

Internal scope label

FUN BUX: 4,500. This is an unfunded internal effort/complexity label, not a real or promised bounty. No payment is represented as available unless separate written funding terms are posted.

Use branch review/bernstein-obstacle-v4-final at commit 61594952ad880d2b61759cfa93a19df979183c09, starting with analytical integration PR #114 and parent audit #96. Check each of the ten listed analytical requirements and deliver a numbered PASS, PASS AFTER CORRECTION, or FAIL report with derivations or precise references, stating the strongest valid theorem when the wording is too broad.