TraceBalloonCutoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth radial balloon cutoffs with one scale-independent derivative constant for each fixed inner-radius ratio. Their derivatives vanish outside the open outer balloon, not just outside its closure.

theorem OAI.CircleDomainRigidity.exists_trace_balloon_cutoffs line 13