born_rule_jcost_connection
plain-language theorem explainer
The theorem states that the expected J-cost of a quantum state equals the sum of Born probabilities times the total costs of its ledger configurations, encoding the Born rule as cost-weighted selection. Researchers deriving quantum mechanics from recognition events would cite it to link variational J-cost minimization to probability amplitudes. The equality holds by direct reflexivity on the definitions of expectedCost and probability inside the QuantumState structure.
Claim. For a quantum state $ψ$ over $n$ ledger configurations, the expected J-cost satisfies $E[Cost(ψ)] = ∑_i p_i · totalCost(L_i)$, where $p_i$ denotes the Born probability of configuration $L_i$ drawn from the normalized amplitudes and totalCost is the J-cost functional on ledger entries.
background
QuantumState is defined as a structure holding a finite set of Ledger configurations, complex amplitudes, and a normalization condition ensuring the sum of squared norms equals one. Probability for each index is the squared modulus of the corresponding amplitude, implementing the Born rule directly from the ledger superposition. Total cost of a configuration is supplied by upstream definitions such as totalCost from LambdaRecDerivation, which combines normalized bit cost with curvature cost, and cost from ObserverForcing, which extracts J-cost of the recognition event state.
proof idea
The proof is a one-line reflexivity that unfolds the definition of expectedCost as the probability-weighted sum over the configurations field of the QuantumState structure.
why it matters
This declaration supplies the explicit bridge between the Recognition Science ledger and quantum states, showing that the Born rule emerges from J-cost minimization rather than being added by hand. It supports the module's claim that quantum states are ledger superpositions and aligns with the variational principle described in the module doc-comment. No direct downstream uses are recorded, yet it closes a required step toward deriving measurement collapse to minimum-J-cost configurations within the eight-tick and phi-ladder framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.