We investigate growth dynamics in deterministic equational discovery substrates. Across three toy domains (arithmetic, boolean, higher-order list; n=592 trajectories), short-range substrate sizes fit a power-law N(t) proportional to t^b. Within each substrate b is architecture-sensitive (cross-validated R^2 approximately 0.82); the regression does not transfer across substrates (arith+bool to list yields R^2 approximately -0.84). A heuristic mean-field closure model predicts a saturating power-law dN/dt = K N^k exp(-mu N) of which the pure power-law is the short-range approximation. Three robustness checks: bootstrap intervals on (k, mu) are tight in 4/5 toy trajectories and degenerate in 1/5; out-of-sample forecasting on toy data (fit first 100 epochs, predict next 400) is won by pure power-law 5/5, indicating the toy trajectories do not reach saturation; on two real-world growth proxies the result splits. New Mathlib/*.lean file additions per month (mathlib4, 60 months, 9701 files) support the saturating form on OOS forecasting by approximately 7x over pure power-law; Coq mathcomp monthly commits (129 months, 3083 commits) favour pure power-law on both tests with mu collapsing to zero. The dynamics are substrate-conditional at two levels: within-substrate architecture-to-b regressions do not transfer, and the preferred functional family for N(t) itself (pure vs. saturating power-law) differs by substrate. We propose "saturating power-law growth with substrate-conditional (k, mu), observable when the substrate has reached its saturation regime" as a working framing.

翻译：我们研究确定性等式发现基底中的增长动力学。在三个玩具领域（算术、布尔、高阶列表；n=592条轨迹）中，短程基底规模服从幂律N(t) ∝ t^b。在每个基底内，b对架构敏感（交叉验证R²约0.82）；该回归在不同基底间不具迁移性（算术+布尔到列表的R²约-0.84）。一种启发式平均场封闭模型预测饱和幂律dN/dt = K N^k exp(-μ N)，其中纯幂律为其短程近似。三项稳健性检验显示：(i) 5条玩具轨迹中有4条的(k, μ)自助法区间紧凑，1条退化；(ii) 对玩具数据的样本外预测（拟合前100个epoch，预测后400个）中纯幂律5/5胜出，表明玩具轨迹未达到饱和；(iii) 在两项真实世界增长代理变量上结果出现分化。每月新增Mathlib/*.lean文件数（mathlib4，60个月，9701个文件）在样本外预测中支持饱和形式的程度约为纯幂律的7倍；Coq mathcomp每月提交量（129个月，3083次提交）则在两项检验中均偏向纯幂律，且μ坍缩至零。该动力学在两个层面具有基底条件性：基底内架构-b回归不可迁移，且N(t)的优选函数族（纯幂律vs饱和幂律）因基底而异。我们提出“具有基底条件性(k, μ)的饱和幂律增长，当基底达到其饱和区域时可观测”作为工作框架。