pith. machine review for the scientific record. sign in
theorem proved term proof

C_equals_2A

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  68theorem C_equals_2A (theta_s : ℝ) :
  69    recognition_action theta_s = 2 * rate_action theta_s := rfl

proof body

Term-mode proof.

  70
  71/-! ## Born Rule Emergence -/
  72
  73/-- Born weight for outcome I with recognition action C_I:
  74    w_I = exp(-C_I). The probability is w_I / Σ w_J.
  75
  76    With C = 2A and A = -ln(sin θ):
  77    w = exp(-2A) = exp(2 ln sin θ) = sin²θ = |α|²
  78
  79    This IS Born's rule: P(I) = |α_I|². -/

used by (3)

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

depends on (15)

Lean names referenced from this declaration's body.