def definition def or abbrev

`solutionDecidable`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  90noncomputable def solutionDecidable (inst : BJSSInstance) (w : BJSSWitness inst) :
  91    Decidable (isSolution inst w) := by

Definition body.

  92  classical
  93  exact inferInstance
  94
  95/-- Ordinary subset-sum embeds by using zero residues, zero rungs, and zero
  96cost bound. -/

Lean names referenced from this declaration's body.

BJSSInstance in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
BJSSWitness in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
isSolution in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
isSolution in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use