`qm_interpretation_structure`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.QMInterpretationStructure
domain: Quantum
line: 14 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.QMInterpretationStructure on GitHub at line 14.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  11def qm_interpretation_from_ledger : Prop :=
  12  ∀ N : ℕ, N > 1 → jcostEntangled N 1 1 > jcostProduct N 1
  13
  14theorem qm_interpretation_structure : qm_interpretation_from_ledger := by
  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. -/
  19theorem qm_interpretation_implies_cost_gap (h : qm_interpretation_from_ledger)
  20    (N : ℕ) (hN : N > 1) :
  21    jcostEntangled N 1 1 > jcostProduct N 1 :=
  22  h N hN
  23
  24end QMInterpretationStructure
  25end Quantum
  26end IndisputableMonolith

papers checked against this theorem

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