OAI/Analysis/CircleDomains/Transfer/OrderedGridCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordered compatibility event for the actual reciprocal grid

Only a new label against earlier labels is tested. Each finite earlier sublist is enumerated without repetitions; absolute continuity of the actual grid tuples then transfers the existing product-null failures.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.ae_ordered_band_grid_compatibility line 18