totalJCost
plain-language theorem explainer
The totalJCost definition sums rung costs over the support of a witness in an 8-balanced J-subset sum instance. Cryptographers and information theorists modeling RS-native search costs would cite it when checking bounds or non-negativity. It is realized as a direct finite summation that delegates each term to rungCost.
Claim. Let $I$ be an 8-balanced J-subset sum instance with $n$ items, integer weights, residues in $ZMod 8$, integer rungs, target sum, and real bound. For a witness given by support subset $S$, the total J-cost equals $∑_{i∈S} Jcost(rungValue(I.rung_i))$, where $Jcost$ is the Recognition Science cost function.
background
The module introduces 8-Balanced J-Subset Sum as a deliberately simple RS-native search problem with no security claims. An instance packages finite data: item count $n$, weight map to integers, residue map to $ZMod 8$, rung map to integers, target integer, and cost bound real. A witness is simply a Finset support of indices. rungCost applies Jcost to the rungValue of each selected rung. Upstream totalJCost appears in PhysicsComplexityStructure as the sum of Jcost over ledger ratios and in ShannonEntropy as the sum that equals Shannon entropy.
proof idea
The definition is a one-line wrapper that sums rungCost inst i over i in w.support.
why it matters
This supplies the cost measure invoked by jCostBound to enforce the instance bound, by totalJCost_nonneg to prove non-negativity, and by fromSubsetSum_totalJCost_zero to show ordinary subset sums incur zero cost. It links the cryptography module to information results such as shannon_entropy_equals_expected_jcost, which equates entropy to expected J-cost. In the Recognition framework it instantiates the J-cost summation for discrete search instances, consistent with ledger total J-cost and the phi-ladder cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.