%% ECRuntime proof architecture, by family
%% Generated by scripts/audit.lean from real proof dependencies.
%% An edge means a proof or statement mentions the target.

graph BT
  n_Foundations["Foundations<br/><small>4 modules</small>"]
  n_Generic_runtime_theory["Generic runtime theory<br/><small>129 modules</small>"]
  n_LeadingOnes["LeadingOnes<br/><small>155 modules</small>"]
  n_Objectives___asymptotics["Objectives & asymptotics<br/><small>45 modules</small>"]
  n_RLS___coupon_collector["RLS & coupon collector<br/><small>130 modules</small>"]
  n_Static_unary_unbiased["Static unary-unbiased<br/><small>44 modules</small>"]
  n_Trajectory_semantics["Trajectory semantics<br/><small>13 modules</small>"]
  n_Witt_scaled_rate_c_n["Witt scaled rate c/n<br/><small>15 modules</small>"]
  n_Witt_standard_rate_1_n["Witt standard rate 1/n<br/><small>12 modules</small>"]

  n_RLS___coupon_collector -->|178| n_Static_unary_unbiased
  n_RLS___coupon_collector -->|173| n_Foundations
  n_LeadingOnes -->|155| n_Trajectory_semantics
  n_LeadingOnes -->|153| n_Foundations
  n_Generic_runtime_theory -->|140| n_Trajectory_semantics
  n_RLS___coupon_collector -->|133| n_Generic_runtime_theory
  n_Static_unary_unbiased -->|125| n_Foundations
  n_Generic_runtime_theory -->|101| n_Foundations
  n_Objectives___asymptotics -->|98| n_Foundations
  n_RLS___coupon_collector -->|58| n_Objectives___asymptotics
  n_Objectives___asymptotics -->|57| n_Generic_runtime_theory
  n_Witt_scaled_rate_c_n -->|53| n_Objectives___asymptotics
  n_Witt_scaled_rate_c_n -->|45| n_Foundations
  n_RLS___coupon_collector -->|44| n_Trajectory_semantics
  n_Witt_standard_rate_1_n -->|42| n_Foundations
  n_LeadingOnes -->|41| n_Generic_runtime_theory
  n_Objectives___asymptotics -->|36| n_Trajectory_semantics
  n_Objectives___asymptotics -->|35| n_Static_unary_unbiased
  n_Witt_standard_rate_1_n -->|35| n_Objectives___asymptotics
  n_Static_unary_unbiased -->|27| n_Objectives___asymptotics
  n_Generic_runtime_theory -->|24| n_LeadingOnes
  n_Witt_scaled_rate_c_n -->|22| n_Generic_runtime_theory
  n_Static_unary_unbiased -->|17| n_Generic_runtime_theory
  n_Witt_scaled_rate_c_n -->|14| n_Witt_standard_rate_1_n
  n_Trajectory_semantics -->|13| n_Foundations
  n_Static_unary_unbiased -->|12| n_Trajectory_semantics
  n_Witt_scaled_rate_c_n -->|12| n_Trajectory_semantics
  n_Witt_standard_rate_1_n -->|12| n_Generic_runtime_theory
  n_Generic_runtime_theory -->|11| n_Static_unary_unbiased
  n_Witt_standard_rate_1_n -->|8| n_Trajectory_semantics
  n_LeadingOnes -->|6| n_Objectives___asymptotics
  n_Generic_runtime_theory -->|5| n_RLS___coupon_collector
  n_Static_unary_unbiased -->|3| n_LeadingOnes
  n_Trajectory_semantics -->|3| n_Generic_runtime_theory
  n_Objectives___asymptotics -->|2| n_RLS___coupon_collector
  n_Generic_runtime_theory -->|1| n_Objectives___asymptotics
  n_Objectives___asymptotics -->|1| n_LeadingOnes
  n_RLS___coupon_collector -->|1| n_LeadingOnes

  classDef facade stroke-width:3px,stroke:#1d7a55,fill:#e7f4ee,color:#12291f;
  classDef orphan stroke-dasharray:4 3,stroke:#96620f,fill:#fbf1de,color:#2a2113;