Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics

A proof checker certifies that a statement is valid, not that it is worth keeping. We ask what a generator can learn about value from an incomplete record of valuable mathematics, starting from one elementary fact: a generator acts only on its information, so everything it can guarantee is decided by the worlds that its information cannot separate. First, a membership verifier localizes: a task judged in the limit is solvable with a verifier exactly when it is solvable inside each formal world, where the verifier is silent. Second, inside a formal world, a record that might be complete leaves value ambiguous. If the record lists $K$ and a larger candidate $K^{\prime }$ is equally consistent with it, every output in $K^{\prime }\setminus K$ is trivia under one reading and a discovery under the other, and the two trade at an exchange rate of exactly one. If $m$ of the first $N$ points of $K^{\prime }$ are recorded, the best coverage of them that can be guaranteed by round $T\ge 2N+2$ is $$\begin{gathered} m/2+\min \\ g(T),N-m \end{gathered}$$ up to $O(\sqrt{N})$, for every trivia budget $g(T)\le \sqrt{T}$ that grows by at most one per round. Guaranteed coverage therefore takes only two values across all trivia regimes: $\alpha /2$ when trivia must stay bounded, and $1-\alpha /2$ when it may grow without bound, however slowly, where $\alpha$ is the relative density of $K$ in $K^{\prime }$. Recovering the unrecorded region takes the inverse budget at its mass, $(1-\alpha -\epsilon {)}^2{N}^2$ rounds under a square-root budget. A description-length model of value realizes $\alpha =0$: bounded trivia guarantees nothing, and every unbounded budget guarantees everything.