cat _posts/2026-08-30-leanfrontier-the-test-was-a-submission-field-note-09.md
LeanFrontier: the test was a submission (Field Note 09)
Field Note 09
— “The Test Was a Submission” — records a deliberately ordinary theorem
contribution exercising the freshly upgraded receiver end to end: local
report, trusted validation, observation, catalogue, and automatic merge. The
submission behind it is
PR #169, adding
natDegree_eq_zero_of_comp_X_add_C_eq_self, the natural-degree consequence of
the existing polynomial translation-rigidity theorem, with the receiver report
returning accepted (the note itself landed as
PR #171). The corpus is at
carlok.github.io/LeanFrontier.