Audit: the factorial route to nilpotent-trace vanishing #
The statements and axioms of the factorial obstruction are pinned here. The final check traverses the types and proof bodies of the factorial route, including opaque declarations, and rejects dependencies on the Schur, hook-confinement, trace-zeta or Deligne engines. Imported modules alone do not constitute a proof dependency.
The appendix proof serves as a control: the same traversal must find an excluded dependency in that proof. This audit checks independence of the nilpotent-trace and semisimplicity lemmas. The summit checks require the factorial theorem in their transitive dependencies and exclude the appendix's nilpotent-trace and trace-zeta mechanisms. Schur theory used by Deligne and by the colour bounds is audited separately.