OAI/Computability/MaxCut/Encoding/MatrixGapInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual matrix reduction assembled from the gadget and decoder. The dimension-uniform shortcode inverse is the sole explicit mathematical input here. This intermediate theorem is not an unconditional endpoint until that input is supplied by the independently proved KMS foundation.

  1. theorem OAI.MaxCutGames.Decoder.MatrixGap.parameters_of_inverse line 19