AdaptivePathsLemmas.lean`

67 declarations, 0 contain sorry, 0 declared as axioms

From full character lifts to linear-map detection

If a target linear map is injective on the logical alphabet, a linear left inverse of that restriction turns all logical characters into a full lift. Detection by this lift implies that the target map does not annihilate the noise. The left inverse is proved to exist by the vector-space splitting theorem; it is not an additional premise.

def OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.Path line 25
Source documentation
A finite sequence represented as successive products, in reveal order.
```
def Path (C : Type u) : ℕ → Type u
  | 0 => PUnit
  | n + 1 => Path C n × C

variable {C : Type*}
```
instance OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.pathFintype line 31
instance OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.pathNonempty line 36

def OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.run line 42

Source documentation

A deterministic state update applied to the revealed choices.

def run {S : Type*} (step : S → C → S) (s₀ : S) : (n : ℕ) → Path C n → S
  | 0, _ => s₀
  | n + 1, (p, c) => step (run step s₀ n p) c

variable [Fintype C] [Nonempty C]

omit [Nonempty C] in

Mentions: OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.Path

theorem OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.average_run_succ line 49
theorem OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.probability_bad_succ line 57

theorem OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.expected_drop_le line 71

Source documentation

No measurability or independence premise about the state's lift is needed: the finite product itself supplies the conditioning identity.

theorem expected_drop_le {S : Type*} (step : S → C → S) (s₀ : S)
    (potential : S → ℚ) (bad : S → Prop) [DecidablePred bad]
    (A θ ε : ℚ) (hA : 0 ≤ A) (hθ : 0 ≤ θ) (hε : 0 ≤ ε)
    (hsmall : A * ε ≤ 1) (hinitial : ¬ bad s₀)
    (hfresh : ∀ s, probability (fun c => bad (step s c)) ≤ ε)
    (hstep : ∀ s, average (fun c => potential s - potential (step s c)) ≤
      3 * θ + A * θ * if bad s then 1 else 0) (n : ℕ) :
    average (fun p : Path C n => potential (run step s₀ n p)) -
      average (fun p : Path C (n + 1) => potential (run step s₀ (n + 1) p)) ≤
      4 * θ := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.Path, OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.run

theorem OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.expected_total_drop_le line 99

Source documentation

Harmonic loss bound on the actual adaptive path sample space.

theorem expected_total_drop_le {S : Type*} (step : S → C → S) (s₀ : S)
    (potential : S → ℚ) (bad : S → Prop) [DecidablePred bad]
    (A θ ε : ℚ) (hA : 0 ≤ A) (hθ : 0 ≤ θ) (hε : 0 ≤ ε)
    (hsmall : A * ε ≤ 1) (hinitial : ¬ bad s₀)
    (hfresh : ∀ s, probability (fun c => bad (step s c)) ≤ ε)
    (hstep : ∀ s, average (fun c => potential s - potential (step s c)) ≤
      3 * θ + A * θ * if bad s then 1 else 0) (n : ℕ) :
    potential s₀ - average (fun p : Path C n => potential (run step s₀ n p)) ≤
      4 * n * θ := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.Path, OAI.UniqueGamesTheorem.Gadget.AdaptivePaths.run

def OAI.UniqueGamesTheorem.Gadget.DetectionBridge.IsFullLift line 141
Source documentation
Every logical character is extended to the ambient input space.
```
def IsFullLift (ι : B →ₗ[K] V)
    (ψ : Module.Dual K B →ₗ[K] Module.Dual K V) : Prop :=
…
```
def OAI.UniqueGamesTheorem.Gadget.DetectionBridge.characterDetection line 147
Source documentation
Detection by any member of a character family. Classical decidability only selects an event indicator on the finite noise sample space.
```
noncomputable def characterDetection (noise : Ω → V)
    (ψ : Module.Dual K B →ₗ[K] Module.Dual K V) : ℚ := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.DetectionBridge.exists_leftInverse_of_logical_injective line 152
