3.1. Total and self time🔗

For an event e, total time is its nonnegative interval length:

\operatorname{total}(e)=\max(0,\operatorname{end}(e)-\operatorname{start}(e))

Self time subtracts the covered union of immediate same-thread child intervals:

\operatorname{self}(e) =\operatorname{total}(e) -\min(\operatorname{total}(e),\operatorname{coveredChildren}(e))

The union prevents overlapping malformed children from being counted twice. Child intervals are clipped to the parent before diagnostic subtraction. The validator still reports the malformed relationship.

A grandchild lies inside an immediate child in a valid nesting tree, so subtracting immediate children is enough. Cross-thread logical children remain linked but are not subtracted.

LeanProfiler proves the inclusive bounds used by this calculation:

#check LeanProfiler.EventTiming.selfNs_le_inclusiveNs
#check LeanProfiler.EventTiming.selfHeartbeats_le_inclusiveHeartbeats
#check LeanProfiler.analyze_timings_areConsistent

These theorems describe the analyzer. They do not prove that the clock has a particular physical resolution or that the profiled action implements its intended algorithm.