carlok — zsh — 88×30

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.