feat: scaffold fd-formalization repo

[Nelson Spence (Fieldnote-Echo)]

Summary

• Lean 4 + Mathlib project scaffold for formalizing the (u,v)-flower fractal dimension formula d_B = ln(u+v)/ln(u) (Rozenfeld et al., NJP 2007)
• Proof spine: FlowerGraph -> FlowerCounts -> FlowerDiameter -> FlowerDimension (zero axioms target)
• GraphBall.lean defines SimpleGraph.ball via edist (upstream Mathlib candidate)
• CI: lake build --wfail, lake lint, sorry contamination check (SHA-pinned actions)
• Conventions: mathlib-playbook compliant (style linters, copyright hooks, fun x ↦, Type*)
• Builds clean against Mathlib v4.28.0

Design decisions

• edist not dist for GraphBall (dist returns 0 for unreachable vertices)
• Hypotheses: 1 < u, u ≤ v (excludes transfractal u=1 case)
• Proof spine: counts/diameter/log-ratio, NOT ball-recurrence-first
• Vertex representation: TBD — key implementation risk tracked in debt.md
• FlowerDiameter: expected to be hardest file (~3x longest), flagged in debt.md

Test plan

• lake build --wfail passes locally
• #print axioms shows no sorryAx for GraphBall declarations
• Pre-commit hooks pass (copyright, trailing whitespace, EOF)
• CI workflow runs on GitHub

🤖 Generated with Claude Code