gi:proof:tao-shortbound
Lean 4 - Proof - Tao ShortBound to Global Regularity
Live version in repository: 0.1.0
Conditional result
This proves OpenObligations.Torus.Tao.core_global_of_shortBound: ShortBound (open premise, not proved here) implies the conclusion. ShortBound is the short-time a-priori bound of T. Tao (arXiv:0710.1604); it is an open premise and is not proved here. mild solutions only, Fourier-side.
Formal statement
Lean declaration name (copyable):
OpenObligations.Torus.Tao.core_global_of_shortBound
Verification metrics
Machine-extracted from the repository at pinned commit 952d19cdaf3b.
| Build jobs | 8,959 |
|---|---|
| Errors | 0 |
| Unproved-declaration warnings | 0 |
| Declarations | 47 (36 theorems + 11 definitions) |
| ECR checks | 11 |
| Axiom-policy checks | 58 |
| Project audit | 544 constants (384 theorems) |
| Token scan | 0 hits in 35 files |
| ECR battery | 36/36 |
| Mutation tests | 4/4 |
| Non-vacuity | proved in Lean (TaoShortBound/ECR.lean) |
Axiom footprint
Every checked declaration depends only on the three standard Lean/Mathlib axioms:
propext Classical.choice Quot.sound
Gates passed
- Axiom-policy — checked on every build (RESULT: PASS, 58 checks).
- ECR battery — 36/36 theorems accepted.
- Mutation tests — 4/4.
- Non-vacuity — proved in Lean (TaoShortBound/ECR.lean).
- Token scan — 0 hits in 35 files.
What this is NOT
- It is not a proof of ShortBound, nor of global regularity or blow-up for Navier-Stokes.
- It is not Fefferman’s statement (A) or (B).
- It is not the converse direction of Tao’s equivalence, nor the whole equivalence.
- It is about mild solutions (Duhamel formulation, coefficientwise, in a Sobolev class), not classical solutions. This package does not prove in Lean that the two notions agree.
- Passing the checks listed below does not show that ShortBound is true or consistent.
Reproduce it yourself
Expected: RESULT: PASS (58 axiom-policy checks)
Tested platform: Linux x86_64 only. See the repository’s rebuild docs for online and offline profiles.
Provenance & credit
The proofs are recorded in the builder’s acceptance records as builder-authored; they were not synthesized by the CHAOS system. The checks (acceptance, ECR battery) were run by the package builder.
- Toolchain
- Lean 4.34.1 · Mathlib d13f23b
- Repository
- kts-global/lean-proofs-tao-shortbound-global-regularity @
952d19cdaf3b - Release
- not yet tagged (release candidate)
Cite
- DOI
- pending
- Wikidata
- pending
- ORCID
- 0009-0008-7130-1448