The Right Isosceles Triangle: A Mathematical Perpetuum Mobile — with Verification in Lean 4

We unfold the deep self-similarity of the right isosceles triangle, showing that it is not merely a geometric figure but a universal standard, a perpetual cycle of abstraction and return. The triangle’s transformation (halving by the hypotenuse and rescaling) closes an identity loop, encoding rationality–irrationality–rationality, unity–duality–unity, and identity–difference–identity. We formalise this cycle in the proof assistant Lean 4, defining the structure, the folding and rescaling operations, and proving that the composite operation is the identity on the standard triangle. The verification demonstrates that the self-similarity is a logical consequence of the defining Pythagorean relation, turning a philosophical insight into a formal theorem.