theorem
proved
term proof
rate_action_pos
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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,
61 - The recognition cost accumulated is C = -2 ln(sin θ_s)
62 - The residual action is A = -ln(sin θ_s)
63 - Therefore C = 2A identically.
64
65 This holds for ALL geodesic rotations, not just specific angles. -/