BaseConstruction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite base gadget with arbitrarily small nonlinear change

The harmonic rank and genericity error are chosen first. A single finite field then supplies all required genericity statements, and the actual recursion is run to its harmonic depth. The kernel quotient injects the logical alphabet. Every linear map injective there detects at least one quarter of the noise.

theorem OAI.UniqueGamesTheorem.Gadget.BaseConstruction.theta_le_one line 38
theorem OAI.UniqueGamesTheorem.Gadget.BaseConstruction.rate_eq_one_sub_theta line 44

theorem OAI.UniqueGamesTheorem.Gadget.BaseConstruction.quotient_detection line 49

Source documentation

Detection for the actual quotient, with every whole-recursion estimate discharged by the adaptive harmonic argument.

theorem quotient_detection
    (r₀ : ℕ) (ε : ℚ) (hr₀ : 0 < r₀)
    (hbudget : badRankCoefficient r₀ * ε ≤ 1)
    (hgeneric : ∀ r : ℕ, r ≤ r₀ → nongenericFraction F r ≤ ε)
    (S₀ : Submodule (ZMod 2) (Vec F))
    (hrank : Module.finrank (ZMod 2) S₀ = r₀) (hS₀ : IsGeneric S₀)
    {E : Type} [AddCommGroup E] [Module (ZMod 2) E]
    (T : (quotientStage (F := F) (depth r₀ (fieldLineTheta F))).Input →ₗ[ZMod 2] E)
…

theorem OAI.UniqueGamesTheorem.Gadget.BaseConstruction.quotient_error_le line 84
Source documentation
The exact nonlinear recurrence satisfies the scalar budget fixed before the field was selected.
```
theorem quotient_error_le (p : ℚ) (r₀ : ℕ)
    (hgeom : (1 - fieldLineTheta F) ^ depth r₀ (fieldLineTheta F) ≤ p) :
    StageNoiseRecurrence.error
      (quotientStage (F := F) (depth r₀ (fieldLineTheta F))) ≤ p := by
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error
theorem OAI.UniqueGamesTheorem.Gadget.BaseConstruction.exists_base line 97
Source documentation
The unconditional finite base endpoint. All choices depend only on p; the larger logical alphabet used by the final enlargement is absent here.
```
theorem exists_base (p : ℚ) (hp : 0 < p) :
    ∃ d : ℕ, 0 < d ∧ ∃ n : ℕ,
      StageNoiseRecurrence.error (quotientStage (F := BinaryField d) n) ≤ p ∧
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error