feat: scaffold fd-formalization repo

Lean 4 + Mathlib project for formalizing the (u,v)-flower analytical
dimension formula d_B = ln(u+v)/ln(u) from Rozenfeld et al. (NJP 2007).

Proof spine: FlowerGraph -> FlowerCounts -> FlowerDiameter -> FlowerDimension.
Zero axioms target. GraphBall.lean is an upstream Mathlib candidate using
edist (not dist) for correct handling of disconnected graphs.

Includes: lakefile.toml, CI workflow (SHA-pinned), pre-commit hooks,
copyright checker, mathlib-playbook conventions, debt tracker.

Builds clean with `lake build --wfail` against Mathlib v4.28.0.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: Fieldnote-Echo

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,52 @@
+name: Lean CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+env:
+  ELAN_HOME: /home/runner/.elan
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
+
+      - name: Install elan and toolchain
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "${ELAN_HOME}/bin" >> "${GITHUB_PATH}"
+          export PATH="${ELAN_HOME}/bin:${PATH}"
+          elan --version
+          elan show
+
+      - name: Cache Lake build artifacts
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: .lake
+          key: lake-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}
+          restore-keys: lake-
+
+      - name: Get Mathlib cache
+        run: lake exe cache get || true
+
+      - name: Build (fail on sorry)
+        run: lake build --wfail
+
+      - name: Lint (Mathlib environment linters)
+        run: lake lint
+
+      - name: Check for sorry contamination
+        run: |
+          echo "Checking axiom dependencies..."
+          touch FdFormal/Verify.lean
+          lake env lean FdFormal/Verify.lean 2>&1 | tee verify_output.txt
+          if grep -q "sorryAx" verify_output.txt; then
+            echo "FATAL: sorryAx found in verified theorems!"
+            exit 1
+          fi
+          echo "No sorry contamination detected."

.gitignore

@@ -0,0 +1,6 @@
+/.lake
+/lake-packages
+
+/build
+/archive
+/docs/internal

.pre-commit-config.yaml

@@ -0,0 +1,15 @@
+repos:
+  - repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v6.0.0
+    hooks:
+      - id: trailing-whitespace
+      - id: end-of-file-fixer
+      - id: check-merge-conflict
+  - repo: local
+    hooks:
+      - id: check-copyright
+        name: Mathlib copyright header (Lean files)
+        entry: scripts/check-copyright.sh
+        language: script
+        files: \.lean$
+        exclude: \.lake/

FdFormal.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import FdFormal.GraphBall
+import FdFormal.FlowerGraph
+import FdFormal.FlowerCounts
+import FdFormal.FlowerDiameter
+import FdFormal.FlowerDimension
+import FdFormal.Verify

FdFormal/FlowerCounts.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import FdFormal.FlowerGraph
+import Mathlib.Tactic
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-!
+# Flower Graph Exact Counts
+
+Exact formulas for the edge and vertex counts of (u,v)-flower graphs
+at generation `g`. With `w = u + v`:
+
+- **Edges:** `E_g = w^g`
+- **Vertices:** `(w - 1) * N_g = (w - 2) * w^g + w`
+
+These are proved by induction on `g` from the construction rule:
+each edge is replaced by two parallel paths of lengths `u` and `v`,
+contributing `(u - 1) + (v - 1) = w - 2` new internal vertices per
+edge and multiplying the edge count by `w`.
+
+## Main statements
+
+- `flower_edge_count` — `E_g = w^g`
+- `flower_vertex_count` — `(w - 1) * N_g = (w - 2) * w^g + w`
+
+## References
+
+- [Rozenfeld2007] §2, construction and counting formulas.
+-/
+
+-- TODO: State and prove edge_count and vertex_count once FlowerGraph
+-- construction is defined.
+--
+-- The edge count E_g = w^g follows directly: each edge produces w
+-- new edges (u edges on the short path + v edges on the long path).
+--
+-- The vertex count uses the recurrence:
+--   N_{g+1} = N_g + (w - 2) * E_g
+--            = N_g + (w - 2) * w^g
+-- with N_0 = 2 (two hub vertices connected by a single edge).
+-- Solving: (w-1) * N_g = (w-2) * w^g + w.
+--
+-- Real-valued wrappers for the headline theorem:
+--   def V_count_real (u v g : ℕ) : ℝ := (N_g : ℝ)
+-- Cast early, prove positivity lemmas here.

