Bizarre Contract Violation in Judgment

I have a judgement with the following contract:

(define-judgment-form DynamicLam
  #:mode     (down I I O O)
  #:contract (down Γ e Γ e)

  [----------------"Lambda"
   (down Γ_0 z_0 Γ_0 z_0)]
  ;; rest of the code ...
)

When I run this:

(define empty (term ()))
(redex-match? DynamicLam Γ empty)
(redex-match? DynamicLam e lam1^*)
(redex-match? DynamicLam z lam1^*)
(judgment-holds (down empty lam1^* empty lam1^*))

I get back:

#t

#t

#t

. . down: judgment input values do not match its contract; (unknown output values indicated by _) contract: (down Γ e Γ e) values: (down empty lam1^* _ _)

But this does not make sense, because I clearly used redex-match? above to test:

• That empty matches Γ
• That lam1^* matches e
• And furthermore that lam1^* matches z.

What am I missing? Is there more to the meaning of #:contract than just matching Γ e Γ e?

I solved the problem by changing the #:mode to (down I I I I) instead of (down I I O O), and changing

(judgment-holds (down empty lam1^* empty lam1^*))

to

(judgment-holds (down ,empty ,lam1^* ,empty ,lam1^*))

The , change makes a lot of sense to me but I still do not understand why the two outputs needed to be inputs, so if someone can either edit this answer to explain that, or provide a comment or another answer explaining that subtlety, that would be fantastic.