Audit panel D: Lean statement faithfulness and no-penetration bridge

Objective

Audit the Lean formalization and theorem-correspondence claims at the final V4 review target for correctness, axiom footprint, reuse quality, and faithfulness to the manuscript.

Frozen V4 target

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

The reviewer must verify that the manuscript does not imply the concrete moving Sobolev recovery or free-boundary geometry is fully formalized.

Current machine-checked scope to inspect

• finite Bernstein positivity, range, face-permutation, conformity, clipping, projection/KKT, energy, and VI layers;
• sequential Mosco, weak closure, diagonal recovery, and assembled minimizer convergence;
• constructive scheduled-stage selection from mesh thresholds;
• ThresholdSobolevFEMRecoveryData as the exact formal interface produced by local FEM estimates;
• strong convergence under explicit recovery and vanishing-gap assumptions;
• strip-scaling and sharp-rate algebra after geometric estimates are supplied.

Candidate V5 PR #117 additionally ports the coordinate-free Hilbert VI, nested-cone recovery inequality, and direct recovery-to-strong-convergence theorem onto V4. Do not count these additions as verified until their pinned workflow is green.

Required checks

1. Pinned Lean/mathlib revisions reproduce.
2. No sorry, project axioms, hidden unsafe declarations, or unreported nonstandard axioms.
3. #print axioms output is accurate.
4. Definitions match Bernstein formulas and global face assembly.
5. Quantifiers and domains match prose claims.
6. ScheduledRecovery.lean proves the claimed threshold-to-diagonal argument.
7. ThresholdSobolevFEMRecoveryData packages assumptions rather than proving positive smooth density, concrete FEM conformity, or interpolation estimates.
8. Finite, assembled, and abstract theorems do not overstate the moving Sobolev PDE/FEM result.
9. Produce an exact table: fully formalized, reduced to assumptions, or not formalized.
10. For PR #117, verify the nested Hilbert recovery inequality and strong-convergence transfer are statement-faithful and genuinely additive rather than duplicative.

Deliverable

A public report with build commands, commit hash, theorem names, axiom output, and a PASS, PASS AFTER CORRECTION, or FAIL statement-faithfulness verdict.

Internal scope label

FUN BUX: 2,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.

Check out review/bernstein-obstacle-v4-final at commit 61594952ad880d2b61759cfa93a19df979183c09 and begin by reproducing the pinned Lean/mathlib workflow. Inspect ScheduledRecovery.lean and ThresholdSobolevFEMRecoveryData, then review the listed theorem layers and PR #117 against the manuscript. Done means a public report with build details, theorem names, axiom output, an exact formalization-status table, and a verdict.