Solid arrows are independently checked theorem prerequisites. Dashed arrows are conservative notation dependencies, never proof steps.