TensorSpectralGGExistence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual finite perturbation minima have subsequential spectral path identification, conditional only on the precise published concentration inputs.

theorem OAI.InvariantIsing.tensorPerturbation_exists_identified_GG_limit line 15