lean-mechanics

What the library covers

About 9,000 lines of Lean and nearly 500 theorems, organised the way a continuum-mechanics textbook is. Results are stated coordinate-free and, where the dimension does not matter, in any finite dimension.

• —Tensor algebra: symmetric and skew parts, invariants and Cayley–Hamilton, the spectral theorem, polar decomposition F = RU = VR, and the representation of isotropic fourth-order tensors.
• —Kinematics and stress: strain measures, objectivity, Saint-Venant compatibility, Cauchy’s theorem by the tetrahedron argument, and the balance laws giving div σ + b = 0 and σ = σᵀ.
• —Constitutive theory: frame indifference, the Rivlin–Ericksen representation theorem, and Saint Venant–Kirchhoff, neo-Hookean and Mooney–Rivlin materials with their linearisations.
• —Linear elastostatics: Clapeyron, Betti reciprocity, Kirchhoff uniqueness, minimum potential energy and Lax–Milgram well-posedness.
• —Beams and plates: Euler–Bernoulli and Timoshenko beams with the limit between them, the Euler buckling load, and Kirchhoff–Love and Mindlin–Reissner plates with Navier solutions.

Assumptions written down, not hidden

Where Mathlib does not yet have the analysis a result needs, such as the divergence theorem on general domains or Korn’s inequality, the library states the missing fact as an explicit hypothesis, lists it in a public GAPS file, and proves the hypothesis can be met by a concrete example. A reader always knows exactly what has been proved and from what.

A paper, checked line by line

The Nexorade folder formalises the 2013 homogenization of reciprocal frames: the four-point-bending stress field of the unit cell, the degenerate plate it produces, its compliance and stiffness, the optimal cell geometry and the Navier solution.