ProductSoundness.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The final graph product inherits the alphabet-independent repetition estimate through its proved uniform occurrence law and arbitrary-local-strategy bridge. The only input soundness premise is the base graph's actual finite maximum.

theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_soundness_rate line 27
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_soundness line 34
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_explicit_soundness line 40
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_soundness_rate line 55
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_soundness line 63
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_explicit_soundness line 70

theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_soundness_rate line 93

Source documentation

Soundness for the actual globally numbered, fully tabulated output.

theorem output_soundness_rate (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t)
    (hvalue : Integration.InstanceValue.value H ≤ 1 - (1 : ℝ) / 800) :
    Integration.InstanceValue.value (output H presentation t ht) ≤
      (1 - (1 : ℝ) / 10240000) ^ t := by
…

Mentions: OAI.MaxCutGames.Integration.InstanceValue.value, OAI.MaxCutGames.Explicit.ProductPaddedOutput.output

theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_soundness line 104

def OAI.MaxCutGames.FinishReduction.of_matrix_reduction line 135

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.MaxCutGames.ParameterSelection.OuterParameters, OAI.MaxCutGames.BinaryLanguage.language