MatrixGap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed finite matrix reduction obtained from the actual v2 latent gadget, dimension-uniform shortcode inverse, sparse full-table law and private local decoder. The construction precedes the parity input and its accuracy. No inverse, noise, spectral, or decoder certificate is supplied as a premise.

theorem OAI.MaxCutGames.Decoder.MatrixGap.exists_parameters line 14