def definition def or abbrev

`totalJCost`

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

formal statement (Lean)

  62def totalJCost (inst : BJSSInstance) (w : BJSSWitness inst) : ℝ :=

Definition body.

  63  ∑ i ∈ w.support, rungCost inst i
  64

From the project-wide theorem graph. These declarations reference this one in their body.

fromSubsetSum_isSolution in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
fromSubsetSum_totalJCost_zero in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
jCostBound in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
totalJCost_nonneg in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
shannon_entropy_equals_expected_jcost in IndisputableMonolith.Information.InformationIsLedger decl_use
balanced_config_zero_cost in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
totalJCost in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
total_jcost_nonneg in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
verification_equivalence in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
entropy_is_expected_surprisal in IndisputableMonolith.Information.ShannonEntropy decl_use
shannon_equals_jcost in IndisputableMonolith.Information.ShannonEntropy decl_use
totalJCost in IndisputableMonolith.Information.ShannonEntropy decl_use

Lean names referenced from this declaration's body.

BJSSInstance in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
BJSSWitness in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
rungCost in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
totalJCost in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
totalJCost in IndisputableMonolith.Information.ShannonEntropy decl_use