theorem OAI.UniqueGamesTheorem.Gadget.DetectionBridge.fullLift_of_leftInverse line 158
Source documentation
The left inverse supplies an actual full character lift through T.
```
theorem fullLift_of_leftInverse (ι : B →ₗ[K] V) (T : V →ₗ[K] E)
    (l : E →ₗ[K] B) (hleft : l.comp (T.comp ι) = LinearMap.id) :
    IsFullLift ι (l.comp T).dualMap := by
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.DetectionBridge.IsFullLift

theorem OAI.UniqueGamesTheorem.Gadget.DetectionBridge.target_detection_of_full_lift_bound line 168

Source documentation

A full-lift detection guarantee transfers to every target map injective on the logical alphabet.

theorem target_detection_of_full_lift_bound [DecidableEq E]
    (noise : Ω → V) (ι : B →ₗ[K] V) (T : V →ₗ[K] E) (q : ℚ)
    (hfull : ∀ ψ : Module.Dual K B →ₗ[K] Module.Dual K V,
      IsFullLift ι ψ → q ≤ characterDetection noise ψ)
    (hinjective : Function.Injective (T.comp ι)) :
    q ≤ probability (fun ω => T (noise ω) ≠ 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.DetectionBridge.IsFullLift, OAI.UniqueGamesTheorem.Gadget.DetectionBridge.characterDetection

theorem OAI.UniqueGamesTheorem.Gadget.DetectionBridge.target_detection_of_retraction_bound line 189

Source documentation

Equivalent useful interface when the recursive calculation already gives detection of every vector-valued linear retraction of the logical inclusion.

theorem target_detection_of_retraction_bound [DecidableEq B] [DecidableEq E]
    (noise : Ω → V) (ι : B →ₗ[K] V) (T : V →ₗ[K] E) (q : ℚ)
    (hretract : ∀ L : V →ₗ[K] B, L.comp ι = LinearMap.id →
      q ≤ probability (fun ω => L (noise ω) ≠ 0))
    (hinjective : Function.Injective (T.comp ι)) :
    q ≤ probability (fun ω => T (noise ω) ≠ 0) := by
…

theorem OAI.UniqueGamesTheorem.Gadget.family_factors_of_ker line 234
Source documentation
A linear family vanishing on the kernel of a surjection factors as one linear family on the target. In particular the factor is linear in its character parameter, rather than a separate arbitrary choice for each one.
```
theorem family_factors_of_ker
    (f : T →ₗ[k] X) (hf : Function.Surjective f)
    (ψ : S →ₗ[k] (T →ₗ[k] k))
    (hker : ∀ z t, f t = 0 → ψ z t = 0) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k), ∀ z t, ψ z t = γ z (f t) := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.common_parent_factorization line 255
Source documentation
The common first-coordinate character of a parent lift. ψ z is the parent character on child shifts, ζ z its prescribed logical character, and (a,b) the aggregate. A parent shift is exactly a tuple with a=0. The conclusion quantifies one γ before all tuples and all later children.
```
theorem common_parent_factorization
    (a : T →ₗ[k] X) (b : T →ₗ[k] B) (ha : Function.Surjective a)
    (ψ : S →ₗ[k] (T →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z t, a t = 0 → ψ z t = ζ z (b t)) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k),
      ∀ z t, ψ z t = γ z (a t) + ζ z (b t) := by
…
```

theorem OAI.UniqueGamesTheorem.Gadget.common_child_factorization line 277

Source documentation

Evaluating the single parent factor on any child embedding gives the child restriction formula. The same γ works for every child, so its choice cannot depend on the fresh orientation subsequently sampled at that child.

theorem common_child_factorization
    {ι P : Type*} [AddCommGroup P] [Module k P]
    (a : T →ₗ[k] X) (b : T →ₗ[k] B) (ha : Function.Surjective a)
    (ψ : S →ₗ[k] (T →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z t, a t = 0 → ψ z t = ζ z (b t))
    (child : ι → P →ₗ[k] T) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k),
      ∀ i z p, ψ z (child i p) = γ z (a (child i p)) + ζ z (b (child i p)) := by
…

theorem OAI.UniqueGamesTheorem.Gadget.aggregate_fst_surjective line 289

Source documentation

