OAI/Computability/UniqueGames/Reduction/FinishReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The concrete final composition, once the matrix reduction has been proved. This constructor copies the actual occurrence list, subdivides every occurrence into four edges, and runs the full tuple-product machine. Its hypotheses are the matrix reduction's actual value bounds and finite-machine computation. It is an intermediate composition theorem, not the unconditional endpoint.

  1. def OAI.UniqueGamesTheorem.FinishReduction.of_matrix_reduction line 31

    Source documentation

    Compose the proved matrix reduction with the explicit three-stage finish. All parameters, machines, alphabets, and time polynomials precede the input. The original raw binary input codec is retained by sequential composition.

    def of_matrix_reduction {ε δ : ℝ} (P : ParameterSelection.OuterParameters ε δ)
    {q s : ℕ} (hq : 2 ≤ q) (hs : 1 ≤ s)
    (coordinates : Fin q ≃ BinaryLinear.Vector s)
    (matrix : List Bool → Instance q)
    (translations : ∀ input, TranslationTarget.IsTranslationInstance coordinates (matrix input))
    (computation : Turing.TM2ComputableInPolyTime (id : List Bool → List Bool)
      gameBits matrix)
    (finiteAlphabet : MachineFiniteAlphabet.FiniteAlphabet computation.tm)
    (d : ℚ) (hd : d ≤ P.epsilon0 / P.repetitions)
    (complete : ∀ input, BinaryLanguage.language input →
      1 - (d : ℝ) ≤ InstanceValue.value (matrix input))
    (sound : ∀ input, ¬BinaryLanguage.language input →
…

    Mentions: OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters, OAI.UniqueGamesTheorem.BinaryLanguage.language