Jcost

formal source

  27/-! ## Recognition Action -/
  28
  29/-- The J-cost functional J(x) = ½(x + x⁻¹) - 1. -/
  30def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  31
  32/-- J-cost is non-negative for positive x. -/
  33theorem Jcost_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ Jcost x := by
  34  unfold Jcost
  35  have : (x - 1)^2 / (2 * x) ≥ 0 := div_nonneg (sq_nonneg _) (by linarith)
  36  have : (x + x⁻¹) / 2 - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
  37  linarith
  38
  39/-! ## Residual Rate Action -/
  40
  41/-- The residual rate action A for a two-branch geodesic rotation
  42    with separation angle θ_s. A = -ln(sin θ_s) for 0 < θ_s < π/2. -/
  43noncomputable def rate_action (theta_s : ℝ) : ℝ := -Real.log (Real.sin theta_s)
  44
  45/-- Rate action is positive when sin(θ_s) < 1 (i.e., θ_s ≠ π/2). -/
  46theorem rate_action_pos (theta_s : ℝ) (h_sin_pos : 0 < Real.sin theta_s)
  47    (h_sin_lt : Real.sin theta_s < 1) :
  48    0 < rate_action theta_s := by
  49  unfold rate_action
  50  rw [neg_pos]
  51  exact Real.log_neg h_sin_pos h_sin_lt
  52
  53/-! ## The C = 2A Identity -/
  54
  55/-- The recognition action C along a geodesic rotation is TWICE the
  56    residual rate action A. This is the central identity connecting
  57    quantum measurement (Born weights from C) to gravitational
  58    collapse (rate from A).
  59
  60    Derivation: For a geodesic rotation by angle θ_s,