FdFormal/FlowerDiameter.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import FdFormal.FlowerGraph
+import Mathlib.Tactic
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-!
+# Flower Graph Diameter Scaling
+
+The diameter of the (u,v)-flower at generation `g` scales as `u^g`
+for `u > 1`. The shortest path between the two hub vertices traverses
+the shorter parallel path (of length `u`) at each generation, giving
+`L_g = u^g`.
+
+## Main statements
+
+- `flower_diam_eq` — `L_g = u^g` (or asymptotic bound if exact
+  formula requires parity analysis)
+
+## Implementation notes
+
+The exact diameter formula `L_g = u^g` holds because:
+1. The two original hubs are at distance `u^g` (the short path
+   recurses through `g` generations).
+2. No pair of vertices can be farther apart (the long path of
+   length `v^g` between hubs provides an alternative route, but
+   `u ≤ v` means internal vertices on the long path are closer
+   to a hub than the hub-to-hub distance).
+
+For the headline theorem, we need `Real.log L_g / g → Real.log u`,
+which follows from `L_g = u^g` and `Real.log (u^g) = g * Real.log u`.
+
+## References
+
+- [Rozenfeld2007] §2, diameter analysis.
+-/
+
+-- TODO: State and prove diameter formula once FlowerGraph is defined.
+--
+-- Real-valued wrapper:
+--   def L_diam_real (u v g : ℕ) : ℝ := (L_g : ℝ)
+-- Cast early, prove positivity (L_g > 0 for g ≥ 1, u > 1).

FdFormal/FlowerDimension.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import FdFormal.FlowerCounts
+import FdFormal.FlowerDiameter
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Tactic
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-!
+# Fractal Dimension of (u,v)-Flower Graphs
+
+The fractal dimension of the (u,v)-flower family (for `1 < u`, `u ≤ v`)
+is `d_B = Real.log (u + v) / Real.log u`.
+
+This is derived from the exact growth laws:
+- `|V_g|` grows like `(u+v)^g` (from `FlowerCounts`)
+- `L_g = u^g` (from `FlowerDiameter`)
+
+So `Real.log |V_g| / Real.log L_g` → `Real.log (u+v) / Real.log u`
+as `g → ∞`.
+
+## Main statements
+
+- `flower_dimension` — the headline theorem:
+  `Filter.Tendsto (fun g ↦ Real.log (V_count_real u v g) /
+    Real.log (L_diam_real u v g))
+    Filter.atTop (nhds (Real.log (u + v) / Real.log u))`
+
+## Implementation notes
+
+Counts and diameters are cast to `ℝ` via explicit wrapper definitions
+(`V_count_real`, `L_diam_real`) defined in `FlowerCounts` and
+`FlowerDiameter`. This avoids implicit coercion fights.
+
+The proof uses:
+- `Real.log_pow` — `Real.log (x ^ n) = n * Real.log x`
+- `Real.log_pos` — `1 < x → 0 < Real.log x`
+- `Filter.Tendsto` for the limit statement
+
+The u = 1 case is excluded by hypothesis (`1 < u`). The source
+treatment identifies u = 1 as transfractal with infinite d_B.
+
+## References
+
+- [Rozenfeld2007] Theorem 1, fractal dimension formula.
+- [Spence2026] navi-fractal calibration against this formula.
+-/
+
+-- TODO: State and prove flower_dimension once FlowerCounts and
+-- FlowerDiameter provide the exact formulas.
+--
+-- Proof sketch:
+--   Real.log (V_count_real u v g) / Real.log (L_diam_real u v g)
+--   = Real.log (C * (u+v)^g) / Real.log (u^g)      [by FlowerCounts]
+--   = Real.log (C * (u+v)^g) / (g * Real.log u)     [by log_pow]
+--   = (Real.log C + g * Real.log (u+v)) / (g * Real.log u)  [by log_mul]
+--   → Real.log (u+v) / Real.log u  as g → ∞         [C term vanishes]

