Noether–Lefschetz Vanishing for Hypersurfaces in P^5 as an Explicit Hypothesis: A Machine-Checked Lean 4 Interface

A Lean 4 record of the propositional form of Noether–Lefschetz vanishing for very general hypersurfaces of degree d≥3 in P^5. Hypersurfaces are abstract records with predicates. Proved, conditional on the vanishing sentence: an extra class on such a hypersurface gives a contradiction, there is no extra class for degree ≥6, and in a second encoding the d≥3 sentence implies its d≥6 case (where the predicate Hdg^2=Q h^2 is a placeholder defined as True). Not formalized: Beauville's monodromy theorem and Deligne's invariance argument. All results are conditional. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/NoetherLefschetz at commit a96b7e01392010bee63fb2d4ab42674baf21ec78.