Audit: Deligne's theorem and the unconditional summit

The pinned axiom checks for Deligne’s theorem and the unconditional summit statements. Each #guard_msgs fails the build if the axiom set changes, so the claim that these depend on nothing beyond propext, Classical.choice and Quot.sound is checked rather than asserted.

Deligne's theorem

The summit, unconditionally

Minimum dimensions, growth and padding