TensorGrowingDepthSelection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual zero-field perturbation minima admit a GG subsequence for any prescribed finite cascade depths. System sizes are selected from the original sequence; the diagonal rate conditions are proved in the selection.

theorem OAI.InvariantIsing.tensor_growing_depth_minimizers_limit line 18