CodeRealFreeTrace.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The free-boundary part of the generic-level theorem for an actual real coordinate and an actual coded law, including the residual times.

theorem OAI.CircleDomainRigidity.ae_code_real_free_level_incidence_null line 22