OAI/Computability/MaxCut/Games/Weighted.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MaxCutGames.Reduction.WeightedSource.RationalSource line 13
2. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.denominator line 25
3. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.denominator_positive line 27
4. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.den_dvd_denominator line 30
5. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.numerator line 34
6. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.numerator_cast line 37
7. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.weight_eq_ratio line 54

   Source documentation

   Exact rational-to-integer conversion, not an approximation.

   theorem weight_eq_ratio (i : Fin S.occurrences) :
       S.weight i = (S.numerator i : ℚ) / S.denominator := by
   …

8. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.numerators line 60
9. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.length_numerators line 62
10. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.sum_numerators line 65
11. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.equationAt line 71
12. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.equationAt_fin line 74
13. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedEquations line 77
14. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedEquations_length line 80
15. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedEquations_nonempty line 84
16. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedEquations_origin line 92

    Source documentation

    Rounding copies complete equation records without altering any of their slots.

    theorem roundedEquations_origin (D : Nat) (e : Eqn) (he : e ∈ S.roundedEquations D) :
        ∃ i : Fin S.occurrences, e = S.equation i := by
    …

17. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.weightedValue line 101
18. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedValue line 104
19. theorem OAI.MaxCutGames.Reduction.WeightedSource.selectedSum_ofFn line 109
20. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.selectedMass_cast line 122
21. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedValue_bounds line 132
22. def OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundingDenominator line 174

    Source documentation

    ceil(4m/γ) computed from the exact numerator and denominator of γ.

    def roundingDenominator (γ : ℚ) : Nat :=
    …

23. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundingDenominator_positive line 177
24. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundingDenominator_budget line 182
25. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundingDenominator_size line 203
26. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.completeness_transport line 207
27. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.soundness_transport line 214
28. theorem OAI.MaxCutGames.Reduction.WeightedSource.RationalSource.roundedEquations_for_nonempty line 222
29. theorem OAI.MaxCutGames.Reduction.WeightedSource.e3lin_completeness line 230
30. theorem OAI.MaxCutGames.Reduction.WeightedSource.e3lin_soundness line 246
31. def OAI.MaxCutGames.Reduction.Preprocessing.rounded line 273
32. theorem OAI.MaxCutGames.Reduction.Preprocessing.rounded_failure_add_value line 278
33. theorem OAI.MaxCutGames.Reduction.Preprocessing.rounded_complete line 288
34. theorem OAI.MaxCutGames.Reduction.Preprocessing.rounded_sound line 300
35. def OAI.MaxCutGames.Reduction.Preprocessing.uniformSource line 313
36. theorem OAI.MaxCutGames.Reduction.Preprocessing.cloned_failure_eq line 316
37. theorem OAI.MaxCutGames.Reduction.Preprocessing.uniformSource_complete line 336
38. theorem OAI.MaxCutGames.Reduction.Preprocessing.uniformSource_distinct line 348
39. theorem OAI.MaxCutGames.Reduction.Preprocessing.uniformSource_sound line 352
40. theorem OAI.MaxCutGames.Reduction.OuterCompleteness.weighted_completeAt line 388

    Source documentation

    Completeness for the actual output after rounding and finite cloning.

    theorem weighted_completeAt {n s d : Nat}
        (W : RationalSource (CloneGap.Equation (Fin n))) (γ ξ : ℚ)
        (hγ : 0 < γ) (hξ : ξ ≤ γ / 4) (k : Nat) (g : SplitGadget s d)
        (error : RationalError)
        (hsource : ∃ A : Fin n → Bool,
          1 - ξ ≤ W.weightedValue (fun e => CloneGap.satisfied e A))
        (hbudget : (k : ℚ) * γ + g.stabilityError / 2 ≤ GapSemantics.errorValue error) :
        CompleteAt error
          (ActualGame.outputInstance (Preprocessing.uniformSource W γ hγ) k g) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.CloneGap.satisfied, OAI.MaxCutGames.Reduction.ActualGame.outputInstance, OAI.MaxCutGames.Reduction.Preprocessing.uniformSource

41. def OAI.MaxCutGames.Reduction.OuterCompleteness.sourceError line 402
42. theorem OAI.MaxCutGames.Reduction.OuterCompleteness.sourceError_pos line 405
43. theorem OAI.MaxCutGames.Reduction.OuterCompleteness.weighted_completeAt_of_parameters line 410
44. theorem OAI.MaxCutGames.Reduction.OuterCompleteness.weighted_explicit_completeAt_of_parameters line 431
45. def OAI.MaxCutGames.Reduction.UniformReduction.rawSource line 456
46. def OAI.MaxCutGames.Reduction.UniformReduction.source line 459
47. def OAI.MaxCutGames.Reduction.UniformReduction.output line 464

    Source documentation

    All proof-only numerical parameters and the correcting function are absent from the runtime input of this map.

    def output (es : List (CloneGap.Equation (Fin n))) (hne : es ≠ [])
        (k : Nat) (T : NoiseTables.Table s d) : Instance (2 ^ s) :=
    …

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation

