LeanFrontier: five new submissions in a day, from sequences to transcendence

LeanFrontier accepted five more machine-generated submissions in a single day: a greatest sequence below a ceiling with bounded steps, how the greatest-step bounded minorant responds to its constraints, Stedman’s plain changes ringing a full extent, Hermite-Lindemann implying that exp is injective on algebraic numbers, and a generalization of finite-group character sum vanishing to noncommutative rings. The receiver was hardened along the way — submissions now authenticate as the LeanFrontier Receiver app, and the corpus dependency graph is published in the catalogue. The whole day is documented in Field Note 05.