finding record / formal-conjectures
recordedvf_c03cbaf64b74017f
vf_c03cbaf64b74017f
Canonical assertion
The Lean 4 theorem `erdos_1150.variants.parseval_lower_bound` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): for every polynomial P over ℂ of degree n whose coefficients (indices 0..n) all lie in {-1, 1}, the supremum of |P(z)| over the unit circle |z| = 1 is at least √(n+1). This closes a previously-open `sorry` (category: textbook) attached to Erdős Problem 1150 in google-deepmind/formal-conjectures.
Notation is rendered from the stored source. The pinned checkout remains the exact record.
- model_output
- theoretical
- 1 spans
- recorded
Scope and conditions
theoretical
domain:complex_analysis; verifier:lean4_kernel; category:textbook; result:lower_bound_sqrt_n_plus_1; open_sorry_closed:true
Provenance summary
- cap_34c4f0e25c5b7011 · vc_8e5b83b719f1b2be
- model_output
- Jun 14, 2026, 12:00 AM
- not recorded
- 1
Exact record identityFinding ID, frontier identity, and pinned Git source
- vf_c03cbaf64b74017f
- vfr_97d7d25957384f80
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- a24f2c67b52a5b3c9163438243b95351bbc8e296
Exact source and rootsGit 2705e4db4ffb and content-addressed ledgers
Source identity
- Commit
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- Tree
- a24f2c67b52a5b3c9163438243b95351bbc8e296
- Committed
- 2026-07-19T05:13:20Z
- Repository
- Open source
Content roots
- Event log
- sha256:c4a00883ab7468dcce59c368b81fd09e45366b21af8e34979d7a639d73a8d32c
- Snapshot
- sha256:45fa712bd6d9a8d4c8514a7cba107e7f814f2c1368805abd577e762ccb6123a4
- Proposals
- sha256:ba47ddf5c16ed567ddf835385066e3fc294b447bc0eabd3f9820f5e707efb39e
- Actor registry
- sha256:f52d59b1db885f467c66a29335ada68544a09da5f3869723461100eed0aac79e
- Artifacts
- sha256:fbd7e05b185cd06bc06484e8b0216c17c5263a71d8481ca38e574e9b2c5156d8