FdFormal/FlowerGraph.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Tactic
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-!
+# (u,v)-Flower Graph Construction
+
+Recursive construction of the (u,v)-flower network family from
+Rozenfeld, Havlin & ben-Avraham (NJP 2007).
+
+## Construction rule
+
+At each generation, every edge is replaced by two parallel paths of
+lengths `u` and `v` (with `1 < u` and `u ≤ v`). The case `u = 1`
+produces transfractal (small-world) networks with infinite box-counting
+dimension and is excluded from this formalization.
+
+## Main definitions
+
+- `FlowerGraph` — the (u,v)-flower at generation `g`
+
+## Implementation notes
+
+Uses a custom recursive vertex type rather than quotient-identification.
+The vertex type grows with each generation as new intermediate vertices
+are inserted along subdivided edges. Hub vertices from generation 0 are
+tracked through the recursion.
+
+The representation prioritizes proof tractability over computational
+efficiency — boring wins in Lean.
+
+## References
+
+- [Rozenfeld2007] Rozenfeld, Havlin & ben-Avraham, "Fractal and
+  transfractal recursive scale-free nets," NJP 9:175 (2007).
+-/
+
+-- TODO: Define FlowerGraph construction.
+-- The key design decision is the vertex type representation.
+-- Options considered:
+--   (a) Fin-indexed: FlowerGraph on Fin (V_count u v g)
+--   (b) Inductive vertex type with generation tags
+--   (c) Sigma type: Σ (e : edges of gen g-1), Fin (path_len - 1)
+--
+-- Option (a) is simplest for Fintype instances but hardest for
+-- tracking hub identity across generations.
+-- Option (c) is closest to the mathematical construction but
+-- requires careful handling of hub merging.
+--
+-- This file will be filled in during implementation.

FdFormal/GraphBall.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+import Mathlib.Combinatorics.SimpleGraph.Metric
+import Mathlib.Combinatorics.SimpleGraph.Finite
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-!
+# Graph Balls via Extended Distance
+
+Defines the metric ball on a `SimpleGraph` using `edist` (not `dist`),
+so that disconnected vertices are correctly excluded (they have
+`edist = ⊤`, not `dist = 0`).
+
+## Main definitions
+
+- `SimpleGraph.ball` — the set of vertices within extended distance `r`
+  of a center vertex `c`
+
+## Main statements
+
+- `SimpleGraph.mem_ball` — membership characterization
+- `SimpleGraph.ball_mono` — monotonicity in radius
+
+## Implementation notes
+
+This file is designed as an upstream Mathlib candidate. It has no
+project-specific imports. The definition and basic API work on
+arbitrary vertex types; finiteness lemmas requiring `[Fintype V]`
+are separated into their own section.
+
+## References
+
+- Mathlib `SimpleGraph.Metric` for `edist`
+-/
+
+namespace SimpleGraph
+
+variable {V : Type*} (G : SimpleGraph V)
+
+/-- The ball of radius `r` around vertex `c` in the graph metric.
+    Uses `edist` so that unreachable vertices (at distance `⊤`) are
+    correctly excluded. -/
+def ball (c : V) (r : ℕ∞) : Set V :=
+  {v | G.edist c v ≤ r}
+
+@[simp]
+theorem mem_ball {c : V} {v : V} {r : ℕ∞} :
+    v ∈ G.ball c r ↔ G.edist c v ≤ r :=
+  Iff.rfl
+
+theorem ball_mono {c : V} {r₁ r₂ : ℕ∞} (h : r₁ ≤ r₂) :
+    G.ball c r₁ ⊆ G.ball c r₂ :=
+  fun _ hv ↦ le_trans hv h
+
+theorem center_mem_ball {c : V} {r : ℕ∞} :
+    c ∈ G.ball c r := by
+  simp [ball, SimpleGraph.edist_self]
+
+/-! ### Finiteness lemmas
+
+These require `[Fintype V]` or similar finiteness assumptions. -/
+
+section Finite
+
+variable [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
+
+-- TODO: card_ball_mono, card_ball_nonneg, etc.
+-- These will be proved once the ball API is exercised by FlowerScaling.
+
+end Finite
+
+end SimpleGraph