RecursiveLawSelection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Retaining every predecessor in a well-ordered construction. The selection hypothesis is discharged by the positive-law construction in the application.

theorem OAI.CircleDomainRigidity.exists_recursive_code_laws line 20