LeanFrontier Field Notes 20 and 21: the diagnostic was the fix, and two measures of building on the corpus

Field Note 20 — The Message Was the Fix — follows the Varignon perimeter submission that had been rejected six times: after the diagnostic was rewritten to say which term it measures, how large the statement is once expanded, and to suggest naming a large subexpression with a definition, the next attempt stated the perimeter as a named definition and was accepted. The note also corrects two published numbers (the pre-registered “imports something recent” column was computed over every module first seen that day, so 32 of 96 rows flip from true to false; the new weekly rejection count had mixed seven weeks of runs at once) and explains Monday’s stalled kernel re-check: asked for one module, the checker checks every module whose name begins with that name, and that one shares its name with a folder of nineteen others.

Field Note 21 — Two Kinds of Building On — lands the two overnight submissions that complete the contributor’s roadmap and separate the two measures the corpus now publishes: the three quadratic subfields of the eighth cyclotomic field build on the corpus twice by imports and not at all by statements, while the Descartes bridge packages the four curvatures as one quadruple and all four reflections as one indexed linear map and builds on it by both. The corpus stands at 104 modules and 83 internal import edges, up from 96 a day earlier.