Independent audit: Grand Barrier formalization and 2026 prior-art collision

Targets

• canonical branch: formal/bernstein-bezier-grand-canonical
• canonical draft PR: #133
• naming and prior-art ledger: math/bernstein_obstacle/GRAND_THEOREM_CANONICAL_NAMING_AND_PRIOR_ART.md
• formalization map: math/bernstein_obstacle/GRAND_FORMALIZATION_MAP.md
• terminal audit: math/bernstein_obstacle/lean/GrandCanonicalAudit.lean

Proposed theorem names

1. Bernstein–Bézier Grand Barrier Theorem
2. Bézier Inner-Cone Certificate
3. Bernstein–Bézier Barrier Envelope Theorem
4. Bernstein–Bézier Inner-Cone Falk Theorem
5. Bernstein–Bézier Codimension–Growth Clipping Law
6. Three-Halves Contact Law
7. Balanced Contact Exponent Principle
8. Bernstein–Bézier Bregman Transfer Theorem

Exact-phrase searches found no mathematically relevant naming collisions. This is not evidence that the underlying results are novel.

Formal audit required

1. Run the pinned Lean build on the exact PR head.
2. Execute GrandCanonicalAudit.lean.
3. Confirm no sorryAx, project axioms, or hidden unsafe declarations.
4. Check the imports copied from PRs #117 and #118 remain valid on the v3 base.
5. Verify the new proofs:
   • BilateralBarrierEnvelopeData.moscoConverges;
   • grandBarrier_mosco_and_hilbertConvergence;
   • monotoneInnerCone_falk_sq;
   • threeHalvesContactLaw;
   • balancedContactOrder_equalizes.
6. Produce a statement-faithfulness table distinguishing kernel theorems from physical analytical hypotheses.

Prior-art audit required

Compare the exact combined claim against at least:

• Allen–Kirby, arXiv:2104.11819;
• Kirby–Shapero, arXiv:2311.05880;
• the 2026 hp/SEM obstacle paper, DOI 10.1016/j.cnsns.2026.110252;
• higher-order p-Laplacian obstacle FEM, DOI 10.1016/j.camwa.2018.07.016;
• current Mosco stability literature for obstacle-type moving sets;
• Bernstein/Bezier positivity limiters and bounds-preserving FEM;
• bilateral/double-obstacle finite-element convergence literature.

The key collision question is not whether the ingredients exist separately. It is whether a prior source proves the same combination:

• conservative sampled bilateral obstacle envelopes;
• exact complete-element Bernstein coefficient inner sets;
• direct W_0^{1,p} strong recovery/Mosco convergence for that computable subset;
• nonlinear uniformly convex or strongly monotone transfer;
• codimension/contact exponent synthesis.

Required verdict

Return separate verdicts:

• LEAN PASS, LEAN PASS AFTER CORRECTION, or LEAN FAIL;
• NO EXACT COLLISION FOUND, PARTIAL COLLISION, or FULL COLLISION;
• exact strongest defensible theorem statement;
• exact acceptable use of the proposed names.

Repository-owner and automated-agent reports do not count as independent endorsement.

Start with the pinned Lean build on the exact head of PR #133, then execute math/bernstein_obstacle/lean/GrandCanonicalAudit.lean. Check the listed theorem proofs, imports from PRs #117 and #118, and the absence of sorryAx, project axioms, and unsafe declarations. Compare the combined claim with the cited literature and finish with the required Lean, collision, theorem-statement, naming, and faithfulness-table verdicts.