def definition def or abbrev

`jcostEntangled`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  53noncomputable def jcostEntangled (N : ℕ) (j_single : ℝ) (α : ℝ) : ℝ :=

Definition body.

  54  N * j_single + α * N * (N - 1) / 2
  55
  56/-- **THEOREM**: Entangled states have higher J-cost for large N. -/

From the project-wide theorem graph. These declarations reference this one in their body.

cost_difference_scales_quadratically in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
entangled_higher_cost in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
qm_interpretation_from_ledger in IndisputableMonolith.Quantum.QMInterpretationStructure decl_use
qm_interpretation_implies_cost_gap in IndisputableMonolith.Quantum.QMInterpretationStructure decl_use

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use