expectedCost
plain-language theorem explainer
Expected J-cost for a quantum state is the sum of each ledger configuration's total cost weighted by its Born probability. Researchers deriving quantum mechanics from Recognition Science ledger costs cite this when linking superpositions to observable costs. The definition is a direct summation over the finite set of configurations using the probability and total cost functions.
Claim. Let $ψ$ be a normalized quantum state over $n$ ledger configurations. The expected J-cost is $∑_{i} p_i ⋅ C(L_i)$, where $p_i$ is the Born probability of configuration $L_i$ and $C$ denotes the total cost functional on ledger entries.
background
The Quantum Ledger module treats quantum states as superpositions over ledger configurations, each carrying a J-cost. A quantum state consists of a finite list of ledger configurations together with complex amplitudes that sum in squared norm to one. The module doc states that quantum states are ledger superpositions and that the Born rule emerges from J-cost minimization rather than being postulated. Upstream, total cost is the sum of bit-normalized J-cost and curvature J-cost; J-cost itself is the cost assigned to any recognition event.
proof idea
The definition is a direct one-line sum that applies the probability function to each index and multiplies by the total cost of the corresponding configuration.
why it matters
This definition supplies the left-hand side for the born_rule_jcost_connection theorem, which states that the expected cost equals the probability-weighted sum and interprets the Born rule as cost-weighted selection. It advances the formal connection between ledger costs and quantum probabilities outlined in the RS_FORMALIZATION_ROBUSTNESS plan. In the framework it supports deriving the Born rule from the variational principle that minimizes expected J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.