module module

`IndisputableMonolith.Cryptography.BalancedJSubsetSum`

show as: view Lean formalization →

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

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (19)

def rungValue L26
theorem rungValue_pos L28
theorem rungValue_zero L32
structure BJSSInstance L37
structure BJSSWitness L46
def weightSum L50
def residueSum L54
def rungCost L58
def totalJCost L62
def weightTarget L65
def residueNeutral L68
def jCostBound L71
def isSolution L75
theorem rungCost_nonneg L78
theorem totalJCost_nonneg L83
def solutionDecidable L90
def fromSubsetSum L97
theorem fromSubsetSum_totalJCost_zero L105
theorem fromSubsetSum_isSolution L111