Import graph: fix disconnected components

[cameronfreer]

Summary

The full declarations import graph has 5 connected components instead of 1. Some are legitimate islands, but at least one is a bug in the graph generator.

Components

Component	Size	Files	Status
Main	386	Most files	✅
ViaKoopman Cesaro	38	CesaroL2ToL1, CylinderFunctions, KoopmanCommutation, etc.	Bug
Quantization	4	ViaKoopman/Quantization	Unused
ProofPlan	2	ProofPlan	Scaffolding
KallenbergHelper	1	KallenbergHelper	Unused wrapper

Bug: ViaKoopman Cesaro infrastructure (38 nodes)

BlockAverage.lean uses L1_cesaro_convergence_bounded (line 257):

exact L1_cesaro_convergence_bounded hσ f hf hf_bd

But the graph has no edge from BlockAverage declarations to this lemma. The graph generator is missing this dependency - likely because it's only tracking direct imports, not transitive declaration references.

Legitimate islands (candidates for cleanup)

1. Quantization (quantize, quantize_abs_le, quantize_err_le, quantize_tendsto) - ProofPlan.lean says "proved, never used". Consider deleting.

2. ProofPlan (condexp_product_factorization, condexp_product_factorization_general) - Planning scaffolding with placeholder theorems. Consider deleting or moving to docs.

3. KallenbergHelper (ae_comp_of_ae_eq_map) - Thin wrapper around mathlib's ae_eq_comp. Not used anywhere. Consider deleting.

Tasks

• Fix graph generator to track declaration-level usage (not just file imports)
• Delete or document Quantization.lean (unused)
• Delete or move ProofPlan.lean to documentation
• Delete KallenbergHelper.lean (unused wrapper)