Visualization Modes

Understand color mapping, size mapping, and layout algorithms in Astrolabe.

Astrolabe provides rich visualization options to help you understand different aspects of your Lean 4 project.

Node Type Colors

Nodes are color-coded by their Lean declaration type:

Edge Types

Edges represent dependencies between declarations:

Size Mapping

Node sizes can be mapped to various graph metrics. The base size is calculated as:

size = (node.meta.size ?? defaultSize) × 0.5

Available Size Metrics

Centrality Measures

• PageRank - Importance based on incoming links PR(v) = (1-d)/N + d × Σ(PR(u)/outdeg(u)) where d=0.85

• Betweenness - How often a node lies on shortest paths Higher = more "bridge" nodes

• Katz Centrality - Influence based on all walks Considers both direct and indirect connections

Degree-Based

• In-degree - Number of nodes that depend on this node
• Out-degree - Number of dependencies
• Total degree - Sum of in and out degrees
• Bottleneck Score - indeg(v) / (outdeg(v) + 1) High = many dependents but few dependencies

Clustering Metrics

• Clustering Coefficient - Local density C(v) = 2×|triangles(v)| / (deg(v) × (deg(v)-1))

• Community ID - Color by detected community

Layout Algorithms

Force-Directed (Default)

Physics-based simulation with:

Adaptive Springs

Edge lengths adapt to node density:

• Linear: length = base + (deg1 + deg2) × scale
• Logarithmic: length = base × (1 + log(deg1 + deg2 + 1) × scale)
• Square Root: length = base + √(deg1 + deg2) × scale

Community-Aware Layout

When enabled, edges within the same community are tighter (0.2×) while cross-community edges are looser (5.0×), naturally clustering related nodes.

Radial Layout

Concentric rings centered on a focus node:

• Ring spacing: 8 units per hop distance
• Uses golden angle for even distribution
• Z-axis flattened to 30% for readability

Hierarchical Layout

Tree-like arrangement showing dependency flow:

• Down direction shows ancestors (what this node depends on)
• Up direction shows descendants (what depends on this node)
• Uses BFS for depth calculation

Community Detection

Astrolabe uses the Louvain algorithm by default:

• Optimizes modularity (quality of partition)
• O(n log n) complexity for fast computation
• Resolution parameter adjustable (default 1.0)

Other available algorithms:

• Label Propagation - Fast, non-deterministic
• Spectral Clustering - Based on graph Laplacian
• Hierarchical Clustering - Produces nested structure

Analysis Metrics

Access via the Analysis panel or API:

Graph Statistics

• Node/edge counts, density, diameter
• Connected components, cycles detection
• DAG verification

Centrality

• PageRank, Betweenness, Katz
• Degree distribution

Clustering Analysis

• Local/global clustering coefficients
• Community structure
• Modularity score

Advanced

• Graph entropy measures
• Critical path analysis
• Transitive reduction
• Ricci curvature (geometric properties)

Customization

See Configuration for:

• Custom color themes
• Physics parameter tuning
• Namespace depth settings
• Performance optimization for large graphs