theorem CommunicativeArithmeticGuard.authorized_irreversible_output_is_exact
theorem CommunicativeArithmeticGuard.authorized_irreversible_output_is_exact
: ∀ (boundary : Boundary) (backend : Backend),
  irreversible boundary → authorized boundary backend → backend = Backend.exact