CodeBranchFreeTrace.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Free-point avoidance for a prior coordinate described by countably many local real branches. 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_branch_free_level_incidence_null line 20