Building What a Proof Needs: A Method for Constructing Leverage Layers

Abstract

Hard problems are often first reformulated: the statement is shown equivalent to another about a transformed object. Such a reformulation is a theorem, but by itself it supplies no independently established law from which the new statement follows. In the solved cases examined, proofs came from building an auxiliary setting where an independently established law applies, with a way in and a way back. We call such a setting a leverage layer, and give a method for constructing one. The method diagnoses why the statement cannot yet be proved, chooses one of six kinds of move, and tries tools that compute or characterize the needed object instead of guessing it. An obligation that cannot yet be met opens explicit child obligations, and a completed finite ladder of them proves its root. On a mutilated chessboard it computes the classical colouring argument, which we prove is the unique linear certificate up to scale. The supporting theorems are elementary and formalized in Lean. We replay eight solved theorems, from Weil's theorem on curves to Perelman's proof of the Poincaré conjecture, marking where the method guided the construction and where invention was needed. The replays are worked examples, not evidence of discovery power.