For a surjective aggregate, its first coordinate is surjective.

theorem aggregate_fst_surjective (A : T →ₗ[k] X × B)
    (hA : Function.Surjective A) :
    Function.Surjective ((LinearMap.fst k X B).comp A) := by
…

def OAI.UniqueGamesTheorem.Gadget.tupleEmbed line 324
Source documentation
Inclusion of all child shifts before imposing the parent kernel condition.
```
def tupleEmbed (e : R →ₗ[k] P) : (I → R) →ₗ[k] (I → P) where
…
```
theorem OAI.UniqueGamesTheorem.Gadget.tupleEmbed_single line 330
theorem OAI.UniqueGamesTheorem.Gadget.shiftAggregate_single line 337

theorem OAI.UniqueGamesTheorem.Gadget.parent_lift_common_child line 346

Source documentation

Actual parent lifts factor through the same aggregate first-coordinate family on all child shifts. The existential γ occurs before both i and h. This is the common-parent requirement used before revealing fresh orientation.

theorem parent_lift_common_child
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (ψ : S →ₗ[k] ((I → P) →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z (h : parentShifts J lam),
      ψ z (parentEmbed J lam e h) = ζ z (parentLogical J lam h)) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k), ∀ i z h,
      ψ z (Pi.single i (e h)) =
        γ z (J i (lam h)).1 + ζ z (J i (lam h)).2 := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.parentShifts, OAI.UniqueGamesTheorem.Gadget.parentEmbed, OAI.UniqueGamesTheorem.Gadget.parentLogical

theorem OAI.UniqueGamesTheorem.Gadget.parent_lift_child_kernel line 375

Source documentation

In particular, every child restriction annihilates the child's logical kernel. This proves that a child logical character exists for every lift.

