[ImprobableTruth]

This is the fault of sloppy language. In Lean, _proofs_ (equivalent to functions) and _proof objects/certificates_ (values) need to be distinguished. You can't compute proofs, only proof objects. In the above quote, replace "proof" with "certificate" and you'll see that it's a perfectly valid (if trivial - it essentially just applies a lemma) proof.

[almostgotcaught]

a distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.