C_19: record the unverified upper bounds 0.4395 and 0.423

[CoolRmal]

This updates the Berry–Esseen page ($C_{19}$) with two recent upper bounds, both marked unverified (asterisk), following the convention for bounds whose verification is at a minimal level.

Changes

• constants/19a.md: two new rows in Known upper bounds, two references, and a comment on verification status.
• README.md: the $C_{19}$ upper-bound cell now reads 0.4690 (0.423*), and two lines are added to Recent progress.

The bounds

Bound	Source	Status
$0.4395^*$	H. Xiao and C. Li, haonan-xiao/iid-berry-esseen (10 Sep 2026)	Lean 4 formalization; finite certificates checked with native_decide
$0.423^*$	Y. Lin, CoolRmal/BerryEsseen (13 Sep 2026)	Lean 4 formalization of berryEsseenConstant ≤ 0.423; finite certificates checked with native_decide

For $0.423$: #print axioms on the final theorem reports propext, Classical.choice, Quot.sound and 579 auxiliary axioms introduced by native_decide, with no sorry and no user-declared axiom. The proof builds on the analytic framework of Xiao and Li (moment coordinates, cosine profile, sine-circle and stop-loss estimates, Prawitz normalization) and does not use Shevtsova's published bound. A readable proof document is at paper/upper-0423.pdf in that repository.

Caveats

• Neither bound has been refereed or published, and neither has been checked with leanprover/comparator.
• Both rely on native_decide, so they trust Lean's compiler in addition to its kernel.
• The $0.423$ proof was developed with substantial AI assistance (the underlying computer-assisted argument with OpenAI Codex, the Lean formalization with Claude Code).

Please adjust the wording or the verification marking as you see fit.

🤖 Generated with Claude Code