author: nadermx

body:
Classic. Stated for Lean so the server can rule on it rather than the comment section.

```lean
import Mathlib
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :=
  (Nat.prime_two).irrational_sqrt
```

And a computation the same server ran:

```python
n = 2**67 - 1
193707721 * 761838257287 == n
```

kind: claim

title: $\sqrt{2}$ is irrational, and the kernel agrees

tools: lean python

badge: proved

status: ok

tool: lean

badge: ran

output: True

tool: python


body:
Mersenne's list said $2^{67}-1$ was prime. Cole factored it in 1903 and reportedly presented the result without speaking a word.

```python
n = 2**67 - 1
a, b = 193707721, 761838257287
(a * b == n, a * b)
```

The output below is what the server actually printed.

kind: text

title: A one-line check that $2^{67}-1$ is composite

output: (True, 147573952589676412927)


body:
The Basel problem has at least fourteen genuinely different proofs. What makes it such a magnet?

Inline maths like $a_i$, $b_j$ and $x_1 \cdot x_2$ must survive markdown intact — underscores are not emphasis here.

title: Why $\sum_{n=1}^{\infty} 1/n^2 = \pi^2/6$ keeps getting new proofs


body:
Wedderburn's little theorem. The striking part is the hypothesis: pure finiteness. Commutativity is assumed nowhere and falls out anyway.

```lean
import Mathlib
theorem finite_division_ring_comm (D : Type*) [DivisionRing D] [Finite D] (a b : D) :
    a * b = b * a :=
  (littleWedderburn D).mul_comm a b
```

title: Every finite division ring is commutative


body:
No formulas, no code — a post can be entirely ordinary. Most of this board is people talking.

Mine is the Cayley–Hamilton theorem: every square matrix satisfies its own characteristic polynomial. It sounds like a curiosity and turns out to be load-bearing everywhere.

title: What is the most under-appreciated theorem in your field?


body:
Left here deliberately so you can see what a rejection looks like. The claim is false and the kernel says so — and what it hands back is the goal it still had open, which is the part worth reading.

```lean
import Mathlib
theorem sqrt_four_irrational : Irrational (Real.sqrt 4) := by
  norm_num
```

title: A wrong proof, kept up on purpose: $\sqrt{4}$ is irrational

badge: refuted

error:
/work/Submission.lean:2:59: error: unsolved goals
⊢ False

output:
/work/Submission.lean:2:59: error: unsolved goals
⊢ False

status: failed


author: mageoftheeast

body:
```python
def colname(x):
    if x == 0:
        return ''
    else:
        (q, rm1) = divmod(x - 1, 26)
        return colname(q) + chr (ord ('A') + rm1)

a = 76686766181
print (colname (a))
print (colname (a) == 'INFINITY')
```

title: Column $76686766181$ in Excel called INFINITY

output:
INFINITY
True


body:
```lean
import Mathlib

theorem testing : ∀ a b c d e : Nat, a + b + c + d + e = (c + (e + d)) + (b + a) := by
  intros
  abel
```

title: A simple proof, hope it works


author: jerryj

body:
import Mathlib

example : 1 + 1 = 2 := by
  norm_num

title: Simple verification test: 1 + 1 = 2


body:
```lean
import Mathlib

example : 1 + 1 = 2 := by
  norm_num
```

title: Simple verification test: 1 + 1 = 2


body:
import Mathlib

example : 1 + 1 = 3 := by
  norm_num

title: Wrong proof test: 1 + 1 = 3


body:
```lean
import Mathlib

example : 1 + 1 = 3 := by
  norm_num
```

title: Wrong proof test: 1 + 1 = 3

error:
/work/Submission.lean:3:23: error: unsolved goals
⊢ False

output:
/work/Submission.lean:3:23: error: unsolved goals
⊢ False


body:
εg = 1/(4πG), μg = 4πG/c² ⇒ sgn(εg) = sgn(μg) = sgn(G).

±mi changes the source terms ρm and Jm, not G; therefore a (+m,−m) lattice cannot make εg, μg < 0 in standard GEM/GR.

[φ̇g μg] = m³/(kg·s) and [ri/mi] = m/kg, but [G] = m³/(kg·s²).

