fd-formalization¶
A complete Lean 4 + Mathlib proof that the \((u,v)\)-flowers have fractal dimension \(\log(u+v)/\log u\), up to box-counting dimension.
What it proves¶
For \(1 < u \leq v\):
| Theorem | Statement | File |
|---|---|---|
| F1 --- log-ratio limit | \(\displaystyle\lim_{g \to \infty} \frac{\log N_g}{\log L_g} = \frac{\log(u+v)}{\log u}\), for the vertex count \(N_g\) and hub distance \(L_g\) defined by recurrences | FlowerDimension.lean |
| F2 --- hub distance | the explicit flower graph on \(\mathrm{Fin}\,N_g\) has distance \(L_g = u^g\) between its hubs, the indices 0 and 1 | FlowerConstruction.lean |
| F3 --- graph dimension | so the flower graphs themselves have log-ratio dimension \(\log(u+v)/\log u\) | FlowerGraphDimension.lean |
| F4 --- box counting | the flower graphs have box-counting dimension \(\log(u+v)/\log u\), along every scale sequence \(\ell_g\) with \(\operatorname{diam} G_g / \ell_g \to \infty\) | FlowerBoxDimension.lean |
Rozenfeld et al. (2007) identify this limit with the box-counting dimension \(d_B\); F4 proves that identification for the explicit graphs.
The library builds with no sorry, and the 78 declarations checked in Verify.lean use only propext, Classical.choice and Quot.sound.
Documentation¶
| Section | Contents |
|---|---|
| Quickstart | Build and verify |
| Proof Strategy | Squeeze argument for F1; cells and box counting for F4 |
| Graph Construction | F2 and F3: gadgets, the distance proof |
| Theorems | Catalog by file |
| Roadmap | What is done, and the scope |
| Prior art | The priority claim and the search behind it |