 167/-! ## Born Rule from J-Cost Minimization -/
 168
 169/-- The expected J-cost of a quantum state. -/
 170noncomputable def expectedCost {n : ℕ} (ψ : QuantumState n) : ℝ :=
 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)). -/
 181theorem born_rule_jcost_connection {n : ℕ} (ψ : QuantumState n) :
 182    -- The expected cost is a weighted average of configuration costs
 183    expectedCost ψ = Finset.univ.sum fun i => probability ψ i * totalCost (ψ.configurations i) :=
 184  rfl
 185
 186/-! ## 8-Tick Phase in Quantum Ledger -/
 187
 188/-- The phase factor for a ledger entry. -/
 189noncomputable def entryPhase (e : LedgerEntry) : ℂ :=
 190  EightTick.phaseExp e.phase
 191
 192/-- The total phase of a ledger (product of entry phases). -/
 193noncomputable def ledgerPhase (L : Ledger) : ℂ :=
 194  (L.entries.map entryPhase).prod
 195
 196/-- An empty ledger has phase 1. -/
 197theorem empty_ledger_phase : ledgerPhase emptyLedger = 1 := by
 198  simp [ledgerPhase, emptyLedger]
 199
 200/-- **8-TICK INTERFERENCE**: When summing over all 8 phase configurations

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.