Independent review requested: Bernstein–Bézier coefficient-inner-cone grand theorem

We request independent review of the Bernstein–Bézier certified inner-cone theorem package in draft PR #133.

Current review branch: formal/bernstein-bezier-grand-canonical
Current repair head at issue creation: 735b96d0d5363c5135b2d536d763060f238e1c88

The broad Bernstein convex-hull property and general finite-element Mosco theory are acknowledged prior art. The candidate combined contribution is narrower:

1. fixed-degree conforming simplicial Bernstein coefficient inner cones;
2. constructive high-order recovery for that practical inner subset;
3. globally assembled coefficient projection localized near an active interface;
4. the defect-order/codimension/duality rate
   gamma = min(beta - 1 + kappa/q, (beta + kappa + sigma)/q);
5. the balanced quadratic codimension-one 3/2 specialization;
6. a Lean bridge from finite coefficient certificates through abstract Mosco, VI, and rate endgames.

Review panels:

• A — numerical analysis / Mosco: convex-target density, positive Bernstein sampling, conformity, diagonal recovery, and prior-art boundary.
• B — free boundary / contact: localization, patch scaling, multiplier pairing, exponent derivation, and restricted sharpness claim.
• C — formal methods: theorem-to-Lean correspondence, explicit analytical hypotheses, full build, axiom transcript, and sorryAx audit.
• D — novelty: search for a source containing the full coefficient-inner-cone recovery plus localized rate mechanism.
• E — clean-room reproduction: independently reconstruct and run the numerical protocol.

Please report:

• name and affiliation;
• panel addressed;
• exact commit reviewed;
• verdict: PASS, PASS AFTER CORRECTION, or FAIL;
• numbered findings with file/theorem references;
• missing citations or collisions;
• permission or refusal to publish the report.

Entry documents on PR #133:

• math/bernstein_obstacle/EXTERNAL_REVIEW_REQUEST_2026-07-20.md
• math/bernstein_obstacle/GRAND_THEOREM_FINAL_REVIEWED_2026-07-20.md
• math/bernstein_obstacle/audit_packets/AI_RED_TEAM_PANEL_2026-07-20.md
• math/bernstein_obstacle/audit_packets/EXTERNAL_REVIEW_STATUS.md
• math/bernstein_obstacle/lean/GrandCanonicalAudit.lean
• math/bernstein_obstacle/lean/BernsteinObstacle/ConvexConstraint.lean

The internal AI red-team report is disclosed but does not count as independent validation.