AI-assisted sharp support criterion for variance-proxy sub-Gaussian laws

The support-criterion project reports that any symmetric real probability law with 0<a≤|X|≤b almost surely and b/a≤√3+√2 satisfies E exp(tX)≤exp(t² E[X²]/2). The inequality is strict for nonzero t, the variance proxy is optimal, and every larger universal support ratio admits a symmetric four-point counterexample.

Sources for this record

What was already known

Necessary cumulant tests and sufficient moment conditions were known. Equal-variance mixture closure does not establish this criterion for varying amplitudes, and a sharp fourth-moment threshold alone does not prove the full moment-generating-function bound.

AI involvement AI-centered

JD Jones directed the project; the disclosure attributes proposal and proof development to AI collaboration, Codex formalization, and GPT assistance with sharper gap and transport statements.

The disclosure identifies a model-supplied sharp eighth-order certificate and global affine-transport argument; this is more specific than the legacy generic assistance label.

Importance Notable

A sharp, distribution-independent criterion converts an annular support restriction into strict sub-Gaussian concentration with the actual variance.

Limitations

The law must be symmetric and bounded away from zero; this is not a criterion for arbitrary bounded or nonsymmetric distributions. Novelty is supported by the project’s bounded literature comparison, not an exhaustive literature review. The disclosed reviewers are automated; separate author-produced checkers are not outside researcher assessments. AIProofWatch has not run the formal proof or audited all dependencies. The reported date records the registry checkpoint, not an established first discovery date.

Technical verification Formal (Lean)

A completed rigorous check is documented for the scoped statement. Palomar: Lean, NanoDa and con-ron (reported): SupportCriterion.universal_support_criterion, universal_strict, variance_proxy_optimality and sharp_universal_ratio at f6185744e26f5862fd704ef637ebef3fd068cef5; only propext, Quot.sound and Classical.choice permitted.

Formal checking

Reported mechanical checking of the stated scope; not reproduced by AIProofWatch and not human peer review.

Checker
Palomar: Lean, NanoDa and con-ron (reported)
Scope
SupportCriterion.universal_support_criterion, universal_strict, variance_proxy_optimality and sharp_universal_ratio at f6185744e26f5862fd704ef637ebef3fd068cef5; only propext, Quot.sound and Classical.choice permitted.
Basis
Reported by the linked checker
Check date
2026-10-14
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Few is the default when evidence for a higher level is insufficient. No sufficient account of a named human explaining the scoped central reasoning is established in this assessment. Missing disclosure is not evidence of little understanding.

Correction and publication history

2026-10-15 · publication

Primary statement, prior work, AI contribution and evidence scope reviewed on 15 October 2026 against the complete current catalog and revision state. New scoped contribution; ordinary notifying editor publication.

Read this published revision