Maximal non-atomic join-irreducibles and Frankl's conjecture for upper semimodular lattices

Let L be a finite upper semimodular lattice. We prove the lattice form of Frankl's union-closed sets conjecture whenever the poset of non-atomic join-irreducible elements has at most three maximal elements. This hypothesis is strictly weaker than requiring at most three non-atomic join-irreducibles, and is also strictly weaker than requiring their width to be at most three. The proof is based on reconstruction injections from principal filters. Its main local ingredients are a relative Boolean deletion lemma and a derivation-core inequality for finite upper semimodular lattices. We also prove a more general criterion involving an essential maximal non-atomic branch. As a consequence, any hypothetical upper semimodular counterexample must have at least four maximal non-atomic branches, with each branch lying below the join of all the others. The main theorem has been completely formalized in Lean 4.31.0 against a fixed Mathlib revision. The supplementary material contains the Lean source, pinned toolchain and Mathlib revision, exact regression scripts, finite verification certificates, and a clean-build verification entry point. This record contains a preprint version of the manuscript together with its supplementary formal-verification materials.