recognition_action

formal source

  63    - Therefore C = 2A identically.
  64
  65    This holds for ALL geodesic rotations, not just specific angles. -/
  66noncomputable def recognition_action (theta_s : ℝ) : ℝ := 2 * rate_action theta_s
  67
  68theorem C_equals_2A (theta_s : ℝ) :
  69    recognition_action theta_s = 2 * rate_action theta_s := rfl
  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|². -/
  80noncomputable def born_weight (C_I : ℝ) : ℝ := Real.exp (-C_I)
  81
  82/-- Born weight is positive. -/
  83theorem born_weight_pos (C_I : ℝ) : 0 < born_weight C_I := Real.exp_pos _
  84
  85/-- For the C = 2A case: born_weight = sin²(θ_s).
  86    This follows from exp(-2A) = exp(2 ln sin θ) = sin²θ. -/
  87theorem born_weight_is_sin_sq (theta_s : ℝ) (h_sin_pos : 0 < Real.sin theta_s) :
  88    born_weight (recognition_action theta_s) =
  89    (Real.sin theta_s) ^ 2 := by
  90  unfold born_weight recognition_action rate_action
  91  rw [show -(2 * -Real.log (Real.sin theta_s)) = 2 * Real.log (Real.sin theta_s) from by ring]
  92  rw [show (2 : ℝ) * Real.log (Real.sin theta_s) =
  93      Real.log ((Real.sin theta_s) ^ 2) from by
  94    rw [Real.log_pow]; ring]
  95  rw [Real.exp_log (sq_pos_of_pos h_sin_pos)]
  96