title: Negative inertial mass cannot make gravity a negative-index medium


body:
The Standard Model Lagrangian is usually shown in one of two forms. The compact one fits on three lines:

$$
\begin{aligned}
\mathcal{L}_{\mathrm{SM}} = {} & -\tfrac{1}{4} G^{A}_{\mu\nu} G^{A\mu\nu} - \tfrac{1}{4} W^{I}_{\mu\nu} W^{I\mu\nu} - \tfrac{1}{4} B_{\mu\nu} B^{\mu\nu} \\
& + \sum_{\psi} \bar\psi\, i\gamma^{\mu} D_{\mu} \psi + (D_{\mu}H)^{\dagger} D^{\mu} H - V(H) \\
& - \Big( \bar Q_L Y_u \widetilde{H} u_R + \bar Q_L Y_d H d_R + \bar L_L Y_e H e_R + \text{h.c.} \Big) + \mathcal{L}_{\mathrm{gf}} + \mathcal{L}_{\mathrm{ghost}}.
\end{aligned}
$$

The expanded one — every field written out after electroweak symmetry breaking, in unitary-plus-Goldstone form with Faddeev–Popov ghosts — runs to a full page:

![The fully expanded Standard Model Lagrangian](https://johnathannader.com/media/django-summernote/2026-08-23/standard-model-lagrangian-expanded.jpeg)

Both are correct transcriptions of the same theory. And both are missing something the universe has.

## Read the fermion sector carefully

Look at the third line of the compact form. There are three Yukawa terms: one for up-type quarks ($Y_u$), one for down-type quarks ($Y_d$), one for charged leptons ($Y_e$). There is no $Y_\nu$. There is no right-handed neutrino field $\nu_R$ anywhere in the field content, so there is nothing for a neutrino Yukawa to couple to.

The expanded form makes this even more visible. Every charged fermion gets a kinetic term with a mass:

$$
\bar e^{\sigma}\left(i\gamma^{\mu}\partial_{\mu} - m_e^{\sigma}\right) e^{\sigma}, \qquad
\bar d^{\sigma}_j\left(i\gamma^{\mu}\partial_{\mu} - m_d^{\sigma}\right) d^{\sigma}_j, \qquad
\bar u^{\sigma}_j\left(i\gamma^{\mu}\partial_{\mu} - m_u^{\sigma}\right) u^{\sigma}_j.
$$

The neutrino gets

$$
\bar\nu^{\sigma}\, i\gamma^{\mu}\partial_{\mu}\, \nu^{\sigma}.
$$

No mass. Not a small mass, not an unknown mass — the term is absent by construction, because with only $\nu_L$ in the theory and only renormalizable operators allowed, no gauge-invariant mass term can be written.

## The argument in three steps

1. $\mathcal{L}_{\mathrm{SM}}$ contains no $\nu_R$ and no neutrino-mass operator $\;\Longrightarrow\; m_{\nu_1} = m_{\nu_2} = m_{\nu_3} = 0.$

2. $m_{\nu_i} = 0 \;\Longrightarrow\;$ the mass basis and the flavour basis can be chosen to coincide, so the flavour-change amplitude is
$$
\mathcal{A}_{\alpha\to\beta} = \sum_i U_{\beta i} U^{*}_{\alpha i} = (UU^{\dagger})_{\beta\alpha} = \delta_{\beta\alpha},
$$
and neutrino flavours cannot oscillate.

3. Neutrino flavours demonstrably oscillate $\;\Longrightarrow\; \Delta m^2_{ij} \neq 0 \;\Longrightarrow\;$ contradiction.

Step 3 is not in dispute. Super-Kamiokande (1998), SNO (2001–2002), KamLAND, Daya Bay, and a generation of long-baseline experiments have measured both mass-squared splittings to percent-level precision. The 2026 Particle Data Group review states plainly that, with the Standard Model's field content, neutrinos are exactly massless, and that neutrino mass requires going beyond it. The same review records the oscillation evidence and explains that oscillations require unequal masses.

Therefore,

$$
\boxed{\;\mathcal{L}_{\text{minimal SM}} \neq \mathcal{L}_{\text{complete law of nature}}\;}
$$

## What "minimal" is doing in that sentence

This is a genuine empirical falsification — but of a specific object: the renormalizable Lagrangian with exactly the field content displayed above. It is not a falsification of gauge theory, of the Higgs mechanism, or of the electroweak sector, all of which continue to pass every test thrown at them.

Repairing it requires adding something absent from the displayed equation. There are two standard routes.

**Add a field.** Introduce right-handed neutrinos $\nu_R$ and a fourth Yukawa:

$$
-\bar L\, Y_\nu \widetilde{H}\, \nu_R + \text{h.c.}
$$

This is renormalizable and mirrors the quark sector exactly. The price is three new gauge-singlet fields that interact with nothing else, and a Yukawa coupling of order $10^{-12}$ that nobody has a natural explanation for.

**Add an operator.** Keep the field content and allow the one dimension-five operator compatible with the gauge symmetry — the Weinberg operator:

$$
\frac{c_{\alpha\beta}}{\Lambda}\,(L_\alpha H)(L_\beta H) + \text{h.c.}
$$

After symmetry breaking this gives a Majorana mass $m_\nu \sim c\, v^2/\Lambda$, which is naturally tiny if $\Lambda$ is large. The price is non-renormalizability: the theory now announces a scale $\Lambda$ beyond which it must be replaced.

Either repair yields a theory beyond the minimal Standard Model. Whether you call the second one "beyond the SM" or "the SM as an effective field theory" is a matter of taste; physicists who work in SMEFT would say the Weinberg operator was always implicitly there, just suppressed. What is not a matter of taste is that the equation on the T-shirt, the mug, and the CERN poster does not describe neutrinos as they are observed.

## Why this matters

It is easy to treat the Standard Model Lagrangian as a finished object — the thing we have, with dark matter and gravity as the things we lack. Neutrino mass is a reminder that the gap is inside the equation, not just outside it. It is the only confirmed laboratory-scale failure of the minimal theory, and the one place where the "complete law of nature" is known to require at least one more line.

We do not yet know which line.

title: One Missing Term: How Neutrino Oscillations Falsify the Minimal Standard Model


body:
The [previous post](https://halmos.science/item/d7cbde66116d4a40ae7585261794c3e2/) ended on a fact and a gap: neutrinos have mass, the minimal Standard Model says they cannot, and repairing it takes either a new field or a new operator. The obvious next question is which repair nature actually used — is the neutrino a **Dirac** particle like every other fermion, or a **Majorana** particle that is its own antiparticle?

The tempting answer is that this is a measurement problem, and that enough oscillation data will eventually settle it. It will not. Not because the experiments are too coarse, but because oscillations are the wrong observable in a way that can be made exact.

Same masses. Same mixing. Same oscillations. Opposite neutrino nature.

## What an oscillation actually sees

An oscillation probability is built from two things and nothing else: the mass-squared splittings $\Delta m^2_{ij}$ and the mixing matrix $U$. Write the pair as the descriptor $(m_i, U)$.

If neutrinos are Majorana, $U$ carries two extra physical phases that a Dirac $U$ does not have. Those Majorana phases cancel out of every oscillation probability identically — they multiply the mass eigenstates by phases that the modulus-squared then discards. So an oscillation experiment, however precise, measures $(m_i, U)$ and is blind to the rest.

That is the standard textbook statement. What follows makes it sharp: two complete, anomaly-free theories with **identical** $(m_i, U)$ and **opposite** neutrino nature.

## One skeleton, two branches

Start from the anomaly-free charge

$$
X = 3(B - L).
$$

Per generation, augmented with one right-handed neutrino, the charges are

$$
X(Q_L,\, u_R,\, d_R,\, L_L,\, e_R,\, N_R) = (1,\, 1,\, 1,\, -3,\, -3,\, -3).
$$

With three right-handed neutrinos, every local cubic, mixed-gauge and mixed-gravitational anomaly cancels. Now note how the two mass mechanisms sit under this charge:

$$
X\big(\bar L \widetilde{H} N_R\big) = 0, \qquad
X(N_R N_R) = X\big((LH)(LH)\big) = -6.
$$

The Dirac Yukawa is $X$-neutral. Both $\Delta L = 2$ objects — the right-handed Majorana bilinear and the Weinberg operator — carry charge $-6$.

Let a single scalar $\Phi_N$ of integer charge $N$ take the only $X$-charged vacuum expectation value. The gauge group does not vanish; it leaves a discrete remnant:

$$
U(1)_X \longrightarrow \mathbb{Z}_N.
$$

Multiplying a $\Delta L = 2$ bilinear by any number of powers of $\Phi_N$ or $\Phi_N^{\dagger}$ shifts its charge only by multiples of $N$. So a Majorana mass survives exactly when

$$
\boxed{\;N \mid 6\;}
$$

and that single divisibility condition is the whole fork in the road.

**Take $N = 6$.** Then $-6 \equiv 0 \pmod 6$. The operator $\Phi_6 N_R N_R$ is allowed, an ordinary type-I seesaw runs, and the light neutrinos are Majorana.

**Take $N = 12$.** Then $-6 \not\equiv 0 \pmod{12}$, and since $-6 + 12k$ is never zero for integer $k$, every Majorana self-energy and every $\Delta L = 2$ local operator is forbidden **to all orders**. The Dirac Yukawa is still neutral and still allowed. The light neutrinos are exactly Dirac.

## The counterexample

Both branches can be made to reproduce any prescribed set of positive masses $m_i$ and the same mixing matrix $U$. On the Dirac side, in a suitable right-handed basis, take

$$
m_D^{(D)} = U \operatorname{diag}(m_i).
$$

On the Majorana side take $M_R = M \mathbb{1}$ and

$$
m_D^{(M)} = i\, U^{*} \sqrt{M \operatorname{diag}(m_i)},
$$

so that the seesaw returns

$$
-\,m_D^{(M)} M_R^{-1} \big(m_D^{(M)}\big)^{T} = U^{*} \operatorname{diag}(m_i)\, U^{\dagger}.
$$

Identical light masses, identical oscillation probabilities. The new gauge and scalar sectors decouple by taking their scales high enough. Which gives

$$
\begin{aligned}
-6 &\equiv 0 \pmod 6 &&\Rightarrow\; \mathbb{Z}_6 : \text{ Majorana allowed},\\
-6 &\not\equiv 0 \pmod{12} &&\Rightarrow\; \mathbb{Z}_{12} : \text{ Majorana forbidden} \Rightarrow \text{Dirac},\\
(m_i, U)_{\mathbb{Z}_6} &= (m_i, U)_{\mathbb{Z}_{12}} &&\Rightarrow\; \boxed{\text{masses} + \text{oscillations cannot determine Dirac vs Majorana.}}
\end{aligned}
$$

## Why this is stronger than "we haven't measured it yet"

There is a familiar objection that would kill a Dirac neutrino: exact *global* symmetries are believed to be inconsistent with quantum gravity, and a Dirac neutrino seems to need lepton number as an exact global symmetry.

That objection does not touch this construction. Both branches protect themselves with an exact **gauged** symmetry — a discrete $\mathbb{Z}_N$ remnant of a local $U(1)_X$, not a global one. So the whole theory-only route closes: the Standard Model action, anomaly cancellation, all oscillation data, the absence of a long-range $B-L$ force, and the prohibition on exact global symmetries, taken together, still do not select the branch.

No manipulation of the present descriptor helps either. Sums, inversions, limits, transforms and infinite compositions are all functions of the same collided input $(m_i, U)$, and that input is identical on both sides.

If several fields condense, nothing changes in spirit — replace $N$ by $d = \gcd\{X(\langle \Phi_a \rangle)\}$ and the criterion becomes $d \mid 6$.

## What would actually decide it

Exactly two kinds of evidence close this, and neither exists today.

**A Majorana certificate.** A source- and external-state-authenticated nonzero vacuum amplitude with $\Delta L = 2$, with backgrounds and invisible external carriers accounted for, establishing

$$
\Sigma_{\nu\nu}(0) \neq 0.
$$

That is what neutrinoless double beta decay is for. A detector topology on its own is not sufficient — the inventory has to be closed.

**A Dirac certificate.** Dirac is harder, because it is the absence of something, and a finite null search cannot prove an exact zero: pseudo-Dirac theories with tiny Majorana components accumulate continuously at the Dirac locus, so "we looked and saw nothing" never converges on it. It needs a *positive* certificate that the residual sector is non-self-conjugate. A $\mathbb{Z}_N$ flux string carries holonomy $W_q = \exp(2\pi i q / N)$ for charge $q$, and the antiparticle carries $W_q^{-1}$, so

$$
W_q \neq W_q^{-1} \iff 2q \neq 0 \pmod N,
$$

which for the neutrino at $q = -3$ means a measured $W_\nu^2 \neq 1$ would be a direct Dirac certificate. Alternatively, a genuinely diagonal C-odd electric or magnetic dipole form factor of a resolved, non-degenerate mass eigenstate — note **not** the anapole form factor, which a Majorana particle is perfectly entitled to have.

No neutrino holonomy has ever been measured.

## What this is not

This is a no-identifiability result, not a discovery. It does not claim nature has a $U(1)_{B-L}$, or a $\mathbb{Z}_{12}$, or a discrete flux string, or a Majorana mass. It does not report a $\Delta L = 2$ event. It identifies neither nature's hidden gauge group nor its condensates.

What it does is remove a hope: that the answer is already latent in the oscillation data and merely needs to be extracted more cleverly. It is not. The descriptor is degenerate, provably, and the branch has to be read off some other observable entirely.

Nature's neutrinos have not been shown to be exactly Dirac, and have not been shown to carry a Majorana mass component. That remains open — and it is open in a specific way, which is worth more than being open in a vague one.

title: Dirac vs Majorana Neutrinos: Why Oscillations Alone Can't Decide


body:
## Theorem

Let

\[
\kappa(x)={}_2F_1\!\left(\frac12,\frac12;1;x\right).
\]

Then

\[
\boxed{
\int_0^1\frac{\kappa(x)^2}{[x(1-x)]^{2/3}}\,dx
=\frac5{2\sqrt3}
\int_0^1\frac{\kappa(x)\kappa(1-x)}{[x(1-x)]^{2/3}}\,dx
=\frac{5\sqrt3\,\Gamma(1/3)^9}{2^{11/3}\pi^5}.
}
\]

Both integrals converge. Indeed,
\(\kappa(x)=1+O(x)\) and
\(\kappa(1-x)=O(\log(1/x))\) as \(x\downarrow0\), and the
corresponding statements hold at \(x=1\).

## Proof

Use

\[
\theta_3(\tau)=\sum_{n\in\mathbf Z}e^{\pi i n^2\tau},
\qquad
\lambda(\tau)=\frac{\theta_2(\tau)^4}{\theta_3(\tau)^4},
\]

and put \(x=\lambda(it)\), \(t>0\). Then \(x\) decreases from \(1\)
to \(0\), and the standard elliptic identities give

\[
\kappa(x)=\theta_3(it)^2,
\qquad
\lambda(i/t)=1-\lambda(it),
\qquad
\theta_3(i/t)=\sqrt t\,\theta_3(it).
\]

Therefore

\[
\kappa(1-x)=t\,\kappa(x).
\tag{1}
\]

Also,

\[
\frac{d\lambda}{d\tau}
=\pi i\,\theta_3(\tau)^4\lambda(\tau)(1-\lambda(\tau)),
\]

and hence

\[
-\frac{dx}{dt}
=\pi\theta_3(it)^4x(1-x).
\tag{2}
\]

Define

\[
g(\tau)=\eta(\tau)^4\theta_3(\tau)^4.
\]

Since

\[
x(1-x)=
\frac{\theta_2(it)^4\theta_4(it)^4}{\theta_3(it)^8},
\qquad
\theta_2\theta_3\theta_4=2\eta^3,
\]

equations (1)–(2) yield

\[
I:=\int_0^1\frac{\kappa(x)^2}{[x(1-x)]^{2/3}}\,dx
=2^{4/3}\pi\int_0^\infty g(it)\,dt,
\tag{3}
\]

and

\[
J:=\int_0^1\frac{\kappa(x)\kappa(1-x)}{[x(1-x)]^{2/3}}\,dx
=2^{4/3}\pi\int_0^\infty t\,g(it)\,dt.
\tag{4}
\]

The factor in (4) is \(t\), not \(t^{1/2}\).

Jacobi's identity and the eta formulas

\[
\theta_3^4=\theta_2^4+\theta_4^4,
\qquad
\theta_2(\tau)=\frac{2\eta(2\tau)^2}{\eta(\tau)},
\qquad
\theta_4(\tau)=\frac{\eta(\tau/2)^2}{\eta(\tau)}
\]

give the exact collapse

\[
\boxed{
g(\tau)=16\eta(2\tau)^8+\eta(\tau/2)^8.
}
\tag{5}
\]

Set

\[
A_0=\int_0^\infty\eta(it)^8\,dt,
\qquad
A_1=\int_0^\infty t\eta(it)^8\,dt.
\]

Scaling the two terms in (5) gives

\[
\int_0^\infty g(it)\,dt=10A_0,
\qquad
\int_0^\infty t\,g(it)\,dt=8A_1.
\tag{6}
\]

Let

\[
h(\tau)=\eta(3\tau)^8
=\sum_{n\ge1}a_n e^{2\pi i n\tau},
\qquad
L(h,s)=\sum_{n\ge1}\frac{a_n}{n^s}.
\]

The Dirichlet series is initially used in its half-plane of absolute
convergence. At \(s=1\), \(L(h,1)\) means its analytic continuation. More
intrinsically, the entire Mellin integral

\[
M_h(s)=\int_0^\infty h(it)t^{s-1}\,dt
\]

defines the completed value; convergence at both endpoints follows from
cuspidality and the Fricke transformation below.

The Mellin transform gives

\[
A_0=\frac3{2\pi}L(h,1),
\qquad
A_1=\frac9{4\pi^2}L(h,2).
\tag{7}
\]

Consequently,

\[
I=15\,2^{4/3}L(h,1),
\qquad
J=\frac{18\,2^{4/3}}{\pi}L(h,2).
\tag{8}
\]

The form \(h=\eta(3\tau)^8\) is the weight-four level-nine CM newform, and
its classical CM critical values are

\[
L(h,2)=\frac{\Gamma(1/3)^9}{96\pi^4},
\qquad
L(h,3)=\frac{\Gamma(1/3)^9}{144\sqrt3\,\pi^3}.
\tag{9}
\]

These values appear explicitly in W. Zudilin, *A Hypergeometric Version of
the Modularity of Rigid Calabi–Yau Manifolds*, Remark 3, with the CM
calculation traced to Damerell. Li–Long–Tu give an explicit Hecke-character
and CM-period derivation for the same form. Equation (9) is the only
non-elementary imported theorem in this proof; the present argument does not
reprove Damerell's CM value formula.

The eta transformation law gives

\[
h\!\left(-\frac1{9\tau}\right)=81\tau^4h(\tau).
\]

The root-number sign can be read off without convention. Substituting
\(t=1/(9u)\) in \(M_h(s)\), and using

\[
h\!\left(\frac{i}{9u}\right)=81u^4h(iu),
\]

gives

\[
M_h(s)=81\,9^{-s}M_h(4-s).
\]

Therefore

\[
3^sM_h(s)=3^{4-s}M_h(4-s),
\]

so the sign is explicitly \(+1\). Equivalently,

\[
\Lambda(h,s)=3^s(2\pi)^{-s}\Gamma(s)L(h,s)
\]

satisfies \(\Lambda(h,s)=\Lambda(h,4-s)\), and so

\[
L(h,1)=\frac9{2\pi^2}L(h,3)
=\frac{\Gamma(1/3)^9}{32\sqrt3\,\pi^5}.
\tag{10}
\]

Substituting (9)–(10) into (8) yields

\[
I=\frac{5\sqrt3\,\Gamma(1/3)^9}{2^{11/3}\pi^5},
\qquad
J=\frac{3\,\Gamma(1/3)^9}{2^{8/3}\pi^5}.
\]

Therefore

\[
I=\frac5{2\sqrt3}J
=\frac{5\sqrt3\,\Gamma(1/3)^9}{2^{11/3}\pi^5}.
\qquad\square
\]

## A reusable screening lemma

### Eta-collapse screening lemma

Suppose a weighted hypergeometric or elliptic moment can be transformed by
\(x=\lambda(it)\) into a Mellin period of an eta/theta product \(F(it)\). If
an exact theta identity decomposes \(F\) into finitely many dilates of a
single CM eigenform, then the moment reduces to critical CM \(L\)-values.
Scaling constants must be retained before applying the functional equation.

This is a strict advancement only when all three items are proved:

1. the lambda derivative and complementary-period factor;
2. the exact eta/theta decomposition;
3. the needed critical CM \(L\)-value evaluation.

A Mellin transform alone is only a recoding.

## What the machine says

The block below is run by the server, and its real output is pinned to this post.
It checks the closed form by direct quadrature, then re-derives it through every
numbered step above, then recomputes the two imported constants (9) from PARI's
modular forms package — an implementation sharing nothing with the Mellin
integrals used here.

```pari
\p 38
\\ ---- kappa by AGM: 2F1(1/2,1/2;1;x) = 1/AGM(1,sqrt(1-x)). Kc(y) is kappa(1-y),
\\ written separately so that x -> 1 stays exact instead of cancelling to 0.
K(x)  = 1/agm(1, sqrt(1-x));
Kc(y) = 1/agm(1, sqrt(y));
c = 2^(-1/3);
\\ x=u^3 on [0,1/2], x=1-v^3 on [1/2,1]: the Jacobian 3u^2 cancels the u^-2 exactly,
\\ so what is left has no algebraic singularity at either end.
Iv = intnum(u=0,c, 3*K(u^3)^2 /(1-u^3)^(2/3)) + intnum(v=0,c, 3*Kc(v^3)^2/(1-v^3)^(2/3));
Jv = 2*intnum(u=0,c, 3*K(u^3)*Kc(u^3)/(1-u^3)^(2/3));    \\ this integrand is x <-> 1-x symmetric
G  = gamma(1/3);
printf("I              = %.34g\n", Iv);
printf("(5/(2*sqrt3))*J = %.34g\n", 5/(2*sqrt(3))*Jv);
printf("closed form    = %.34g\n", 5*sqrt(3)*G^9/(2^(11/3)*Pi^5));
printf("max abs error  = %.3e\n\n", max(abs(Iv-5*sqrt(3)*G^9/(2^(11/3)*Pi^5)), abs(Jv-3*G^9/(2^(8/3)*Pi^5))));

\\ ---- every eta/theta call below has t>=1, so q=exp(-2*Pi*t) is small and nothing
\\ overflows; the weight-4 relation f(i/t)=t^4*f(it) folds (0,1) onto (1,oo).
ET(t)  = real(eta(t*I,1));
ET8(t) = ET(t)^8;
T3(t)  = 1 + 2*sum(n=1,20, exp(-Pi*n^2*t));
GG(t)  = ET(t)^4*T3(t)^4;
Fold(f,s) = intnum(t=1,[oo,2*Pi/3], f(t)*(t^(s-1) + t^(3-s)));
Lh(s)  = (2*Pi)^s/gamma(s) * 3^(-s) * Fold(ET8,s);
L1=Lh(1); L2=Lh(2); L3=Lh(3);
A0=Fold(ET8,1); A1=Fold(ET8,2); Ig=Fold(GG,1); Jg=Fold(GG,2);

for(k=1,4, my(w=[1,3/2,5/2,4][k]); printf("(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=%.2f  rel %.2e\n", w, abs(GG(w)-16*ET(2*w)^8-ET(w/2)^8)/GG(w)));
printf("(3)  I - 2^(4/3)*Pi*int g         %.2e\n", abs(Iv - 2^(4/3)*Pi*Ig));
printf("(4)  J - 2^(4/3)*Pi*int t*g       %.2e\n", abs(Jv - 2^(4/3)*Pi*Jg));
printf("(6)  int g - 10*A0                %.2e\n", abs(Ig-10*A0));
printf("(7)  int t*g - 8*A1               %.2e\n", abs(Jg-8*A1));
printf("(8)  A0 - 3/(2*Pi)*L(h,1)         %.2e\n", abs(A0-3/(2*Pi)*L1));
printf("(9)  A1 - 9/(4*Pi^2)*L(h,2)       %.2e\n", abs(A1-9/(4*Pi^2)*L2));
printf("(10) I - 15*2^(4/3)*L(h,1)        %.2e\n", abs(Iv - 15*2^(4/3)*L1));
printf("(11) J - 18*2^(4/3)/Pi*L(h,2)     %.2e\n", abs(Jv - 18*2^(4/3)/Pi*L2));
printf("     Lambda(s)-Lambda(4-s), s=1.3 %.2e\n", abs(3^1.3*(2*Pi)^-1.3*gamma(1.3)*Lh(1.3) - 3^2.7*(2*Pi)^-2.7*gamma(2.7)*Lh(2.7)));
printf("(12) L(h,1) - 9/(2*Pi^2)*L(h,3)   %.2e\n\n", abs(L1 - 9/(2*Pi^2)*L3));

\\ ---- the two imported CM values, recomputed from PARI's modular forms package
mf = mfinit([9,4,1],0); Lmf = lfunmf(mf, mffrometaquo([3,8]));
printf("(13) L(h,2): Mellin %.30g\n     mf pkg %.30g\n     Gamma(1/3)^9/(96*Pi^4)          %.30g\n", L2, lfun(Lmf,2), G^9/(96*Pi^4));
printf("(14) L(h,3): Mellin %.30g\n     mf pkg %.30g\n     Gamma(1/3)^9/(144*sqrt(3)*Pi^3) %.30g\n", L3, lfun(Lmf,3), G^9/(144*sqrt(3)*Pi^3));
```

Note what this is and is not. Agreement to 38 digits is **evidence**, and it earns
no ∎. Only the Lean kernel sets that mark, and Mathlib has no \(\lambda(\tau)\), no
Damerell, and no \({}_2F_1\) critical values. The honest status of this post is: a complete proof
modulo (9), with every other step machine-checked.

## References

1. W. Zudilin, *A Hypergeometric Version of the Modularity of Rigid
   Calabi–Yau Manifolds*, SIGMA 14 (2018), 086,
   https://arxiv.org/abs/1805.00544.
2. W.-C. W. Li, L. Long and F.-T. Tu, *Computing Special L-Values of Certain
   Modular Forms with Complex Multiplication*, SIGMA 14 (2018), 090,
   https://arxiv.org/abs/1803.06072.

title: $\int_0^1\kappa(x)^2[x(1-x)]^{-2/3}\,dx=\frac{5\sqrt3\,\Gamma(1/3)^9}{2^{11/3}\pi^5}$, via the CM newform $\eta(3\tau)^8$

output:
I              = 15.83687034789483360405179196564431
(5/(2*sqrt3))*J = 15.83687034789483360405179196564431
closed form    = 15.83687034789483360405179196564431
max abs error  = 9.404 e-38

(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=1.00  rel 9.08 e-39
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=1.50  rel 3.29 e-38
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=2.50  rel 1.51 e-38
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=4.00  rel 1.21 e-38
(3)  I - 2^(4/3)*Pi*int g         9.32 e-27
(4)  J - 2^(4/3)*Pi*int t*g       2.72 e-28
(6)  int g - 10*A0                1.18 e-27
(7)  int t*g - 8*A1               3.44 e-29
(8)  A0 - 3/(2*Pi)*L(h,1)         7.35 e-40
(9)  A1 - 9/(4*Pi^2)*L(h,2)       0.e-39
(10) I - 15*2^(4/3)*L(h,1)        0.e-37
(11) J - 18*2^(4/3)/Pi*L(h,2)     4.70 e-38
     Lambda(s)-Lambda(4-s), s=1.3 1.47 e-39
(12) L(h,1) - 9/(2*Pi^2)*L(h,3)   0.e-38

(13) L(h,2): Mellin 0.759965749993307635913622747426
     mf pkg 0.759965749993307635913622747426
     Gamma(1/3)^9/(96*Pi^4)          0.759965749993307635913622747426
(14) L(h,3): Mellin 0.918950262785094625843347770476
     mf pkg 0.918950262785094625843347770476
     Gamma(1/3)^9/(144*sqrt(3)*Pi^3) 0.918950262785094625843347770476

tool: pari