kappa_ne_zero

formal source

  48theorem kappa_rs_closed_form : kappa_rs = 8 * phi ^ 5 := rfl
  49
  50/-- The derived Einstein coupling cannot vanish. -/
  51theorem kappa_ne_zero : kappa_rs ≠ 0 := ne_of_gt kappa_pos
  52
  53/-! ## The Equivalence Principle -/
  54
  55/-- **G-003 Resolution**: The equivalence principle is automatic.
  56
  57    In RS, all mass comes from J-cost defect. Both "inertial mass"
  58    (resistance to state change, from J''(1) = 1) and "gravitational mass"
  59    (source of curvature, from J(x) itself) are computed from the SAME
  60    unique cost function J(x) = ½(x + x⁻¹) − 1.
  61
  62    Since J is the unique solution to the RCL (T5), there is only one
  63    notion of mass. The equivalence principle is forced by cost uniqueness.
  64
  65    The formal content: J is symmetric (J(x) = J(1/x)), has unique minimum
  66    at x = 1, and its second derivative J''(1) = 1 is universal — the same
  67    for ALL bodies regardless of composition. This universality IS the EP.
  68
  69    See also: EquivalencePrinciple.lean for the SingleSourceMassTheory
  70    formalization and the rs_equivalence_principle theorem. -/
  71theorem equivalence_principle_automatic :
  72    ∀ x : ℝ, 0 < x → Cost.Jcost x = Cost.Jcost (x⁻¹)⁻¹ := by
  73  intro x hx
  74  have : (x⁻¹)⁻¹ = x := inv_inv x
  75  rw [this]
  76
  77/-! ## Gravity as Emergent Curvature -/
  78
  79/-- Gravitational potential at distance r (in RS units) from a mass M.
  80    Φ(r) = -G·M/r where G is determined by φ. -/
  81noncomputable def gravitational_potential (M r : ℝ) : ℝ :=