5.4 What this gives a Stanley reader
Every result in this blueprint is kernel-checked and axiom-free. The two headline theorems above (5.4 and 5.3) report “Closed under the global context” via Rocq’s Print Assumptions; coqchk on the maintained library reports “Modules were successfully checked”.
In particular, the path
\[ \ref{def:descent_set} \; \to \; \ref{def:beta} \; \to \; \ref{thm:phi_w_apply_psis} \; \to \; \ref{thm:phi_w_support_general} \; \to \; \ref{thm:fact3} \; \to \; \ref{prop:omega_proper_beta_lt} \; \to \; \ref{cor:beta_alt_max} \]
is fully formalized with no Admitted and no postulated axioms beyond Rocq’s standard core.