DomainMeetingBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior meetings of two independent laws are bounded by their local occupation energies. The geometric small-ball constant is kept explicit.

theorem OAI.CircleDomainRigidity.domain_meeting_bound_of_ball_area line 19