No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
71def jCostBound (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
proof body
Definition body.
72 totalJCost inst w ≤ inst.bound
73
74/-- Full solution predicate for the finite BJSS problem. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
isSolution
in IndisputableMonolith.Cryptography.BalancedJSubsetSum
decl_use
depends on (6)
Lean names referenced from this declaration's body.
-
BJSSInstance
in IndisputableMonolith.Cryptography.BalancedJSubsetSum
decl_use
-
BJSSWitness
in IndisputableMonolith.Cryptography.BalancedJSubsetSum
decl_use
-
totalJCost
in IndisputableMonolith.Cryptography.BalancedJSubsetSum
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
totalJCost
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
totalJCost
in IndisputableMonolith.Information.ShannonEntropy
decl_use