expectedCost
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.
claimLet $ψ$ 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 in Recognition Science
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.
scope and limits
- Does not derive the probability function from J-cost minimization.
- Does not address continuous or infinite-dimensional states.
- Does not compute explicit numerical values for specific configurations.
- Does not prove ledger conservation under this definition.
formal statement (Lean)
170noncomputable def expectedCost {n : ℕ} (ψ : QuantumState n) : ℝ :=
proof body
Definition body.
171 Finset.univ.sum fun i => probability ψ i * totalCost (ψ.configurations i)
172
173/-- **BORN RULE INTERPRETATION**: The probability of a configuration is
174 inversely related to its J-cost (cost-weighted selection).
175
176 In full RS, this is derived from the variational principle:
177 The observed configuration minimizes expected J-cost subject to constraints.
178
179 Here we state the connection: lower J-cost configurations have higher probability
180 in the cost-optimal distribution (analogous to Boltzmann: P ∝ exp(-βE)). -/