totalJCost
plain-language theorem explainer
The definition aggregates J-cost across all entries of a finite ledger configuration by summing the individual costs of its positive ratios. Information theorists equating entropy to expected cost and cryptographers bounding subset-sum witnesses cite this aggregation when establishing non-negativity or zero-cost solutions. It is realized as a direct finite sum over the configuration vector.
Claim. For a ledger configuration with $N$ positive ratios $r_i$, the total J-cost is $T = sum_{i=1}^N J(r_i)$ where $J(x) = (x + x^{-1})/2 - 1$.
background
LedgerConfig is the structure holding a vector of $N$ positive real ratios, introduced in the IC-005 module on computational complexity of physics from Recognition Science. J-cost is the strictly convex function $J(x) = (x + 1/x)/2 - 1$ with unique minimum at $x=1$, as used throughout the framework for recognition events and cost minimization. The module states that ground-state verification is linear-time while high-rung phi computations are exponential.
proof idea
The definition is a one-line summation that applies the Jcost function to each ratio entry in the LedgerConfig vector.
why it matters
This supplies the total-cost measure referenced by downstream results including shannon_entropy_equals_expected_jcost (equating Shannon entropy to expected J-cost) and the cryptographic totalJCost_nonneg and fromSubsetSum_totalJCost_zero theorems. It occupies the IC-005.9 slot on non-negativity within the J-cost minimization analysis, linking directly to T5 J-uniqueness and the convex ground-state property in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.