New frequency sets aim to capture every signal
- What it is
- A paper claims new frequency sets that can reconstruct every signal in broad classes, with the main statements formalized in Lean.
- Who did it
- Susanna Bertolini, Enric Florit-Simon, Lukas Liehr, and Mitchell A. Taylor
- What it could mean
- Fourier analysis asks what samples retain enough information to recover a signal. If the formalization matches the paper, it offers both new constructions and a machine-checkable route through delicate analytic claims.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Universal completeness of exponentials ↗See the proposed checks
In a separate ephemeral environment, source-lock the cited repository and toolchain, reproduce the five declarations and inspect their axiom closure; then compare the formal statements with Theorems 1.1–1.4 and the stated (L^p), density, and measurability hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The abstract claims uniformly discrete density-one frequency sets complete in every (L^p(S)) for (|S|<1), density-(v) integer-frequency counterparts for (|S|<v), and sharpness of a Sobolev threshold. Section 7 describes a Lean formalization of the results. This is a newly posted mathematical result that also makes its checking boundary inspectable.
- Why this could matter
- New frequency sets aim to capture every signal A signal can be rebuilt from frequencies only when they carry enough information. This paper proposes unusual sparse-looking sets that still capture every function in stated classes, then records key claims in Lean for machines to check.
- If it holds up
- Methods: the constructions would extend the map of when frequency samples determine a function, while the formalization supplies a reusable example of checking advanced analysis with software.
- If it does not
- A replay or alignment examination would isolate whether the frequency construction, analytic assumptions, or formal statement is too strong.
- Impact horizon
- Methods · Harmonic analysis · Formal verification · Fourier analysis
- Version
- submitted 2026-09-17 17:58:15 UTC
- Why we tracked it
- a fresh analysis result with a public Lean formalization. The primary source reports compilation, but State of Proof has not replayed the package or checked paper-to-Lean correspondence.
- Highest-risk dependency
- A compiling endpoint can establish only its exact formal declarations and trusted axioms; it does not automatically establish that every analytic hypothesis, novelty claim, or prose conclusion in the paper is represented.
- Available artifacts
- The arXiv record links UniversalCompleteness; Section 7 states that five public Lean theorems compile under Lean 4.31.0. No repository was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started.