48. def OAI.MaxCutGames.Reduction.UniformReduction.satisfaction line 468
49. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_variables line 471
50. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_occurrences line 474
51. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_occurrences_le line 478
52. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_distinct line 486
53. theorem OAI.MaxCutGames.Reduction.UniformReduction.output_constraint_count line 489
54. theorem OAI.MaxCutGames.Reduction.UniformReduction.output_vertex_count line 499
55. def OAI.MaxCutGames.Reduction.UniformReduction.liftAssignment line 504
56. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_failure_preserved line 508
57. theorem OAI.MaxCutGames.Reduction.UniformReduction.raw_failure_add_satisfaction line 513
58. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_complete line 522
59. theorem OAI.MaxCutGames.Reduction.UniformReduction.raw_quarter_count_gap line 533

    Source documentation

    The original uniform ((1+ξ)/2) satisfaction bound supplies exactly the quarter-gap premise needed by the cloning theorem.

    theorem raw_quarter_count_gap (es : List (CloneGap.Equation (Fin n))) (hne : es ≠ [])
        (ξ : ℚ) (hξ : ξ ≤ 1 / 2)
        (hsource : ∀ A : Fin n → Bool, satisfaction es A ≤ (1 + ξ) / 2) :
        ∀ A : Fin (rawSource es hne).«variables» → Bool,
          (rawSource es hne).sourceList.length ≤
            4 * (rawSource es hne).sourceList.countP (fun e => !CloneGap.satisfied e A) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.UniformReduction.satisfaction, OAI.MaxCutGames.Reduction.UniformReduction.rawSource, OAI.MaxCutGames.Reduction.CloneGap.satisfied

60. theorem OAI.MaxCutGames.Reduction.UniformReduction.source_sound line 545
61. theorem OAI.MaxCutGames.Reduction.UniformReduction.sourceGame_sound line 565
62. theorem OAI.MaxCutGames.Reduction.UniformReduction.completeAt_of_parameters line 580
63. theorem OAI.MaxCutGames.Reduction.OutputTranslations.translationTable_vector line 610

    Source documentation

    A forward table translates every binary vector by the same offset sum.

    theorem translationTable_vector {s : Nat} (a b x : Vector s) :
        (Encoding.translationTable a b).images[Encoding.alphabetEquiv s x] =
          Encoding.alphabetEquiv s (x + (a + b)) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.Encoding.translationTable, OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv

64. theorem OAI.MaxCutGames.Reduction.OutputTranslations.translationTable_coordinates line 616

    Source documentation

    The same law on every numbered alphabet label, in fixed vector coordinates.

    theorem translationTable_coordinates {s : Nat} (a b : Vector s) (label : Fin (2^s)) :
        (Encoding.alphabetEquiv s).symm ((Encoding.translationTable a b).images[label]) =
          (Encoding.alphabetEquiv s).symm label + (a + b) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv, OAI.MaxCutGames.Reduction.Encoding.translationTable

65. theorem OAI.MaxCutGames.Reduction.OutputTranslations.explicitEdge_vector line 625

    Source documentation

    Every actual explicit edge has a concrete translation vector.

    theorem explicitEdge_vector (S : Source) (k : Nat) {s d : Nat}
        (g : SplitGadget s d) (ω : ActualGame.Outcome S k g) :
        ∃ shift : Vector s, ∀ x : Vector s,
          (ActualGame.explicitEdge S k g ω).permutation.images[Encoding.alphabetEquiv s x] =
            Encoding.alphabetEquiv s (x + shift) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.Outcome, OAI.MaxCutGames.Reduction.ActualGame.explicitEdge, OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv

66. theorem OAI.MaxCutGames.Reduction.OutputTranslations.explicitEdge_coordinates line 635
67. theorem OAI.MaxCutGames.Reduction.OutputTranslations.outputInstanceWithEnumeration_vector line 648

    Source documentation

    All emitted occurrences, including parallel edges and repeated noise values, use translations in the same alphabet coordinates.

    theorem outputInstanceWithEnumeration_vector (S : Source) (k : Nat) {s d : Nat}
        (g : SplitGadget s d) (en : NoiseEnumeration g) :
        ∀ constraint ∈ (ActualGame.outputInstanceWithEnumeration S k g en).constraints,
          ∃ shift : Vector s, ∀ x : Vector s,
            constraint.permutation.images[Encoding.alphabetEquiv s x] =
              Encoding.alphabetEquiv s (x + shift) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.outputInstanceWithEnumeration, OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv

68. theorem OAI.MaxCutGames.Reduction.OutputTranslations.outputInstanceWithEnumeration_coordinates line 658
69. theorem OAI.MaxCutGames.Reduction.OutputTranslations.tableOutput_vector line 669

    Source documentation

    Erasing the correcting-map witness leaves the translation promise intact.

    theorem tableOutput_vector (S : Source) (k : Nat) {s d : Nat}
        (T : Integration.NoiseTables.Table s d) :
        ∀ constraint ∈ (Integration.TableReduction.output S k T).constraints,
          ∃ shift : Vector s, ∀ x : Vector s,
            constraint.permutation.images[Encoding.alphabetEquiv s x] =
              Encoding.alphabetEquiv s (x + shift) :=
    …

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Integration.TableReduction.output, OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv

70. theorem OAI.MaxCutGames.Reduction.OutputTranslations.tableOutput_coordinates line 678
71. theorem OAI.MaxCutGames.Reduction.OutputTranslations.uniformOutput_vector line 687
72. theorem OAI.MaxCutGames.Reduction.OutputTranslations.uniformOutput_coordinates line 696