Lean formalization bounty: Bernstein obstacle theorem package

Goal

Produce a faithful, pinned, no-sorry, axiom-audited Lean formalization of the corrected Bernstein–Bézier obstacle theorem package.

Staged public bounty schedule and current state

Total proposed staged project bounty: $248,500. These figures are project estimates, not verified market values or guaranteed funds.

Verified Lean baseline

• Branch: review/bernstein-obstacle-v1
• Commit: 209460f762b24d05534075424a5a3864cc5edb9c
• Successful Lean audit: run 29777931837
• Successful full reproduction: run 29777931942

This baseline remains immutable because the finite algebraic and abstract Hilbert-space layers are machine verified there.

Corrected analytical statement target

• Branch: review/bernstein-obstacle-v2-corrected
• Commit: f2bd41f19ff5afbcca8a23f9afdcdf084364dae4
• Correction PR: #106

Any new theorem-correspondence work must compare the Lean baseline with the corrected v2 manuscript, especially the local-size risky set, one-ring grading, uniform broken regularity, and physical-boundary hypotheses. The analytical moving-Sobolev/free-boundary theorem is not claimed as fully formalized.

Current extension

PR #104 adds a coordinate-free real Hilbert-space layer:

• VI Pythagorean inequality;
• squared-distance error control;
• VI-to-metric-minimizer transfer;
• uniqueness of the Hilbert-space VI solution.

It targets review/bernstein-obstacle-v1 so the extension is reviewed against the immutable machine-verified baseline.

Remaining high-value formalization tasks

1. Define a changing family of conforming simplicial finite-element spaces as subspaces of a fixed physical Sobolev/Hilbert space.
2. Formalize nonnegative smooth density in H_0^1 ∩ {v ≥ 0}.
3. Formalize the positive Bernstein sampling/recovery operator and its affine-element estimates.
4. Prove the moving-cone Mosco recovery and weak-limit conditions in the physical space.
5. Connect the abstract Hilbert-space VI theorem to the moving discrete minimizers.
6. Formalize the corrected local-size risky set, one-ring grading, tubular free-boundary geometry, coefficient localization, strip measure and the h_Gamma^(3/2) repair estimate.
7. Formalize the physical-boundary face/off-face split, multiplier consistency and the energy/Falk routes.

Acceptance requirements

Every paid milestone must include:

• a pinned Lean/mathlib revision;
• no sorry and no undeclared project axioms;
• explicit #print axioms regression tests;
• deterministic build instructions;
• a theorem correspondence document proving statement faithfulness to v2;
• independent review before analytical theorem milestones are accepted.

These bounty values are project estimates, not claims of a universal market rate.