You write mathematics in LaTeX. Sucuri reads it as SymPy, and shows what it understood — in textbook mathematics, and in code you can copy. Where the notation is ambiguous, it asks instead of guessing. That is the only rule, and everything here follows from it.
To see Sucuri facing exercises from real differential geometry problem sets — what it solves, what it doesn't, and why —, there is the tutorial.
Every example in this manual is run by the test suite on every change. What is written here as output is the output.
1. Writing and running
In the notebook, type in the cell and press
Shift+Enter. Every cell that becomes mathematics gets a
name — eq1, eq2 — and that is how you refer to it
later.
x^2 + 1
x**2 + 1
2. When it asks
Not all notation says what it means. y'' may be the second
derivative of y, or a symbol called “y double prime” — both are
written the same way, and Sucuri does not choose for you:
y'' + y = 0
y'' → derivative of order 2 of y | symbol named y''
You answer by clicking the right reading — or, better, by declaring, which answers once for the whole notebook.
The division slash is another case. The parser puts into the denominator
everything written right after it — 1/2 x would become 1/(2x) —, and
in ordinary writing the opposite is almost always meant. Sucuri asks; to avoid the
question, write \frac{1}{2}, or a \cdot after the denominator:
y = 1/2 (x+z)
/2 → the fraction multiplies what follows: (…/2)·(…) | what follows goes into the denominator: …/(2·…)
3. Declaring
Declaring does not pick between the readings: it dissolves the ambiguity. If
y is a function of x, then y' can only be
dy/dx — there is nothing to ask.
y = y(x)
y'' + y = 0
Eq(y(x) + Derivative(y(x), (x, 2)), 0)
u = u(t,x) | u is a function of t and x |
e = euler | e is Euler's number, not a symbol |
a = symbol | a is not a function: a(x+1) is a product |
\mu, \nu = indices | tensor indices — indices(3) gives the dimension; indices(d), a letter |
T = tensor(0,2) | Schutz's type: 0 forms, 2 vectors |
F = tensor(0,2, antisymmetric) | and the symmetry of the slots: symmetric, antisymmetric, riemann |
\omega = form(2) | a 2-form — an antisymmetric (0,2) |
g = metric | the metric: lowers and raises indices, and is symmetric |
g = metric(-,+,+,+) | with the signature, written in signs |
g = metric(cartesian) | Euclidean and constant, ∂g = 0; or (-,+,+,+, constant) |
x = coordinates | xi, the coordinates with an index: ∂jxi = δij |
g = det(g) | g without an index is det gμν: √−g, ln|g| |
g = metric(…components…) | with the diagonal components (section 8) |
\delta = kronecker | the delta: δμν |
\epsilon = levi-civita(tensor) | or (symbol) — the books don't agree |
\nabla = levi-civita | the connection: ∇g = 0, torsion-free |
R = riemann(eq1) | the Riemann tensor, in the convention eq1 writes |
R = ricci(eq2) | Rμν and R, contractions of the Riemann tensor, in the convention eq2 writes |
\Gamma = christoffel(eq1) | the Christoffel symbols, in the slot order eq1 writes |
R = curvature | R(U,X)W is the curvature operator, index-free |
\star = hodge | the Hodge dual (needs the signature) |
Parentheses, as in a book. Written with the same name on both sides it is a
tautology — nobody writes u = u(t,x) as an equation —, and that
repetition is what separates a declaration from mathematics: u(t,x) alone
is still an expression.
4. The verbs
They are few, and closed on purpose. If you could write Python here, the bridge this program is would stop being mandatory — and what would be left is a Jupyter with extra steps.
The list below is the whole list: what is not in it is not a verb. The
English and the Portuguese names work in either interface language. The
declarations — metric, indices, tensor,
… — are in section 3.
| Verb | Portuguese | What it does |
|---|---|---|
| Equations | ||
solve(eq) | resolver(eq) |
A differential equation goes to the ODE solver, and the solution comes back checked by substitution; an algebraic equation gives the roots. Refuses what is not an equality. |
evaluate(eq) | avaliar(eq) |
Does the held computation: the exact value, with the approximation
beside it; an indefinite integral gives the family. With indices and a
metric with components, gives the components; a table label,
evaluate(\Gamma^{r}_{tt}), gives its value (section 8). |
simplify(eq) | simplificar(eq) |
Simplifies, and the result gets a name. With indices, uses the
declared symmetries, and an equality between tensors comes out
True when the sides coincide (section 7). |
separate(eq) | separar(eq) |
Separates the variables of a PDE assuming a product, u = T(t)·X(x): the ODEs come out named, each with its solution. Does not prove that the superposition of the modes is complete. |
check(eq, cand) | conferir(eq, cand) |
Substitutes the candidate into the equation: candidate verified, with remainder 0, or the remainder left over. With a single argument, refuses. |
export(eq) | exportar(eq) |
The SymPy code that declares, builds and solves eq — it runs without Sucuri. |
latex(eq) | latex(eq) |
The LaTeX writing, to copy. |
series(eq, x, n) | série(eq, x, n) |
The series around x = 0 up to order n, with the O(xn); for an equality, that of the left side minus the right. The polynomial gets a name. Without the three arguments, refuses. |
| Index notation | ||
contract(eq) | contrair(eq) |
Lowers and raises indices with the declared metric: gμνAν becomes Aμ. Refuses when the metric is contracted with nothing (section 7). |
indices(eq) | indices(eq) |
Writes with indices what was written without — ∇UX
becomes Uα∇αXμ —, with the declared
indices; without them, refuses (section 11).
\mu, \nu = indices(4) is something else: the declaration
(section 3). |
expand(eq)expand(eq, g) |
expandir(eq)expandir(eq, g) |
Opens ∇ into ∂ and Γ; with g, also opens Γ through the metric. Needs
the Γ convention declared, \Gamma = christoffel(eq1). An
equality that closes comes out True (section 7). |
independent(T, eq…) | independentes(T, eq…) |
How many components of T remain, given the declared symmetries and
the given equations, in the dimension of indices(n). |
in_components(eq) | em_componentes(eq) |
Checks the identity with the most general tensor the declarations
allow and an arbitrary metric: True or
False. |
linearize(eq, h) | linearizar(eq, h) |
g = η + εh, to first order in ε. Needs
h = tensor(0, 2, symmetric) declared. |
prove(eq, h1, h2, …) | provar(eq, h1, h2, …) |
The goal from the named hypotheses only, line by line, with or without indices (sections 9 and 10). When it finds nothing, it says that not finding is no proof of falsehood. |
| Components in a chart | ||
christoffel(g) | christoffel(g) |
The nonzero Γ of the metric with components, in the declared chart
(section 8). With a name on the left, \Gamma = christoffel(eq1)
is not this verb: it declares the Γ convention eq1 writes (section 3). |
riemann(g) | riemann(g) |
The nonzero components of the Riemann tensor. R = riemann(eq1)
declares the Riemann convention eq1 writes (section 3). |
ricci(g) | ricci(g) |
The nonzero components of Rμν. R = ricci(eq2)
declares Rμν and R as contractions of the Riemann tensor
(section 3). |
scalar(g) | escalar(g) |
The Ricci scalar. All four take a second name,
scalar(g, \Phi): the computation to first order in Φ. |
geodesics(g) | geodesicas(g) |
The geodesic equations, with affine parameter, each one named; and what is conserved: g(ẋ, ẋ) and g(∂k, ẋ) for each coordinate the metric does not depend on. |
orbits(g) | órbitas(g) |
The geodesics of a diagonal 2D metric with a cyclic coordinate, by quadrature: dφ/dr and, when the integral is elementary, the orbit, named. Any other dimension, refuses. |
volume(g, x = a .. b, …) | volume(g, x = a .. b, …) |
∫√|det g|, with one limit per coordinate: the volume element and the value, named. With a limit missing, refuses. |
element(g) | elemento(g) |
The line element ds². |
tetrad(g) | cartan(g) |
For a diagonal metric: the tetrad ea = √|gaa| dxa, the connection forms, the curvature forms and the Riemann tensor in the orthonormal basis. |
in_chart(eq) | em_carta(eq) |
An expression with indices, component by component in the chart of
the declared metric; Riemann and Ricci enter through the declared
conventions. For an equality, True or the components of
the difference. |
killing(g, X)killing(g, n) |
killing(g, X)killing(g, n) |
With a field: ℒXg, and whether X is Killing. With a
number: the Killing fields with polynomial components of degree ≤ n.
A field is declared with X = field(…) or
covector(…), in the components of the chart. |
bracket(X, Y) | colchete(X, Y) |
[X, Y], in the coordinate basis. |
nabla(g, A) | nabla(g, A) |
The first and second covariant derivatives of a field or covector. |
laplacian(g, A) | laplaciano(g, A) |
gik∇i∇kA, component by component. |
h = induced(g, X^1, …) | h = induzida(g, X^1, …) |
The induced metric — the pull-back of g by the parametrization —, in the coordinates declared last; h is a metric like any other. Without new coordinates, refuses. |
restrict(K, h) | restringir(K, h) |
A field of the outer space, restricted to the submanifold of h and registered under the same name. A field with a normal component, refuses. |
| Forms in a chart | ||
wedge(\alpha, \beta) | cunha(\alpha, \beta) |
α∧β, in a chart: \alpha = form(x\,dy). With a name on
the left, P = wedge(\alpha, \beta), the result becomes a
named form — this also holds for star, exterior, interior and lie. |
star(\alpha, g) | estrela(\alpha, g) |
The Hodge dual by the metric; star(1, g) is the volume
element. |
exterior(\alpha) | exterior(\alpha) |
dα. |
interior(X, \alpha) | interior(X, \alpha) |
ιXα, with X a field. |
lie(X, \alpha) | lie(X, \alpha) |
ℒXα. |
equal(\alpha, \beta) | iguais(\alpha, \beta) |
True, or the difference. Takes 0:
equal(E, 0). |
ortonormal(\alpha, g) | ortonormal(\alpha, g) |
α in the orthonormal cobasis σi = √|gii| dxi. |
solve
A single verb; the object decides the computation. A differential equation goes to the
ODE solver, with the solution checked by substitution; an algebraic
equation goes to solve.
y = y(x)
y'' + y = 0
solve(eq1)
Eq(y(x), C1*sin(x) + C2*cos(x))
plus the line check: substituted into the equation, remainder 0. Without it the answer is not presented as a conclusion.
evaluate
\int_0^1 x^2
evaluate(eq1)
1/3
with the approximation ≈ 0.333333333333 beside it —
never in place of the exact value.
An indefinite integral returns the family, with the constant:
\int \sin x\,dx
evaluate(eq1)
-cos(x)
shown as −cos(x) + C: the result is the
whole family, and the copyable code carries one antiderivative of it.
simplify
\frac{x^2 - 1}{x - 1}
simplify(eq1)
x + 1
export
The most honest request a program like this gets: give me the code you used. What comes out runs on its own, without Sucuri.
y = y(x)
y'' + y = 0
export(eq1)
eq1 = Eq(y(x) + Derivative(y(x), (x, 2)), 0)
together with the symbol declarations, the solver call and the line that checks the solution.
separate and check
For partial differential equations. SymPy's pdsolve solves
little — it does not solve the wave equation —, but separating variables and checking
a candidate solve the problem the classical way.
u = u(t,x)
c = symbol
\frac{\partial^2 u}{\partial t^2} = c^2 \frac{\partial^2 u}{\partial x^2}
separate(eq1)
Eq(Derivative(T(t), (t, 2)), k*T(t))
and the equation in x, each with its own solution — and each
with a name (eq2, eq3), so you can carry on:
solve(eq2).
Separating does not solve the equation, and the result says so: it assumes the solution is a product. What comes out are the modes; the general solution is their superposition, and separation does not prove it is complete.
And check goes the opposite way from solve: you
propose, it tests.
u = u(t,x)
c = symbol
F = F(z)
G = G(z)
\frac{\partial^2 u}{\partial t^2} = c^2 \frac{\partial^2 u}{\partial x^2}
u = F(x - c t) + G(x + c t)
check(eq1, eq2)
candidate verified
d'Alembert: remainder 0. A wrong candidate comes out as candidate NOT verified, with the remainder left over; and when the checker cannot test, it says so instead of accusing.
prove
The goal first, then the hypotheses — only the named ones. Writing an equation in the notebook is not asserting it, and a proof that used the scratch computation on the line above would prove nothing.
U = tensor(1, 0)
X = tensor(1, 0)
Y = tensor(1, 0)
\nabla_U X = \nabla_X U
\nabla_Y \nabla_U X = \nabla_Y \nabla_X U
prove(eq2, eq1)
nabla_Y(eq1)
each line of the answer says which hypothesis it came from and what was done with it — here, ∇Y applied to both sides of eq1 —, and the sum is checked again before the ∎. Index-free, it works with the connection and with forms (sections 9 and 10); when it finds nothing, it says that not finding is not proof that it is false.
With indices, the same verb. The relations the search draws from each hypothesis are those that hold for any tensor equation: permuting the free indices (and contracting them, with the metric), multiplying by a tensor, applying ∇ once or twice. With Levi-Civita and the Riemann tensor declared, the first Bianchi identity enters as a theorem, and the proof cites it when it uses it.
a, b = indices
T = tensor(2, 0, symmetric)
X = tensor(0, 1)
\nabla = levi-civita
g = metric
\nabla_a T^{ab} = 0
\nabla_a X_b + \nabla_b X_a = 0
\nabla_a (T^{ab} X_b) = 0
prove(eq3, eq1, eq2)
1/2 · eq2 [a→L_0, b→L_1] × T(-L_0, -L_1)
the current of a Killing field is conserved: eq1 times X, plus ½ eq2 times T. The two notations do not mix in a proof: an index-free hypothesis in a goal with indices is refused.
independent, in_components, linearize
Three verbs for what index algebra cannot reach on its own, all
in a dimension given as a number — indices(4):
independent(T, eq…) | how many components of T
remain, given the declared symmetries and the given equations (linear in T).
Zero: only the null tensor has these properties. The Riemann tensor defined
by the connection — R = riemann(eq), with Levi-Civita — brings the
first Bianchi identity along (20 in 4D); a declared tensor(0,4,riemann)
only has the pair symmetries, and gives 21. |
in_components(eq) | checks the identity with the most general tensor the declarations allow and an arbitrary metric, component by component. |
linearize(eq, h) | g = η + εh to first order in ε: opens ∇ into Γ and Γ into ∂g, substitutes g and ∂g, and truncates. |
\mu, \nu, \rho, \sigma = indices(2)
V = tensor(1, 0)
\nabla = levi-civita
g = metric
\nabla_\mu \nabla_\nu V^\rho - \nabla_\nu \nabla_\mu V^\rho = R^\rho{}_{\sigma\mu\nu} V^\sigma
R = riemann(eq1)
R_{\mu\nu} = R^\rho{}_{\mu\rho\nu}
R = ricci(eq2)
R_{\mu\nu} = \frac{1}{2} R g_{\mu\nu}
in_components(eq3)
True
in two dimensions, the Einstein tensor vanishes
identically. With indices(3), False.
contract, indices
contract lowers and raises indices with the metric (section 7);
indices writes with indices what was written without them (section 11). The
component verbs — christoffel, riemann,
ricci, scalar — are in section 8.
expand opens ∇ into ∂ and Γ, with indices (section 7) — and
\Gamma = christoffel(eq1), with a name on the left, is not the component
verb: it is the declaration of the Γ convention.
5. What each answer means
| established | checked. May be cited as a conclusion. |
| unsourced | the program found something and could not confirm it. It is not presented as a conclusion. |
| not applicable | it is data, not a conclusion — a table, a separation, an intermediate step. |
And the colours: green decided or checked; amber came from a general rule and nobody looked at that case; red blocks you from going on. A scope note — “this does not solve the equation” — is green: the computation is right; what it does not do is something that needed saying.
6. When it finds nothing
y = y(x)
y'' = 6 y^2
solve(eq1)
no solution found
with the patterns SymPy tried, and the reminder that
matters: not finding a solution is not proof that none exists.
For that other question there is the korvin module, which decides
non-integrability via Galois theory — and which does not ship with the
online version.
7. Tensors with indices
An index is not an exponent, and SymPy's LaTeX parser does not know the difference:
without a declaration, A^\mu would become A raised to μ. You are the one
who decides:
\mu, \nu = indices
g = tensor(0, 2)
g_{\mu\nu} A^\mu A^\nu
g(-L_0, -L_1)*A(L_0)*A(L_1)
all indices contracted. The valence appears on screen, because it is the first thing you check in a tensor.
And consistency comes along — this is a relativity error, not a typo, and nobody spots it by eye:
\mu, \nu = indices
A^\mu B_\mu + C^\nu
the terms of the sum have different free indices
Once the metric is declared, indices go down and up — contract applies the
convention Aμ ≡ gμνAν:
\mu, \nu = indices
g = metric
A = tensor(1,0)
g_{\mu\nu} A^{\nu}
contract(eq1)
A(-mu)
It requires g = metric because lowering an index is a
convention of the metric, not of any (0,2) — and nothing in the
expression distinguishes the two cases. Without the declaration, it refuses.
Symmetry
And the symmetry of the slots is declared together with the type. It serves both notations:
with indices, simplify uses it; index-free, prove does.
\mu, \nu = indices
F = tensor(0, 2, antisymmetric)
h = tensor(2, 0, symmetric)
F_{\mu\nu} h^{\mu\nu}
simplify(eq1)
0
antisymmetric contracted with symmetric. The metric is symmetric without needing to be told; and symmetry on a (1,1) is refused — swapping an upper index with a lower one needs the metric, and then it is another tensor.
a, b, c, d = indices
R = tensor(0, 4, riemann)
R_{abcd} - R_{cdab}
simplify(eq1)
0
the symmetries of the (0,4) Riemann tensor: antisymmetric in each pair, symmetric under exchange of the pairs — the same in every book. The cyclic identity does not enter: it is a theorem, and needs zero torsion.
\mu, \nu = indices
T = tensor(0, 2)
T_{(\mu\nu)} + T_{[\mu\nu]} - T_{\mu\nu}
simplify(eq1)
0
(…) symmetrizes, […] antisymmetrizes, with the 1/n! factor of
Wald, MTW and Carroll; what is between bars, S_{(\mu|\rho|\nu)},
is left out. Without the indices declared, it refuses: SymPy's parser
drops the parentheses and would read T(μν) as Tμν.
Kronecker and Levi-Civita
The Kronecker delta and Levi-Civita are declared too — δ because
\delta also means variation, and ε because there are two readings:
\mu, \nu = indices
\delta = kronecker
A = tensor(1, 0)
\delta^\mu_\nu A^\nu
simplify(eq1)
A(mu)
and \delta^\mu_\mu becomes the dimension.
\epsilon = levi-civita
levi-civita(symbol) or levi-civita(tensor)?
the symbol is ±1 in every chart and is not raised or lowered
with g; the tensor is √|g| times the symbol, and is raised and lowered. The two
readings give different results in contract.
\mu, \nu, \rho, \sigma = indices
\delta = kronecker
g = metric(-,+,+,+)
\epsilon = levi-civita(tensor)
\epsilon^{\mu\nu\rho\sigma} \epsilon_{\mu\nu\rho\sigma}
simplify(eq1)
-24
the sign is (−1)s, with s the number of minus signs
in the signature — which is why it is declared with the signs, and
metric(lorentzian) alone is refused. With the symbol, it is +24
in any signature.
Derivative with an index
And the derivative with an index is an object of its own, not a factor — ∂ commutes, ∇ does not, and both obey Leibniz:
\mu, \nu = indices
\partial_\mu \partial_\nu \phi - \partial_\nu \partial_\mu \phi
simplify(eq1)
0
with ∇ in place of ∂, it does not vanish: ∇μ∇ν − ∇ν∇μ is torsion and curvature, and nothing is assumed.
With the connection declared, the commutator becomes curvature — in the convention of the definition you wrote:
\mu, \nu, \rho, \sigma = indices
V = tensor(1, 0)
W = tensor(0, 1)
\nabla = levi-civita
\nabla_\mu \nabla_\nu V^\rho - \nabla_\nu \nabla_\mu V^\rho = R^\rho{}_{\sigma\mu\nu} V^\sigma
R = riemann(eq1)
\nabla_\mu \nabla_\nu W_\rho - \nabla_\nu \nabla_\mu W_\rho
simplify(eq2)
-R(L_0, -rho, -mu, -nu)*W(-L_0)
the sign and slot order of the Riemann tensor vary from book
to book; riemann(eq1) reads them off the identity you wrote. And
\nabla = levi-civita is what makes ∇g = 0 — without it, no.
And ∇ opens into ∂ and Γ. The slot order of Γ also varies — Carroll puts the
derivative index first, Reall last — and so it too is read from the
definition. expand(eq) replaces each ∇ with ∂ plus one Γ per index
(+ for upper, − for lower); expand(eq, g) also writes
each Γ in terms of the metric, which only holds — and is only done — with
\nabla = levi-civita. For an equation, the answer is
True when both sides agree.
\mu, \nu, \lambda, \sigma = indices
V = tensor(1, 0)
\nabla = levi-civita
g = metric
\nabla_\mu V^\nu = \partial_\mu V^\nu + \Gamma^\nu{}_{\mu\lambda} V^\lambda
\Gamma = christoffel(eq1)
\partial_\lambda g_{\mu\nu} = g_{\mu\sigma} \Gamma^\sigma{}_{\nu\lambda} + g_{\nu\sigma} \Gamma^\sigma{}_{\mu\lambda}
expand(eq2, g)
True
∂λgμν = −gμαgνβ∂λgαβ
— what “inverse” means — is applied by simplify whenever
a metric is declared.
8. Components in a chart
Index notation gives the structure — that g has two
lower indices. It does not say what g is. For Christoffel,
Ricci and Riemann you need the other side: components, in a chart. Declare the
coordinates and then the metric, by its diagonal:
x = coordinates(t, r, \theta, \phi)
g = metric(-(1 - \frac{2M}{r}), \frac{1}{1 - \frac{2M}{r}}, r^2, r^2 \sin^2\theta)
g is the metric in (t, r, \theta, \phi), diagonal, with 4 components
Schwarzschild. The diagonal, and not \begin{pmatrix},
because SymPy's LaTeX parser does not read matrices — and because that is how
books give almost every metric that matters.
From there come christoffel, riemann, ricci
and scalar. What comes back are components, and so the
answer always says which coordinates it is in: changing chart changes all of
them.
x = coordinates(t, r, \theta, \phi)
g = metric(-(1 - \frac{2M}{r}), \frac{1}{1 - \frac{2M}{r}}, r^2, r^2 \sin^2\theta)
ricci(g)
0 nonzero component(s)
Vanishing Ricci — Schwarzschild is a vacuum solution. This is the sanity check of all of relativity, and the program does it in seconds. Unlike a component, “Ricci vanishes” does not depend on the chart.
And if the metric has components, evaluate gives the other side:
not the structure, the value.
x = coordinates(t, r, \theta, \phi)
g = metric(-(1 - \frac{2M}{r}), \frac{1}{1 - \frac{2M}{r}}, r^2, r^2 \sin^2\theta)
\mu, \nu = indices
A = tensor(1,0)
g_{\mu\nu} A^{\nu}
evaluate(eq1)
A_{t}
the four components of Aμ, each as a function
of those of Aμ — which nobody declared, and so they enter as names
(A__t is At in SymPy's convention, which re-enters
without becoming a power).
What the table prints has a name, and a name is a target for a verb:
x = coordinates(t, r, \theta, \phi)
g = metric(-(1 - \frac{2M}{r}), \frac{1}{1 - \frac{2M}{r}}, r^2, r^2 \sin^2\theta)
christoffel(g)
evaluate(\Gamma^{r}_{tt})
M*(-2*M + r)/r**3
without the double braces the table uses — braces are TeX
typography, not identity. And a component that is zero does not go
into the table (55 zeros would hide the nine that matter) but answers when
asked: evaluate(\Gamma^{t}_{rr}) gives 0.
9. Without indices: the connection
Without indices, the vector is the abstract object, and the same declaration
says what \nabla_U means: the derivative in the direction of U.
U = tensor(1, 0)
X = tensor(1, 0)
\nabla_U \nabla_X U - \nabla_X \nabla_U U
nabla_U(nabla_X(U)) - nabla_X(nabla_U(U))
application, not product: the order stays in the structure,
and the two terms do not cancel. Without the declaration the parser would read
X*nabla_{U}, which commutes — and the curvature would vanish.
\nabla_V X
'V' was not declared
∇V and ∇μ are written the same way. What decides between direction and index is the declaration.
With R = curvature, R(U,X)W is the operator applied to
W, not R times the parenthesis. And between two vectors the bracket can only be
the Lie bracket:
U = tensor(1, 0)
X = tensor(1, 0)
R = curvature
R(U,X)U = \nabla_U \nabla_X U - \nabla_X \nabla_U U - \nabla_{[U,X]} U
Eq(R(U, X)(U), nabla_U(nabla_X(U)) - nabla_X(nabla_U(U)) - nabla_{[U, X]}(U))
the declaration gives R's role, not its sign: the argument order and the sign vary from book to book, and for reading that does not matter.
And with the reading comes the proof. prove takes the goal and the
hypotheses — only the named ones: writing an equation in the notebook is not
asserting it.
U = tensor(1, 0)
X = tensor(1, 0)
R = curvature
[U,X] = 0
\nabla_U U = 0
\nabla_U X - \nabla_X U = [U,X]
R(U,X)U = \nabla_U \nabla_X U - \nabla_X \nabla_U U - \nabla_{[U,X]} U
\nabla_U \nabla_U X = R(U,X)U
prove(eq5, eq1, eq2, eq3, eq4)
proved from eq1, eq2, eq3, eq4
the geodesic deviation equation. Each step of the table says
which hypothesis it came from and what was done to it — nabla_U(eq3)
is eq3 with ∇U applied to both sides — and the sum is checked again
before the ∎. On its own the engine knows only what holds for any connection —
linearity, Leibniz; the sign of R comes from the definition you gave, and with
the opposite sign the same call does not prove.
A definition holds for any vector. With \forall it is stated
once, and the proof instantiates it wherever it needs to:
U = tensor(1, 0)
X = tensor(1, 0)
R = curvature
\forall A, B, W: R(A,B)W = \nabla_A \nabla_B W - \nabla_B \nabla_A W - \nabla_{[A,B]} W
\forall A, B: \nabla_A B - \nabla_B A = [A,B]
[U,X] = 0
\nabla_U U = 0
\nabla_U \nabla_U X = R(U,X)U
prove(eq5, eq1, eq2, eq3, eq4)
eq1[A→U, B→X, W→U]
the table says in which instance each general hypothesis was
used. The separator after the ∀ list is mandatory — a colon,
\colon, \quad — and the bound variables do not
leak into the lines below.
A scalar is whatever was not declared a tensor, and \nabla_U f is
the directional derivative U(f). Every symbol that is not a number is treated as a
function — the safe side: if c is constant, U(c) = 0 is a special case, and a
proof that needs it asks for the hypothesis.
U = tensor(1, 0)
X = tensor(1, 0)
\nabla_U f = 0
\nabla_U (f X) = f \nabla_U X
prove(eq2, eq1)
eq1·X
Leibniz: ∇U(fX) = U(f)X + f∇UX, and the scalar hypothesis enters multiplied by X. The combination that closes a proof uses numbers only: multiplying by a function is an explicit step, and fX = fU does not give X = U — false where f vanishes.
With g = metric, g(X,Y) is the inner product —
symmetric and linear in each slot, with no hypothesis. Metric compatibility is a
hypothesis, and with it and zero torsion the Koszul formula follows:
X = tensor(1, 0)
Y = tensor(1, 0)
Z = tensor(1, 0)
g = metric
\forall A, B, C: \nabla_A g(B,C) = g(\nabla_A B, C) + g(B, \nabla_A C)
\forall A, B: \nabla_A B - \nabla_B A = [A,B]
2 g(\nabla_X Y, Z) = \nabla_X g(Y,Z) + \nabla_Y g(X,Z) - \nabla_Z g(X,Y) + g([X,Y],Z) - g([X,Z],Y) - g([Y,Z],X)
prove(eq3, eq1, eq2)
g(eq2[A→X, B→Y], Z)
zero torsion placed in the first slot of g: a relation between vectors turned into one between scalars. Without eq2, the same call does not prove.
10. Differential forms
And differential forms, without indices: d, ∧, ιX,
ℒX. \omega = form(2) declares a 2-form;
\mathrm{d} is always the operator, and d only when it
acts on a declared form.
\omega = form(1)
\eta = form(2)
\mathrm{d}(\omega \wedge \eta) = \mathrm{d}\omega \wedge \eta - \omega \wedge \mathrm{d}\eta
prove(eq1)
proved from no hypothesis
d², graded Leibniz, graded commutativity, ι as an antiderivation and Cartan's formula hold with no hypothesis. η∧η = 0 does not pass — η has even degree.
g = metric(-,+,+,+)
\star = hodge
F = form(2)
\star \star F = -F
prove(eq1)
proved from no hypothesis
⋆⋆ = (−1)p(n−p)+s: with Euclidean signature the same call does not prove. Hodge requires the signature to be declared; the orientation, no — it flips the sign of ⋆, not that of ⋆⋆.
11. From one notation to the other
And from one notation to the other: indices writes with indices
what was proved without them.
\mu, \alpha, \beta = indices
U = tensor(1, 0)
X = tensor(1, 0)
\nabla_U X
indices(eq1)
U(L_0)*D_X(-L_0, mu)
Uα∇αXμ. The curvature
R(U,X)W is translated in the convention of riemann(eq), and the
translation states in a note what it assumed about the index-free R.
12. The notebook
| New | erases what is written and what has accumulated |
| Open / Save | a text file, cells separated by %%; opens in
any editor |
| Run all | redoes everything from what is written, in order |
| Restart | throws away only what has accumulated: eq1 ceases to exist,
and not one line of what you wrote moves |
Between two cells there is a + to insert; in the corner of each one, a × to delete, with undo in the notice bar.
Enter breaks the line; Shift+Enter runs. A single cell can hold more than one instruction, one per line, and each answers in order:
\mu, \nu = indices
A = tensor(1,0)
A is a tensor of type (1,0)
it only chains when every line is a recognized instruction. A LaTeX equation may span two lines, and splitting it would give two meaningless halves instead of an error.
13. What it does not do yet
Saying this is part of the job. Nothing below fails silently — everything is refused with the reason.
- Functions the parser does not know:
\operatorname{arsinh},\coth,\left\|·\right\|. SymPy has these functions; it is the LaTeX parser that does not read them. \frac{d}{dx}as an operator is not a declared site: it works because SymPy's grammar has a rule for it, and where that rule does not reach, the silence returns.- Systems of equations: one verb at a time, one equation at a time.
- Non-diagonal metric: the declaration asks for the diagonal. Kerr, with its cross term dt dφ, does not go in yet.
provechains hypotheses by linear algebra, with a finite search: a proof that needs an idea — introducing a quantity that does not appear in the statement — does not come out, and a proof that needs many chained instances may take a while. With indices, it goes up to ∇∇ of the hypotheses.- Forms: the formula for dω on vectors enters as a hypothesis, because its factor changes with the normalization; the codifferential δ = ±⋆d⋆ does not come built in, because the sign is a convention.
- Translation: only from index-free to indexed; ∀ and forms are not translated.
The code, the audits and the full list of limitations are at github.com/RafaelCRdeLima/SUCURI.