(u,v)-Flower Log-Ratio Convergence — Lean 4 Formalization

Formal verification of the vertex-count / hub-distance log-ratio limit for the (u,v)-flower network family, from:

H. D. Rozenfeld, S. Havlin & D. ben-Avraham, "Fractal and transfractal recursive scale-free nets," New Journal of Physics 9, 175 (2007).

What is verified

For the arithmetic (u,v)-flower model, the log-ratio of vertex count to hub distance converges to log(u+v) / log(u):

lim   log |V_g| / log L_g  =  ln(u + v) / ln(u)    for 1 < u ≤ v
g→∞

In the physics literature (Rozenfeld et al. 2007), this quantity equals the box-counting fractal dimension d_B. This formalization proves the log-ratio convergence and that the hub distance in the explicit SimpleGraph construction equals u^g (see F2 bridge below). A formal bridge to a box-counting dimension definition is future work (see debt.md).

This is the ground truth formula that navi-fractal calibrates its sandbox dimension estimates against (see the calibration table in that project's README).

Proof spine

Step	Declaration	File	Topic
Edge count	flowerEdgeCount_eq_pow	FlowerCounts	E_g = (u+v)^g
Vertex count	flowerVertCount_eq	FlowerCounts	(w-1) N_g = (w-2) w^g + w
Two-sided bounds	flowerVertCount_lower/upper	FlowerCounts	Squeeze inputs
Monotonicity	flowerVertCount_strict_mono etc.	FlowerCounts/FlowerDiameter	N_g, E_g, L_g strictly increasing
Hub distance	flowerHubDist_eq_pow	FlowerDiameter	L_g = u^g
Hub vertices	hub0, hub1	FlowerGraph	Distinguished vertices
Graph construction	flowerGraph', flowerGraph	FlowerConstruction	Explicit SimpleGraph on FlowerVert / Fin
Connectivity	flowerGraph'_connected	FlowerConstruction	Flower graph is connected
F2 bridge	flowerGraph_dist_hubs	FlowerConstruction	SimpleGraph.dist hub0 hub1 = u^g
Log identities	log_flowerHubDist_eq etc.	FlowerLog	log L_g = g · log u
Log-ratio limit	flowerDimension	FlowerDimension	lim log N_g / log L_g = log(u+v) / log(u)

Upstream candidates

Declaration	File	Topic	Mathlib status
SimpleGraph.ball + 7 core lemmas	GraphBall	Open metric ball via edist (8 core + 6 convenience lemmas)	No SimpleGraph.ball in Mathlib; PR ready to open
pathGraph_edist, pathGraph_dist + 2 corollaries	PathGraphDist	Distance in path graphs = index difference	No distance lemmas for pathGraph in Mathlib

Axiom boundary

Zero custom axioms. All results proved from Mathlib primitives. The #print axioms dashboard in Verify.lean confirms every declaration depends only on [propext, Classical.choice, Quot.sound] with no sorryAx.

The log-ratio theorem uses pure arithmetic recurrences for vertex count and hub distance. The F2 bridge (flowerGraph_dist_hubs) additionally proves that SimpleGraph.dist on the explicit graph construction equals u^g, connecting the arithmetic formula to graph-theoretic distance. A formal box-counting dimension definition remains future work (see debt.md).

Hypotheses

• 1 < u — excludes the transfractal case (u = 1 gives infinite d_B)
• u ≤ v — WLOG normalization from the source paper

Building

Requires Lean 4 (v4.28.0) and Mathlib.

lake build
lake build --wfail   # fail on any sorry or warning

Project structure

FdFormal/
  GraphBall.lean         — SimpleGraph.ball (open ball via edist), 8 core + 6 convenience lemmas (upstream candidate)
  FlowerGraph.lean       — Hub vertices and structural helpers
  FlowerCounts.lean      — Exact edge/vertex count formulas, bounds, monotonicity
  FlowerDiameter.lean    — Hub-distance scaling L_g = u^g, cast identities
  FlowerLog.lean         — Log identities and squeeze-sandwich bounds
  FlowerLogRatio.lean    — HasLogRatioDimension definition (F3 bridge target)
  FlowerDimension.lean   — Headline theorem: log-ratio limit = log(u+v) / log(u)
  PathGraphDist.lean     — pathGraph distance lemmas (upstream candidate)
  FlowerConstruction.lean — F2 bridge: SimpleGraph construction + dist = u^g
  Verify.lean            — #print axioms dashboard (27 declarations)

Mathematical background

The (u,v)-flower is a deterministic recursive network: start with two vertices connected by an edge (generation 0), then at each generation replace every edge with two parallel paths of lengths u and v. For u > 1, the physics literature identifies this as a fractal network with finite box-counting dimension d_B = log(u+v)/log(u). For u = 1, the network is transfractal (small-world).

The log-ratio convergence proof (Route B — squeeze) works as follows:

1. Two-sided bounds: c₁ · w^g ≤ N_g ≤ c₂ · w^g where w = u + v
2. Hub distance: L_g = u^g
3. Decompose log(N_g) / (g · log u) = residual + log(w) / log(u)
4. Squeeze the residual to 0 between log(c₁) / (g · log u) and log(2) / (g · log u)
5. The limit is log(u + v) / log(u)

Key references

• Rozenfeld, Havlin & ben-Avraham, NJP 9:175 (2007) — construction and dimension formula
• Song, Havlin & Makse, Nature 433:392 (2005) — fractal self-similarity of complex networks
• Furuya & Yakubo, Phys. Rev. E 84:036118 (2011) — multifractal spectrum (future work)

Development Process

What the author did: The formalization architecture — the proof spine (counts + bounds → hub distance → squeeze limit → graph construction → distance bridge), the structured-gadget approach for FlowerConstruction, and the zero-axiom target — is the core contribution. The underlying mathematics is from Rozenfeld et al. 2007.

What AI tools did: Claude Opus assisted with Lean 4 syntax, Mathlib API navigation, and proof term synthesis. Aristotle (Harmonic) independently proved leaf lemmas (positivity, monotonicity, cast identities) via automated proof search, and contributed proof simplification — eliminating intermediate bindings, converting tactic proofs to term mode, and inlining redundant variables. These roles are analogous to omega, aesop, and other proof automation — the strategy is human, the term-level search and cleanup is machine-assisted.

Verification: The final arbiter is the Lean compiler:

lake build --wfail   # type-checks or it doesn't

License

Copyright 2026 Nelson Spence. Licensed under Apache 2.0.