=== lean4-0001: guardCycle List vs HashSet ===
N=100  : defective=0.125ms  fixed=0.021ms  speedup=6.0x
N=500  : defective=3.103ms  fixed=0.139ms  speedup=22.3x
N=1000 : defective=12.449ms  fixed=0.300ms  speedup=41.4x
N=2000 : defective=40.612ms  fixed=1.025ms  speedup=39.6x

=== lean4-0002: inductive type check std::find vs set ===
K=N=100 : defective=0.206ms  fixed=0.004ms  speedup=57.6x
K=N=500 : defective=5.312ms  fixed=0.016ms  speedup=325.6x
K=N=1000: defective=18.706ms  fixed=0.030ms  speedup=629.7x

=== lean4-0003: fresh name generation ===
N=100  : defective=0.167ms  fixed=0.004ms  speedup=44.0x
N=500  : defective=4.501ms  fixed=0.022ms  speedup=206.1x
N=1000 : defective=17.938ms  fixed=0.049ms  speedup=369.1x

=== lean4-0004: ir_interpreter double-checked lock race (correctness) ===
threads=2  ops=500 : defective_lost_updates(max)= 490 fixed_lost_updates(max)=   0
threads=4  ops=500 : defective_lost_updates(max)=1084 fixed_lost_updates(max)=   0
threads=8  ops=500 : defective_lost_updates(max)= 994 fixed_lost_updates(max)=   0

=== lean4-0005: Lake jobreg IO.Ref.modify race (correctness) ===
workers=4  pushes=200 : expected=800   defective_lost(max)= 599 fixed_lost(max)=   0
workers=8  pushes=200 : expected=1600  defective_lost(max)=1400 fixed_lost(max)=   0
workers=16 pushes=200 : expected=3200  defective_lost(max)=2993 fixed_lost(max)=   0

=== lean4-0006: kernel/trace g_opts thread-local leakage (correctness) ===
threads=2  tasks=200 : defective_leakages(max)=  199 fixed_leakages(max)=    0
threads=4  tasks=400 : defective_leakages(max)=  399 fixed_leakages(max)=    0
threads=8  tasks=800 : defective_leakages(max)=  798 fixed_leakages(max)=    0

=== lean4-0007: process.cpp Windows env vars list-count vs unordered_set ===
N=100  : defective=0.315ms  fixed=0.028ms  speedup=11.2x
N=500  : defective=4.737ms  fixed=0.127ms  speedup=37.4x
N=1000 : defective=19.896ms  fixed=0.281ms  speedup=70.9x
N=2000 : defective=23.665ms  fixed=0.171ms  speedup=138.0x