theorem parent_lift_child_kernel
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (ψ : S →ₗ[k] ((I → P) →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z (h : parentShifts J lam),
      ψ z (parentEmbed J lam e h) = ζ z (parentLogical J lam h))
    (i : I) (z : S) (h : R) (hh : lam h = 0) :
    ψ z (Pi.single i (e h)) = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.parentShifts, OAI.UniqueGamesTheorem.Gadget.parentEmbed, OAI.UniqueGamesTheorem.Gadget.parentLogical

theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.card_binary_space line 411
Source documentation
A finite-dimensional binary vector space has 2^dimension vectors.
```
theorem card_binary_space : Nat.card V = 2 ^ Module.finrank (ZMod 2) V := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.kernel_card_mul_pow_rank line 416
Source documentation
Exact cross-multiplied uniform kernel probability: |ker f| * 2^rank f = |V|.
```
theorem kernel_card_mul_pow_rank (f : V →ₗ[ZMod 2] P) :
    Nat.card f.ker * 2 ^ Module.finrank (ZMod 2) f.range = Nat.card V := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.card_source_pos line 424
Source documentation
The denominator of the uniform vector experiment is positive.
```
theorem card_source_pos : 0 < Nat.card V := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.kernel_card_eq_pow_sub_rank line 429
Source documentation
The kernel size itself is the familiar power of the nullity.
```
theorem kernel_card_eq_pow_sub_rank (f : V →ₗ[ZMod 2] P) :
    Nat.card f.ker =
      2 ^ (Module.finrank (ZMod 2) V - Module.finrank (ZMod 2) f.range) := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.zero_event_card_mul_pow_rank line 438
Source documentation
The kernel formula expressed directly as the cardinality of the zero event.
```
theorem zero_event_card_mul_pow_rank (f : V →ₗ[ZMod 2] P) :
    Nat.card {x : V // f x = 0} * 2 ^ Module.finrank (ZMod 2) f.range = Nat.card V :=
…
```
theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.zero_event_card_mul_pow_le line 443
Source documentation
A rank threshold gives the exact cleared-denominator bound used on a good leaf.
```
theorem zero_event_card_mul_pow_le (f : V →ₗ[ZMod 2] P) (r : Nat)
    (hr : r ≤ Module.finrank (ZMod 2) f.range) :
    Nat.card {x : V // f x = 0} * 2 ^ r ≤ Nat.card V := by
…
```

theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_rank line 453

Source documentation

The same exact probability identity for a direct count over a finite universe.

theorem zero_event_finset_count_mul_pow_rank [Fintype V] [DecidableEq P]
    (f : V →ₗ[ZMod 2] P) :
    (Finset.univ.filter (fun x : V => f x = 0)).card *
      2 ^ Module.finrank (ZMod 2) f.range = Fintype.card V := by
…

theorem OAI.UniqueGamesTheorem.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_le line 461

Source documentation

A rank-r lower bound yields a 2⁻ʳ bound on the actual finite zero-event count.

theorem zero_event_finset_count_mul_pow_le [Fintype V] [DecidableEq P]
    (f : V →ₗ[ZMod 2] P) (r : Nat)
    (hr : r ≤ Module.finrank (ZMod 2) f.range) :
    (Finset.univ.filter (fun x : V => f x = 0)).card * 2 ^ r ≤ Fintype.card V := by
…

theorem OAI.UniqueGamesTheorem.Gadget.Orientation.sum_action_eq line 497
Source documentation
Right translation of the uniform group element changes the starting point, but leaves the complete sample sum unchanged.
```
theorem sum_action_eq (x y : X) (h : ∃ a : G, a • x = y) (f : X → ℚ) :
    (∑ g : G, f (g • x)) = ∑ g : G, f (g • y) := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.card_mul_sum_action line 505
Source documentation
Cross-multiplied uniform-pushforward identity for a transitive finite action. This form also handles empty event sets without additional cases.
```
theorem card_mul_sum_action (x : X)
    (transitive : ∀ y : X, ∃ a : G, a • x = y) (f : X → ℚ) :
    (Fintype.card X : ℚ) * (∑ g : G, f (g • x)) =
      (Fintype.card G : ℚ) * (∑ y : X, f y) := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.mean_action line 525
Source documentation
A uniform group element sends a fixed point to the uniform distribution on the entire transitive space. Apply to indicator functions for event bounds.
```
theorem mean_action (x : X)
    (transitive : ∀ y : X, ∃ a : G, a • x = y) (f : X → ℚ) :
    (∑ g : G, f (g • x)) / Fintype.card G =
      (∑ y : X, f y) / Fintype.card X := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.exists_map_eq_of_finrank_eq line 545
Source documentation
Every two equal-dimensional subspaces are related by an automorphism of the ambient space. This supplies actual transitivity, rather than assuming the desired distribution on the Grassmannian.
```
theorem exists_map_eq_of_finrank_eq (E F : Submodule K V)
    (h : finrank K E = finrank K F) :
    ∃ a : V ≃ₗ[K] V, E.map a.toLinearMap = F := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.rank_map line 562
Source documentation
Rank does not depend on the fresh orientation.
```
theorem rank_map (E : Submodule K V) (a : V ≃ₗ[K] V) :
    finrank K (E.map a.toLinearMap) = finrank K E :=
…
```
def OAI.UniqueGamesTheorem.Gadget.Orientation.RankSpace line 567
Source documentation
The finite Grassmannian at a rank chosen before orientation.
```
def RankSpace (K V : Type*) [Field K] [AddCommGroup V] [Module K V] (r : ℕ) :=
…
```
instance OAI.UniqueGamesTheorem.Gadget.Orientation.rankSpaceAction line 570
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.rankSpace_transitive line 580
Source documentation
Equal-rank transitivity specialized to the rank-indexed sampling space.
```
theorem rankSpace_transitive {r : ℕ} (E F : RankSpace K V r) :
    ∃ a : V ≃ₗ[K] V, a • E = F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.Orientation.RankSpace

theorem OAI.UniqueGamesTheorem.Gadget.Orientation.mean_oriented_subspace line 588

Source documentation

The exact uniform law of a fixed-rank subspace under a fresh uniform linear orientation, with no genericity or independence premise.

theorem mean_oriented_subspace {r : ℕ} [Fintype (V ≃ₗ[K] V)]
    [Fintype (RankSpace K V r)] (E : RankSpace K V r) (f : RankSpace K V r → ℚ) :
    (∑ a : V ≃ₗ[K] V, f (a • E)) / Fintype.card (V ≃ₗ[K] V) =
      (∑ F : RankSpace K V r, f F) / Fintype.card (RankSpace K V r) :=
…

Mentions: OAI.UniqueGamesTheorem.Gadget.Orientation.RankSpace

theorem OAI.UniqueGamesTheorem.Gadget.Orientation.rank_dual_pullback line 599
Source documentation
Pullback of a fixed character space by an isomorphism preserves rank. The character space is an argument preceding the newly chosen orientation.
```
theorem rank_dual_pullback (E : Submodule K (Module.Dual K U)) (J : B ≃ₗ[K] U) :
    finrank K (E.map J.dualMap.toLinearMap) = finrank K E :=
…
```
def OAI.UniqueGamesTheorem.Gadget.Orientation.orientationEquiv line 605
Source documentation
Choosing a reference isomorphism identifies all orientations with the automorphism group of the target.
```
def orientationEquiv (J₀ : B ≃ₗ[K] U) : (B ≃ₗ[K] U) ≃ (U ≃ₗ[K] U) where
…
```

theorem OAI.UniqueGamesTheorem.Gadget.Orientation.mean_map_equiv line 613

Source documentation

Uniform orientations between two spaces send a fixed character subspace to the uniform distribution on all subspaces of the same dimension.

theorem mean_map_equiv [FiniteDimensional K U] (E : Submodule K B) (J₀ : B ≃ₗ[K] U)
    [Fintype (B ≃ₗ[K] U)] [Fintype (U ≃ₗ[K] U)]
    [Fintype (RankSpace K U (finrank K E))]
    (f : RankSpace K U (finrank K E) → ℚ) :
    (∑ J : B ≃ₗ[K] U, f ⟨E.map J.toLinearMap, J.finrank_map_eq E⟩) /
        Fintype.card (B ≃ₗ[K] U) =
      (∑ F : RankSpace K U (finrank K E), f F) /
        Fintype.card (RankSpace K U (finrank K E)) := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.Orientation.RankSpace

def OAI.UniqueGamesTheorem.Gadget.Orientation.dualOrientationEquiv line 640
Source documentation
Dualization is a bijection on finite-dimensional isomorphisms. This connects uniform primal orientations to uniform character-space orientations.
```
def dualOrientationEquiv [FiniteDimensional K B] [FiniteDimensional K U] :
    (B ≃ₗ[K] U) ≃ (Module.Dual K U ≃ₗ[K] Module.Dual K B) where
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Orientation.mean_dual_pullback line 653
theorem OAI.UniqueGamesTheorem.Gadget.OrientationVectors.exists_equiv_map_nonzero line 699
Source documentation
Extend the isomorphism taking one specified nonzero vector to another.
```
theorem exists_equiv_map_nonzero (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ e : V ≃ₗ[K] V, e x = y := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.OrientationVectors.equiv_apply_ne_zero line 709
instance OAI.UniqueGamesTheorem.Gadget.OrientationVectors.nonzeroAction line 716
theorem OAI.UniqueGamesTheorem.Gadget.OrientationVectors.nonzero_transitive line 721

theorem OAI.UniqueGamesTheorem.Gadget.OrientationVectors.mean_oriented_nonzero line 728

Source documentation

A uniform ambient automorphism sends a fixed nonzero symbol uniformly onto all nonzero symbols.

theorem mean_oriented_nonzero [Fintype (V ≃ₗ[K] V)]
    [Fintype {x : V // x ≠ 0}] (x : {v : V // v ≠ 0})
    (f : {v : V // v ≠ 0} → ℚ) :
    (∑ a : V ≃ₗ[K] V, f (a • x)) / Fintype.card (V ≃ₗ[K] V) =
      (∑ y : {v : V // v ≠ 0}, f y) / Fintype.card {v : V // v ≠ 0} :=
…

theorem OAI.UniqueGamesTheorem.Gadget.OrientationVectors.mean_iso_nonzero line 737

Source documentation

The exact law used after fixing a child line and its nonzero output difference: averaging over all J : B ≃ₗ[K] U is uniform on U \ {0}.

theorem mean_iso_nonzero {B U : Type*} [AddCommGroup B] [Module K B]
    [AddCommGroup U] [Module K U] (J₀ : B ≃ₗ[K] U)
    [Fintype (B ≃ₗ[K] U)] [Fintype (U ≃ₗ[K] U)]
    [Fintype {u : U // u ≠ 0}] (b : B) (hb : b ≠ 0)
    (f : {u : U // u ≠ 0} → ℚ) :
    (∑ J : B ≃ₗ[K] U, f ⟨J b, equiv_apply_ne_zero J hb⟩) /
        Fintype.card (B ≃ₗ[K] U) =
      (∑ u : {u : U // u ≠ 0}, f u) / Fintype.card {u : U // u ≠ 0} := by
…

Mentions: OAI.UniqueGamesTheorem.Gadget.OrientationVectors.equiv_apply_ne_zero

theorem OAI.UniqueGamesTheorem.Gadget.Parameters.harmonic_double line 771
Source documentation
Every block from n+1 through 2n adds at least one half.
```
theorem harmonic_double (n : ℕ) (hn : 0 < n) :
    harmonic n + 1 / 2 ≤ harmonic (2 * n) := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.harmonic_pow_two line 792
def OAI.UniqueGamesTheorem.Gadget.Parameters.rankFor line 802
Source documentation
Computable rank exceeding any prescribed rational harmonic level.
```
def rankFor (level : ℚ) : ℕ := 2 ^ ⌈2 * level⌉₊
```
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.rankFor_pos line 804
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.le_harmonic_rankFor line 808
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.harmonic_unbounded line 814
def OAI.UniqueGamesTheorem.Gadget.Parameters.genericityError line 819
Source documentation
Strictly positive genericity error meeting the harmonic bad-rank budget.
```
def genericityError (r₀ : ℕ) : ℚ := 1 / (2 * (badRankCoefficient r₀ + 1))
```
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.genericityError_pos line 821
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.genericityError_lt_one line 826
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.genericityError_budget line 832
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.geometric_reciprocal_bound line 841
Source documentation
The geometric decay has an elementary reciprocal upper bound.
```
theorem geometric_reciprocal_bound (θ : ℚ) (_hθ : 0 ≤ θ) (hθone : θ ≤ 1)
    (n : ℕ) : (1 - θ) ^ n * (1 + (n : ℚ) * θ) ≤ 1 := by
…
```
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.geometric_at_depth_le line 863
Source documentation
The chosen harmonic depth works uniformly for every subsequent 0 < θ ≤ 1. Thus the rank can be selected before the field/noise parameter.
```
theorem geometric_at_depth_le (p θ : ℚ) (r₀ : ℕ) (hp : 0 < p)
    (hθ : 0 < θ) (hθone : θ ≤ 1)
    (hlarge : 8 * (p⁻¹ + 1) ≤ harmonic r₀) :
    (1 - θ) ^ depth r₀ θ ≤ p := by
…
```
def OAI.UniqueGamesTheorem.Gadget.Parameters.initialRank line 881
Source documentation
Explicit threshold depending only on the requested nonlinear error.
```
def initialRank (p : ℚ) : ℕ := rankFor (8 * (p⁻¹ + 1))
```
Mentions: OAI.UniqueGamesTheorem.Gadget.Parameters.rankFor
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.initialRank_pos line 883
theorem OAI.UniqueGamesTheorem.Gadget.Parameters.initialRank_large line 885

theorem OAI.UniqueGamesTheorem.Gadget.Parameters.effective_parameters line 889

Source documentation

All scalar choices needed before the field dimension is selected.

theorem effective_parameters (p : ℚ) (hp : 0 < p) :
    ∃ r₀ : ℕ, ∃ ε : ℚ,
      0 < r₀ ∧ 0 < ε ∧ ε < 1 ∧ badRankCoefficient r₀ * ε ≤ 1 ∧
      ∀ θ : ℚ, 0 < θ → θ ≤ 1 → (1 - θ) ^ depth r₀ θ ≤ p := by
…