CI regenerate-main check

ci_regenerate_main_check

Submitter: Kim Morrison.

Notes: Internal trivial problem used to exercise the regenerate-main workflow end-to-end.

Source: Internal CI check.

Informal solution: True is true.

theorem declaration uses `sorry`ci_regenerate_main_check : True := by⊢ True
  sorryAll goals completed! 🐙

Solved by

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)