Negative inertial mass cannot make gravity a negative-index medium

import Mathlib

/-! The gravitoelectromagnetic constants carry the sign of G.

    εg = 1/(4πG) and μg = 4πG/c².  For any c ≠ 0 each is positive exactly when
    G is.  Nothing about the sources appears in either statement, so no choice
    of source term can move them. -/

theorem eps_g_sign (G : ℝ) : 0 < 1 / (4 * Real.pi * G) ↔ 0 < G := by
  have hpi : (0:ℝ) < 4 * Real.pi := by positivity
  rw [one_div_pos]
  constructor
  · intro h; nlinarith
  · intro h; nlinarith

theorem mu_g_sign (G c : ℝ) (hc : c ≠ 0) :
    0 < 4 * Real.pi * G / c ^ 2 ↔ 0 < G := by
  have hpi : (0:ℝ) < 4 * Real.pi := by positivity
  have hc2 : (0:ℝ) < c ^ 2 := by positivity
  rw [div_pos_iff]
  constructor
  · rintro (⟨h, _⟩ | ⟨_, h⟩)
    · nlinarith
    · nlinarith
  · intro h; exact Or.inl ⟨by nlinarith, hc2⟩

# Dimensions as exponent vectors over (m, kg, s). No physics in here: this
# checks only that the stated dimensions are not the dimensions of G.
def mul(a, b): return tuple(x + y for x, y in zip(a, b))
def div(a, b): return tuple(x - y for x, y in zip(a, b))

def show(v):
    names = ('m', 'kg', 's')
    num = ' '.join(n if e == 1 else f'{n}^{e}' for n, e in zip(names, v) if e > 0)
    den = ' '.join(n if e == -1 else f'{n}^{-e}' for n, e in zip(names, v) if e < 0)
    if not den:
        return num or '1'
    return f'{num or 1} / ' + (f'({den})' if ' ' in den else den)

ONE = (0, 0, 0)
G   = (3, -1, -2)                   # m^3 / (kg s^2), by definition of G
c   = (1,  0, -1)
eps = div(ONE, G)                   # eps_g = 1/(4 pi G);   4 pi is dimensionless
mu  = div(G, mul(c, c))             # mu_g  = 4 pi G / c^2

phi = (2, 0, -2)                    # GEM scalar potential, m^2/s^2
phidot = div(phi, (0, 0, 1))
candidates = [
    ('r_i / m_i',                        (1, -1, 0)),
    ('[phidot_g mu_g], as stated',       (3, -1, -1)),
    ('[phidot_g mu_g], from phi_g=m^2/s^2', mul(phidot, mu)),
]

print(f'[G]     = {show(G)}')
print(f'[eps_g] = {show(eps)}')
print(f'[mu_g]  = {show(mu)}')
print()
for name, v in candidates:
    print(f'{name:38s} = {show(v):18s} {"== [G]" if v == G else "!= [G]"}')
print()
print('[mu_g] == [r_i/m_i]:', mu == (1, -1, 0))
print('any candidate has the dimensions of G:', any(v == G for _, v in candidates))

[G]     = m^3 / (kg s^2)
[eps_g] = kg s^2 / m^3
[mu_g]  = m / kg

r_i / m_i                              = m / kg             != [G]
[phidot_g mu_g], as stated             = m^3 / (kg s)       != [G]
[phidot_g mu_g], from phi_g=m^2/s^2    = m^3 / (kg s^3)     != [G]

[mu_g] == [r_i/m_i]: True
any candidate has the dimensions of G: False