author: nadermx

body: Plain reply, no maths at all — most comments look like this.


body: Replies nest. Inline maths works here too: the partial sums $\sum_{n=1}^{N} 1/n^2$ approach $\pi^2/6$ from below, which is why the numerical check further down is one-sided.


body:
And a comment can ask the server for a number rather than assert one. The output below is what actually ran:

```python
s = sum(1.0 / n**2 for n in range(1, 200001))
(s, 3.141592653589793**2 / 6)
```

badge: ran

output: (1.6449290668607264, 1.6449340668482264)

status: ok

tool: python


body: A separate top-level reply, to show the tree rather than one straight line.


body:
Both checkable halves, checked.

The sign lemma carries no physics: εg and μg are positive exactly when G is, for any c ≠ 0. Nothing about a source appears in either statement, so nothing a source does can move them.

```lean
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⟩
```

The dimensional step, taking the stated dimensions as given:

```python
# 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] and [rᵢ/mᵢ] coincide — presumably where the identification comes from — and neither is [G].

Not checked: that ±mi leaves G alone. That is a claim about which symbols appear in the field equations, not a claim about ℝ, and it stays prose until the model itself is formalised.

badge: proved

tool: lean

output:
[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


body:
The arithmetic of the fork, checked. The physics is not, and cannot be — the charge assignment, the anomaly cancellation and the seesaw reconstruction are statements about a model, not about ℤ.

```lean
import Mathlib

/-! The arithmetic of the fork — the part a kernel can see.

    The ΔL = 2 bilinears carry X-charge −6, and a `Z_N` remnant shifts a charge
    only by multiples of N.  So a Majorana operator survives exactly when
    `N ∣ 6`: `N = 6` allows it, `N = 12` forbids it to all orders, and the
    holonomy test that would certify Dirac is exactly `2q ≠ 0`. -/

/-- Dressing a −6 bilinear with powers of `Φ_N` can reach charge zero iff N ∣ 6. -/
theorem majorana_survives_iff (N : ℤ) : (∃ k : ℤ, -6 + N * k = 0) ↔ N ∣ 6 := by
  constructor
  · rintro ⟨k, hk⟩
    exact ⟨k, by linarith⟩
  · rintro ⟨k, hk⟩
    exact ⟨k, by linarith⟩

theorem allowed_at_six : ∃ k : ℤ, -6 + 6 * k = 0 := ⟨1, by norm_num⟩

/-- Not "not yet seen": no integer k works, so the operator is absent to all orders. -/
theorem forbidden_at_twelve : ¬ ∃ k : ℤ, -6 + 12 * k = 0 := by
  rintro ⟨k, hk⟩
  omega

/-- In the `Z_N` remnant a charge is its own conjugate exactly when `2q = 0`. -/
theorem self_conjugate_iff (N : ℕ) (q : ZMod N) : q = -q ↔ 2 * q = 0 := by
  rw [two_mul, eq_neg_iff_add_eq_zero]

/-- At q = −3 in `Z_12` it is not, which is what a Dirac certificate would measure. -/
theorem neutrino_is_not_self_conjugate : (-3 : ZMod 12) ≠ -(-3 : ZMod 12) := by
  decide
```

Three things that survive the kernel, and are worth separating from the prose around them:

1. `N ∣ 6` really is the whole criterion — the existence of a dressing that lands on charge zero is *equivalent* to the divisibility, not merely implied by it.
2. `N = 12` forbids the operator **to all orders**, not "not yet observed": `omega` rules out every integer `k`, which is the difference between a selection rule and a null result.
3. The Dirac certificate is exactly `2q = 0` — a charge is its own conjugate in the remnant iff its double vanishes — and at `q = −3` in `Z₁₂` it does not.

Not checked, because a kernel has no opinion on them: that the ΔL = 2 bilinears carry charge −6, that both branches are anomaly-free, and that the Majorana-side Dirac mass returns the same light masses as the Dirac-side one. That is where the physics is.