Cauchy’s rigidity theorem says a convex polyhedron is determined by its faces: if two convex polyhedra have congruent corresponding faces, attached to each other in the same combinatorial pattern, then the two polyhedra are congruent. You cannot flex one into the other. It is one of the oldest theorems about polyhedra, and one of the prettiest, and formalizing it forces a question that the prose statement glides over: what, exactly, is the object the theorem is about?

To state “two polyhedra with the same faces glued the same way,” you first need a faithful notion of “a convex polyhedron with its face-gluing.” And the moment you write that structure down in a proof assistant, you have to decide, field by field, which of its parts are data and which are assumptions in disguise.

The object, and its seams

Take the surface to be triangulated: a finite set of vertices with coordinates, and a list of triangular faces, each face recording its three vertices in a cyclic order together with an outward normal. So far this is plain data — the shape of a polyhedron.

But a surface needs more than a bag of triangles. For the combinatorics of Cauchy’s argument to even make sense, the triangles have to fit together into a closed oriented surface. Concretely:

• every edge is shared by exactly two triangles;
• no directed edge is repeated;
• around each vertex, the incident triangles form a single closed fan (not two separate fans pinched at a point);
• adjacent triangles induce opposite orientations on their shared edge.

Call these the seam conditions. In a first formalization they sit in the structure as fields you must supply — assumptions the user hands over along with the coordinates. And that is the uncomfortable part. A reader who hands you four coordinates for a tetrahedron should not also have to promise you that its edges meet two triangles each. That is not extra information about the tetrahedron; it is true of every convex polyhedron. If the seam conditions are consequences of convexity, then carrying them as assumptions is carrying a theorem in the costume of a hypothesis.

So the question is sharp: are the seam conditions data, or are they theorems?

They are theorems

They are theorems — provided you add one honestly geometric hypothesis in their place: that the listed triangles are exactly the facets of the convex hull of the vertices. This says nothing combinatorial. It is the geometric statement that the face list is complete and sound: every genuine flat face of the solid is listed, and every listed triangle is a genuine face. Everything about how the faces meet then follows from convex geometry.

Two facts carry the weight.

The first is local to an edge: in a full-dimensional convex polyhedron, every edge lies on exactly two facets. The clean textbook proof talks about the normal cone of the edge and counts its extreme rays — machinery a bare proof assistant does not have on hand. But there is an elementary route. Fix an edge with direction $d$, and measure the other vertices by two coordinates transverse to $d$: a “height” $X$ that is zero exactly on the edge and positive elsewhere, and a sideways coordinate $Y$. Each off-edge vertex $s$ has a slope $Y(s)/X(s)$. Full-dimensionality forces at least two distinct slopes; the smallest and largest slopes pick out two supporting planes through the edge, and a short argument shows any facet through the edge must use one of those two extreme slopes. Two slopes, two facets. No cones, no abstract face lattice — just the minimum and maximum of finitely many numbers.

The second fact is about a single vertex: the triangles around it form one cycle. This is what rules out a “pinched” vertex where two cones of triangles touch at a point but share no edge. The natural proof wants the fact that the boundary of a convex body is a topological sphere — again, not something lying around. The elementary substitute is a descent argument. Pick a generic linear function; on the link of the vertex it has a unique lowest point, and the one geometric lemma you need is that near a vertex the solid sits inside the cone spanned by its two incident edge directions. From that, every vertex other than the lowest has a neighbor strictly lower, so you can always walk downhill to the bottom — which means the link is connected, hence a single cycle. Connectivity by a potential function, the same trick that shows the $1$-skeleton of a polytope is connected, with none of the topology.

With those two in hand, the seam conditions stop being assumptions. Each edge has its unique opposite side; no directed edge repeats; the fan around each vertex is one orbit. The whole closed-surface skeleton — and with it the consistency of orientations, the fact that the surface is a sphere, the rotation system Cauchy’s argument runs on — is downstream of convexity plus completeness. The user supplies a shape; the seams come for free.

The sharpest field: is the orientation a definition or a theorem?

One field resists, and it is the most interesting one. Each face carries an outward normal, and a compatibility axiom states that the stored normal agrees with the stored cyclic order of the vertices — that the normal points out of the face the way the right-hand rule, applied to the vertex order, says it should. In symbols, with $P_0,P_1,P_2$ the face’s vertices and $n$ its normal, the axiom is

Is that a theorem too? Here one runs into a genuine obstruction. Reflect the whole polyhedron in a mirror. Every unoriented fact survives: the same faces, the same edges, the same support planes, the same convexity. But every triple product flips sign. So no orientation-sensitive quantity can be derived from unoriented data alone — orientation is information you have to put in. It looks, at first, like the one irreducible assumption.

That conclusion is too quick, and the right correction is a small lesson about what a “field” is. The mistake is to store the normal and the cyclic order as two separate pieces of data and then demand an axiom that they match. The normal is redundant. Define it directly from the vertex order as the cross product of two edges,

and the compatibility axiom evaporates: the triple product above becomes $\lVert n\rVert^2$, which is positive for any non-degenerate triangle, no assumption required. The “orientation axiom” was never irreducible; it was the cost of carrying redundant data.

What is left is exactly the orientation that should be left: the cyclic order in which each triangle lists its vertices. And that is not an assumption at all — it is a definition. Choosing the vertex order is choosing an orientation, the way orienting a surface means choosing an atlas; you accept it as part of what it means to specify an oriented polyhedron. The mirror argument, read correctly, says only this: the cyclic order is genuine input, because you cannot recover it from unoriented data. It does not say to keep a normal and an axiom.

This is the distinction the whole exercise turns on. A field of a structure is one of two things. It is data you define — accept it, and do not dress it up as an assumption you failed to eliminate. Or it is a consequence you derive — then prove it from the primitives. There is no third drawer labeled “irreducible field.” Calling a definition an assumption, or leaving a consequence sitting as a hypothesis, are two ways of being unclear about which is which.

Where it lands

After the dust settles, the object a user must hand over is small and honest: the vertex coordinates, the triangle list (whose cyclic orders are the orientation), the plain convexity conditions, and the one geometric completeness hypothesis — the faces are the facets of the hull. Nothing else. The outward normals, the planarity of faces, the outward-orientation inequality, the two-faces-per-edge condition, the single-cycle vertex links, the consistency of orientations, the sphere-ness of the surface — every one of them is now a theorem, checked by the machine against the same three foundational axioms the rest of mathematics rests on.

None of this changes Cauchy’s theorem. It changes the bookkeeping of its hypotheses, which is most of what formalizing a classical result turns out to be: not catching the proof in an error, but being made to say, for each thing you wrote in the structure, whether you are defining it or claiming it. A surface, it turns out, holds together for reasons — and once you are forced to name them, almost nothing about the gluing was ever yours to assume.

依乎天理，批大郤，导大窾。 “Follow the natural lines; strike into the great gaps, guide through the great hollows.” — Zhuangzi, on the cook who carved the ox by its own seams.