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

In plain words

Hard problems are often first restated. The statement is shown to be equivalent to another one about a transformed object. That restatement is a real theorem, but by itself it proves nothing. In the solved cases the paper examines, the proof came from building a helper setting where an independently established law applies, with a way in and a way back. Weil's proof for curves over finite fields is the model. It moves to a surface built from two copies of the curve, applies a known inequality there, and reads the result back as the bound. The paper calls such a setting a leverage layer.

The method asks four things in order. Why can the statement not be proved yet? Which of six kinds of move fits that reason? Can the needed object be computed or characterized instead of guessed? And if a step still cannot be done, which smaller obligations does it open? A finished finite ladder of obligations proves the original statement; a cycle of local steps does not. On a chessboard with two opposite corners removed, exact linear algebra produces the classic colouring argument without being told about colours, and the paper proves it is the only linear certificate up to scale.

Eight solved theorems are replayed, from Weil's theorem on curves to Green and Tao on primes in arithmetic progression, Park and Pham on the Kahn Kalai conjecture, and Perelman on the Poincaré conjecture. Each replay starts from the restatement, reports the same fields, and marks where the method guided the construction and where invention was still needed. The supporting theorems are elementary, and they are formalized in Lean.

What it shows

• A precise notion of a leverage layer: a way in, an independently established law, and a way back.
• A diagnosis step, six kinds of move, and construction tools that compute rather than guess.
• The chessboard colouring is the unique linear certificate up to scale, and computation finds it.
• Fifteen failure signatures for plausible constructions that go wrong.
• Eight replays of solved theorems, each marking where invention was needed.

What it does not claim

The method does not find a layer or guarantee that one exists. The replays were written by an author who knew the answers, so they are worked examples, not evidence of discovery power. Nothing is claimed about any open problem.

Cite

Tsiokos, I. (2026). Building What a Proof Needs: A Method for Constructing Leverage Layers. Zenodo. https://doi.org/10.5281/zenodo.23097947