UltrapowerRelativeGram.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous Gram orthogonality and orthogonality relative to one extra coefficient. This is the finite two-pass diagonalization in KR02 Lemma 7.12; its coefficient bound is independent of the number of spectral cells.

theorem OAI.WeakPureInfiniteness.ultrapower_relative_cut_gram_row line 18