For a long time, one arm stayed stuck in the wall. Today it came out — but only after breaking three times.

The lemma

The spherical arm lemma (Cauchy, and later Schoenberg–Zaremba) states something the hand already knows: take a convex polygonal arm on the sphere, keep every segment the same length, and open each joint a little wider; then the two endpoints move farther apart. Straighten your elbow and your hand reaches farther.

Believing it is easy. The work is proving that as you open the joints — a continuous process — convexity is preserved frame by frame, and the endpoint moves monotonically outward. In Lean this compresses to an induction on endpoint monotonicity, and every layer of that induction needs one inequality to hold the floor: the opening angle $\delta^*$ plus the angle subtended at some interior vertex must not exceed $\pi$.

Cross $\pi$ and the arm folds back on itself; monotonicity collapses. The whole proof came down to this one bound.

Broken three times

Each time it stuck, it stuck the same way.

What I needed was a fact about this specific opened arm. Each time, I couldn’t resist abstracting it into a prettier, more general lemma — one that would hold for any weakly convex polygon. The first two abstractions (a bound on a turning number; an “at most one support taut at a time” claim) were killed by counterexamples. The third was the most insidious. I reduced the cap to a “weak convex diagonal” statement:

For a planar family of points where every directed edge supports all vertices on its nonnegative side, every increasing triple is also positively oriented.

It looked obviously true. It passed every mechanical check Lean has; #print axioms came back spotless — {propext, Classical.choice, Quot.sound}, not a trace of a sorry. I nearly committed it.

It is false.

A doubled triangle

The counterexample is embarrassingly simple. Take three points in the plane $z=1$,

and walk the same positively oriented triangle twice: $f=(A,B,C,A,B,C)$. Every edge supports every vertex, $\det_3 \ge 0$ throughout (each vertex lands on the edge or its positive side). But the increasing triple $(0,2,4)$ reads off as $A,C,B$ —

The weak hypotheses permit the path to wrap around and retrace itself; the cyclic edge supports cannot see this, but the linear increasing triple sees it plainly.

What makes the example so dangerous is that it hides behind every standard line of defense. Monte-Carlo sampling never lands on it — it is a measure-zero degenerate configuration. Perturbation and limit arguments cannot rescue the statement either, because the doubled triangle is the limit, and the determinant there is exactly $-1$. Every mechanical light turns green, and the claim is still false.

This is the disease #print axioms will never catch: it checks only whether a sorry was used, never whether your hypothesis is vacuous or your statement true. A false lemma, once “proved,” is trusted faithfully. The flaw isn’t in how the foundation was poured — it’s in the bedrock underneath that you took for rock and was quicksand.

This time, an adversarial reviewer (ChatGPT 5.5 Pro) handed me the doubled triangle on sight. Finding the error is good news, not bad: the moment a false proof is caught is the moment the real conclusion is saved.

Cutting along the grain

The way out was one sentence: stop abstracting; return to the structure of the object itself.

The cook in Zhuangzi carves the ox by following its natural seams — “cutting along the grain, guiding the blade through the openings that are already there” — never hacking. This opened arm has its own grain too, and I had been blind to it.

The geometric insight is this: from an interior vertex $A_K$, the angle subtended by any two far-off points $A_r, A_s$ cannot exceed the local joint angle to its two immediate neighbors $A_{K-1}, A_{K+1}$. The chord always lies inside the tangent cone spanned by the adjacent edges. So the cap splits into two pieces:

The top line is a tangent-cone fact about the original strict arm alone — nothing to do with opening, nothing to do with weak supports. The bottom line’s cap comes from a genuine edge support: after opening, the adjacent triple $(K{-}1,K,K{+}1)$ is a real edge, not a diagonal, and its nonnegativity was always there in the structure. Glue the two together (linarith) and the cap is done.

The false “weak diagonal” was deleted outright. The largest angle is the local joint angle, held in check by a real edge support — not the endpoint angle, not a diagonal. Once you see that, the rest is a few pages of trigonometry in the tangent plane.

What a broken arm teaches

The lesson, reduced to something you can act on:

When you’re stuck too long, you’re usually on the wrong road, not short on strength. The same over-generalization failing three times is itself the diagnosis — the move is not to grind harder on the general lemma, but to step back and ask: which specific property of this object do I actually need? Nail the statement to the object’s real structure, and false residues have nowhere left to hide.

Before, it was “one nail short — but the nail was fake and would never go in.” Now the fake nail is replaced by a real one, and driven all the way home. Replace the unprovable with the provable, then finish the proof — that is what it means to close.

Chapter 13, the spherical arm lemma: zero sorry, three clean axioms.

The arm, broken three times, is set.

三折肱，知为良医。 — 《左传·定公十三年》

依乎天理，因其固然。 — 《庄子·养生主》