theorem
proved
term proof
qm_interpretation_structure
show as:
view Lean formalization →
formal statement (Lean)
14theorem qm_interpretation_structure : qm_interpretation_from_ledger := by
proof body
Term-mode proof.
15 intro N hN
16 simpa using entangled_higher_cost N hN 1 1 (by norm_num)
17
18/-- QM-interpretation structure implies entangled J-cost exceeds product J-cost. -/