1 Scope and status

This is the standard Lean blueprint dependency graph for the project. Hardy’s theorem is proved and the exact frozen statement passes the local Comparator check. Sharp Five Exponentials is the next research target. Work on Four Exponentials follows a successful Sharp Five proof.

The graph contains every declaration exported from the compiled project environment. The edges between those declarations come from their Lean types and proof terms. Open proof steps have planned edges. They have no completed proof marker. A green proposition definition states a target; it does not prove that target. The open target nodes below record this distinction.

Click a graph node to read its statement and status. Use its Lean link to open the checked source with hover information.