TraceTruncationWeak.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Truncating a continuous zero trace produces genuine global weak partial derivatives, supported away from the excluded closed set.