Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Arbitrarily small projection-game soundness with polynomial size

Lax253009.Amplification · concepts/Lax253009/Amplification.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A fixed sequence of tuple fortifications and tensor squarings reduces any constant symmetric soundness s in (0,1) below any prescribed positive δ. The sequence depends only on s, δ, and the fixed answer alphabets, and is chosen before the question spaces and the game.

    All transformations preserve perfect completeness and uniform question marginals. Explicit cardinality formulas show polynomial growth of the question spaces and constant answer alphabets for each fixed sequence. This provides the soundness amplification needed for the Håstad reduction.

    Concept map
    7 concepts; 2 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_small_value_scheme proven

    2 Scheme.card_centers proven

    3 Scheme.card_extensions proven

    4 Scheme.card_questions proven

    5 Scheme.size_polynomial proven

    6 Scheme.transform_complete proven

    7 Scheme.transform_uniform proven

    Lean source view on GitHub

    1import Lax253009.CenteredProjection
    2import Mathlib.Data.PNat.Basic
    3
    4/-!
    5---
    6title: Arbitrarily small projection-game soundness with polynomial size
    7type: theorem
    8---
    9A fixed sequence of tuple fortifications and tensor squarings reduces any
    10constant symmetric soundness s in (0,1) below any prescribed positive δ.
    11The sequence depends only on s, δ, and the fixed answer alphabets, and is
    12chosen before the question spaces and the game.
    13
    14All transformations preserve perfect completeness and uniform question
    15marginals. Explicit cardinality formulas show polynomial growth of the
    16question spaces and constant answer alphabets for each fixed sequence.
    17This provides the soundness amplification needed for the Håstad reduction.
    18-/
    19
    20namespace Lax253009.Amplification
    21
    22open CenteredProjection TupleFortification
    23open scoped BigOperators
    24
    25inductive Scheme where
    26 | base
    27 | step (t : ℕ+) (previous : Scheme)
    28
    29namespace Scheme
    30
    31def centers (S : Scheme) (U : Type) : Type := match S with
    32 | .base => U
    33 | .step _ S => centers S U × centers S U
    34
    35def questions (S : Scheme) (W : Type) : Type := match S with
    36 | .base => W
    37 | .step t S => (Fin t → questions S W) × (Fin t → questions S W)
    38
    39def extensions (S : Scheme) (Ω W : Type) : Type := match S with
    40 | .base => Ω
    41 | .step t S => (extensions S Ω W × History t (questions S W)) ×
    42 (extensions S Ω W × History t (questions S W))
    43
    44instance centersFintype {U : Type} [Fintype U] (S : Scheme) : Fintype (centers S U) :=
    45 match S with
    46 | .base => inferInstanceAs (Fintype U)
    47 | .step _ S =>
    48 letI : Fintype (centers S U) := centersFintype S
    49 inferInstanceAs (Fintype (centers S U × centers S U))
    50
    51instance questionsFintype {W : Type} [Fintype W] (S : Scheme) : Fintype (questions S W) :=
    52 match S with
    53 | .base => inferInstanceAs (Fintype W)
    54 | .step t S =>
    55 letI : Fintype (questions S W) := questionsFintype S
    56 inferInstanceAs (Fintype ((Fin t → questions S W) × (Fin t → questions S W)))
    57
    58instance extensionsFintype {Ω W : Type} [Fintype Ω] [Fintype W] (S : Scheme) :
    59 Fintype (extensions S Ω W) := match S with
    60 | .base => inferInstanceAs (Fintype Ω)
    61 | .step t S =>
    62 letI : Fintype (extensions S Ω W) := extensionsFintype S
    63 inferInstanceAs (Fintype ((extensions S Ω W × History t (questions S W)) ×
    64 (extensions S Ω W × History t (questions S W))))
    65
    66instance centersNonempty {U : Type} [Nonempty U] (S : Scheme) : Nonempty (centers S U) :=
    67 match S with
    68 | .base => inferInstanceAs (Nonempty U)
    69 | .step _ S =>
    70 letI : Nonempty (centers S U) := centersNonempty S
    71 inferInstanceAs (Nonempty (centers S U × centers S U))
    72
    73instance questionsNonempty {W : Type} [Nonempty W] (S : Scheme) : Nonempty (questions S W) :=
    74 match S with
    75 | .base => inferInstanceAs (Nonempty W)
    76 | .step t S =>
    77 letI : Nonempty (questions S W) := questionsNonempty S
    78 inferInstanceAs (Nonempty ((Fin t → questions S W) × (Fin t → questions S W)))
    79
    80instance extensionsNonempty {Ω W : Type} [Nonempty Ω] [Nonempty W] (S : Scheme) :
    81 Nonempty (extensions S Ω W) := match S with
    82 | .base => inferInstanceAs (Nonempty Ω)
    83 | .step t S =>
    84 letI : Nonempty (Fin t) := Fin.pos_iff_nonempty.mp t.pos
    85 letI : Nonempty (extensions S Ω W) := extensionsNonempty S
    86 inferInstanceAs (Nonempty ((extensions S Ω W × History t (questions S W)) ×
    87 (extensions S Ω W × History t (questions S W))))
    88
    89def transform {U Ω W X Y : Type} (S : Scheme) (G : System U Ω W X Y) :
    90 System (centers S U) (extensions S Ω W) (questions S W) (centers S X) (questions S Y) :=
    91 match S with
    92 | .base => G
    93 | .step t S => ((transform S G).fortify t).tensor
    94
    95def centerPower : Scheme → ℕ
    96 | .base => 1
    97 | .step _ S => S.centerPower * 2
    98
    99def questionPower : Scheme → ℕ
    100 | .base => 1
    101 | .step t S => S.questionPower * t * 2
    102
    103def extensionCoefficient : Scheme → ℕ
    104 | .base => 1
    105 | .step t S => (S.extensionCoefficient * t) ^ 2
    106
    107def extensionPower : Scheme → ℕ
    108 | .base => 0
    109 | .step t S => (S.extensionPower + S.questionPower * t) * 2
    110
    111axiom transform_complete {U Ω W X Y : Type} (S : Scheme) (G : System U Ω W X Y)
    112 (h : G.Complete) : (S.transform G).Complete
    113
    114axiom transform_uniform {U Ω W X Y : Type}
    115 [Fintype U] [Fintype Ω] [Fintype W] [Nonempty W]
    116 (S : Scheme) (G : System U Ω W X Y) (h : G.Uniform) : (S.transform G).Uniform
    117
    118axiom card_centers {U : Type} [Fintype U] (S : Scheme) :
    119 Fintype.card (S.centers U) = Fintype.card U ^ S.centerPower
    120
    121axiom card_questions {W : Type} [Fintype W] (S : Scheme) :
    122 Fintype.card (S.questions W) = Fintype.card W ^ S.questionPower
    123
    124axiom card_extensions {Ω W : Type} [Fintype Ω] [Fintype W] (S : Scheme) :
    125 Fintype.card (S.extensions Ω W) =
    126 S.extensionCoefficient * Fintype.card Ω ^ S.centerPower * Fintype.card W ^ S.extensionPower
    127
    128axiom size_polynomial {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W] (S : Scheme) :
    129 Fintype.card (S.centers U) + Fintype.card (S.extensions Ω W) + Fintype.card (S.questions W) ≤
    130 (S.extensionCoefficient + 2) * (Fintype.card U + Fintype.card Ω + Fintype.card W + 1) ^
    131 (S.centerPower + S.questionPower + S.extensionPower)
    132
    133end Scheme
    134
    135def SoundReduction (S : Scheme) (X Y : Type) [Fintype X] [Fintype Y] (s δ : ℝ) : Prop :=
    136 ∀ (U Ω W : Type) [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    137 [Fintype W] [Nonempty W] (G : System U Ω W X Y),
    138 G.Uniform → G.symmetrize.Sound s → (S.transform G).symmetrize.Sound δ
    139
    140axiom exists_small_value_scheme (X Y : Type) [Fintype X] [Nonempty X]
    141 [Fintype Y] [Nonempty Y] (s δ : ℝ) (hs : 0 < s) (hs1 : s < 1) (hδ : 0 < δ) :
    142 ∃ S : Scheme, SoundReduction S X Y s δ
    143
    144end Lax253009.Amplification
    145
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…