Certified period-doubling thresholds of the gradient-descent cubic map (1+a)x-ax³, from a₄ to a₅₁₂
Abstract
Fixed-step gradient descent with step size a on the double-well loss 1/4(x²-1)² is the odd cubic map gₐ(x)=(1+a)x-ax³. Hofmann (arXiv:2607.04993) uses it as the scalar core of a hierarchy of solvable learning models: the edge of stability a=1 is its first flip bifurcation, and the period-doubling thresholds aₘ — the parameters at which the attracting m-cycle has multiplier -1 — organise everything past the edge. He proves a₂=sqrt5-1 and prints a₄,a₈,a₁₆,a₃₂ to eight significant digits, "solved numerically", with no error bound; a₄ and a₈ are also algebraic numbers of degrees 32 and 3200 in Zhang's tables for the map rx-x³. We prove, with every step checked by a proof assistant, that for each m ∈ {4,8,16,32,64,128,256,512} there is a parameter aₘ carrying a cycle of exact period m with multiplier exactly -1, that the pair (cycle point, parameter) is the unique one in an explicit closed ball of radius 2⁻¹⁸⁰ (m ≤ 64), 2⁻³⁶⁰, 2⁻⁷⁰⁰ or 2⁻¹⁴⁰⁰ (m=128,256,512), and that aₘ lies in a stated interval of width 10⁻⁴⁸. The values a₆₄,…,a₅₁₂ appear nowhere in the literature we could find, and a₁₆,a₃₂ only to eight digits. From the brackets we obtain the strict ordering sqrt5-1<a₄<…<a₅₁₂ and rigorous enclosures of the first seven Feigenbaum gap ratios (aₘ-a_(m/2))/(a₂ₘ-aₘ), three of them to three decimals and four to six, all below δ=4.6692016… and the seventh within 4 · 10⁻⁶ of it; nothing is claimed about the limit. The certificate is a Krawczyk-type test whose Lipschitz input is obtained by exact divided differences along two orbits, with no calculus, so that a period-n certificate is a recursion of length n over rational intervals; a second period-4 flip parameter at 1.5488… and a root of Zhang's polynomial at 1.9676… are certified as controls that the uniqueness and the algebraic characterisation are local statements.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
d21f7b661afe82607246045d573633b9e22aec59aafefbbc6666598fcf81f8f5
Claim ledger
Stated results
GC1known2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC2known2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC3known2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC4routine2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC5known data2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC6known data2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC7candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC8candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC9candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC10routine2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC11measurement2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
This ledger entry is reported in prose and is not bound to a Lean theorem.GC12routine2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC13routine2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC14candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC15candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC16candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC17candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC18candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC19routine2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC20measurement2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
This ledger entry is reported in prose and is not bound to a Lean theorem.GC21candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
GC22candidate2026-09-03
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Fixed-step gradient descent with learning rate a > 0 on the double-well quartic loss ℓ(x) = ¼(x² − 1)² is the one-dimensional map
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7