The Grokking Nucleation Theorem: A Classical-Nucleation-Theory Account of the Grokking Transition and a Goldilocks Temperature

Series S6 (Cognition & Learning) of the Viridis Canon. The core Intelligence-Bound canon spine is unchanged (frozen at v10.1.0 “The Keystone Wave”, record 21223021); this record links to the spine via isDerivedFrom the concept DOI 10.5281/zenodo.19317982, and references the S6 series anchor (concept 10.5281/zenodo.21002783). “Grokking” — a neural network's sudden jump from memorization to generalization long after training loss has plateaued — has resisted a first-principles account of *why* the delay exists and *why* it is non-monotone in an effective temperature (learning rate / weight decay ratio, or similar control). The Grokking Nucleation Theorem (GNT) models generalization as a classical-nucleation-theory phase transition: a generalizing sub-network must cross a barrier set by a competition between a driving force Δ and a surface-tension-like cost σ, exactly the same mathematical structure already certified elsewhere in the Viridis canon for reforestation (the Forest Nucleation Theorem and Afforestation Stewardship Theorem). GNT proves the resulting nucleation barrier matches the classical form, identifies the critical nucleus size, and — the headline result — proves the existence of a unique interior Goldilocks temperature T* at which the expected grokking delay is minimized, with the delay strictly convex and non-monotone around that optimum. Five results are machine-checked in Lean 4 (zero sorry, axioms ⊆ {propext, Classical.choice, Quot.sound}), module GrokkingNucleation.lean: (i) gnt_barrier_eq_cnt — the nucleation barrier takes the classical CNT closed form; (ii) gnt_critical_point — the critical nucleus size is a stationary point of the driving/tension competition; (iii) tau_grok_nonmonotone_unique_min — existence and uniqueness of an interior Goldilocks temperature minimizing expected grokking delay, via strict convexity; (iv) nucleation_ib_floor — a combined kinetic/information-generation floor on grokking delay, monotone in the information-generation term; (v) gnt_nonvacuous — an explicit interior witness. GNT joins the S6 Cognition & Learning cluster (Cognitive Throughput / Dissipative Generalization / Mutualistic Entropy Learning / Harmonized Descent) as a downstream application of nucleation-theory machinery to a deep-learning phenomenon, rather than a domain-defining extension of the Intelligence Bound itself — hence series (not spine) routing. Scope. The Lean proofs certify the validity of the reasoning, not empirical magnitudes. Working paper; not peer-reviewed.