• Confirm the trace category is small and finite.
  • Confirm each fiber is a Heyting algebra.
  • Confirm stabilizer and drift are monotone and commute.
  • Confirm fixed fibers match the toy model.
  • Confirm the closure sequence matches the golden output.