CodePeriodFreeTrace.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Free-point avoidance for a masked period coordinate. Narrow patches are selected from its bounded branch atlas; none are assumed as extra data. All path-law and independent-level inputs are those of the actual base code; no free-incidence conclusion is assumed.

theorem OAI.CircleDomainRigidity.ae_code_period_free_level_incidence_null line 20