StageNoiseRecurrence.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-stage nonlinear noise law

This packages the one-level recurrence for the actual recursive Stage, solves it at every height, and proves that the ambient-kernel quotient preserves it. The averaged block kernel remains an explicit argument for later instantiation with the concrete quadratic family.

def OAI.MaxCutGames.Gadget.StageNoiseRecurrence.average line 19
theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.average_eq_expect line 23
def OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error line 34
Source documentation
Uniform finite input and the stage's actual uniform finite noise choices.
```
noncomputable def error (s : Stage k B) : ℚ := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage
theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error_eq_expect line 39
theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.base_error line 52
theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.next_error line 81
Source documentation
The exact one-level law for the actual stage constructor.
```
theorem next_error (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 →
      (𝔼 i, 𝔼 z : X × B,
        NonlinearRecurrence.change (fun p => p.2 + Q p.1) z (J i d)) = ρ)
    (s : Stage k B) : error (Stage.next J hJ Q s) = ρ * error s := by
…
```
Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.NonlinearRecurrence.change, OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error, OAI.MaxCutGames.Gadget.Stage.next

theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.iterate_error line 103

Source documentation

Solving the proved recurrence, with the actual height-zero probability.

theorem iterate_error (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 →
      (𝔼 i, 𝔼 z : X × B,
        NonlinearRecurrence.change (fun p => p.2 + Q p.1) z (J i d)) = ρ)
    (n : ℕ) : error (Stage.iterate J hJ Q n) =
      (1 - 1 / (Fintype.card B : ℚ)) * ρ ^ n := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.NonlinearRecurrence.change, OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error, OAI.MaxCutGames.Gadget.Stage.iterate

theorem OAI.MaxCutGames.Gadget.StageNoiseRecurrence.quotient_error line 118
Source documentation
The quotient uses the original noise choices and preserves their full uniform-input change probability.
```
theorem quotient_error (s : Stage k B) : error (StageQuotient.toStage s) = error s := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error, OAI.MaxCutGames.Gadget.StageQuotient.toStage
def OAI.MaxCutGames.Quadratic.basisCoord line 157
Source documentation
The three standard coordinate vectors of the quadratic block.
```
def basisCoord (i : Fin 3) : Vec F := Pi.single i 1
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.basisCoord_ne_zero line 159
theorem OAI.MaxCutGames.Quadratic.Q_smul_basisCoord line 164
theorem OAI.MaxCutGames.Quadratic.dot_smul_basisCoord_of_ne line 169
theorem OAI.MaxCutGames.Quadratic.basisCoord_decomposition line 175
Source documentation
The explicit coordinate decomposition, over the field rather than only over the binary scalars of the block spaces.
```
theorem basisCoord_decomposition (x : Vec F) :
    x = x 0 • basisCoord 0 + x 1 • basisCoord 1 + x 2 • basisCoord 2 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.basisCoord
theorem OAI.MaxCutGames.Quadratic.horizontal_mem_U_basisCoord line 182
theorem OAI.MaxCutGames.Quadratic.vertical_mem_U_basisCoord_of_ne line 188
def OAI.MaxCutGames.Quadratic.coordinateBlockSpan line 195
Source documentation
The binary span of the three coordinate block spaces.
```
def coordinateBlockSpan : Submodule (ZMod 2) (Vec F × Vec F) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.U_basisCoord_le_coordinateBlockSpan line 198
theorem OAI.MaxCutGames.Quadratic.horizontal_mem_coordinateBlockSpan line 205
theorem OAI.MaxCutGames.Quadratic.vertical_mem_coordinateBlockSpan line 210
theorem OAI.MaxCutGames.Quadratic.mem_coordinateBlockSpan line 224
Source documentation
Every pair is a sum of three horizontal and three vertical coordinate pairs, all already in the sum of the coordinate blocks.
```
theorem mem_coordinateBlockSpan (p : Vec F × Vec F) :
    p ∈ (coordinateBlockSpan : Submodule (ZMod 2) (Vec F × Vec F)) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.coordinateBlockSpan
theorem OAI.MaxCutGames.Quadratic.coordinateBlockSpan_eq_top line 242
theorem OAI.MaxCutGames.Quadratic.iSup_U_nonzero_eq_top line 250
Source documentation
The block spaces for all nonzero line generators span the whole ambient binary vector space. The proof uses just the three coordinate generators.
```
theorem iSup_U_nonzero_eq_top :
    (⨆ v : {v : Vec F // v ≠ 0}, U v.1) = ⊤ := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
def OAI.MaxCutGames.Quadratic.blockEmbedding line 276
def OAI.MaxCutGames.Quadratic.blockAggregate line 280
theorem OAI.MaxCutGames.Quadratic.blockAggregate_single line 283
theorem OAI.MaxCutGames.Quadratic.fieldLine_block_le_range_aggregate line 296
theorem OAI.MaxCutGames.Quadratic.blockAggregate_surjective line 311
Source documentation
All blocks occur in the actual pair-indexed aggregate. Their already proved span is the entire horizontal/vertical space, so the aggregate is surjective, as required by the recursive shift construction.
```
theorem blockAggregate_surjective : Function.Surjective (blockAggregate (F := F)) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.blockAggregate
theorem OAI.MaxCutGames.Quadratic.aggregate_blockEmbedding_surjective line 327
def OAI.MaxCutGames.Gadget.QuadraticStageNoise.rate line 355
theorem OAI.MaxCutGames.Gadget.QuadraticStageNoise.actual_kernel line 358
def OAI.MaxCutGames.Gadget.QuadraticStageNoise.stage line 366
Source documentation
The actual recursive spaces, shifts, outputs and finite leaf-noise sampler.
```
noncomputable def stage (n : ℕ) : Stage (ZMod 2) (Vec F) :=
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage
theorem OAI.MaxCutGames.Gadget.QuadraticStageNoise.stage_error line 369
def OAI.MaxCutGames.Gadget.QuadraticStageNoise.quotientStage line 378
Source documentation
The logical alphabet is an actual injected shift subspace after quotient.
```
noncomputable def quotientStage (n : ℕ) : Stage (ZMod 2) (Vec F) :=
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage
theorem OAI.MaxCutGames.Gadget.QuadraticStageNoise.quotientStage_error line 381
theorem OAI.MaxCutGames.Gadget.Parameters.harmonic_double line 395
Source documentation
Every block from n+1 through 2n adds at least one half.
```
theorem harmonic_double (n : ℕ) (hn : 0 < n) :
    MaxCutGames.Gadget.Harmonic.harmonic n + 1 / 2 ≤ MaxCutGames.Gadget.Harmonic.harmonic (2 * n) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.harmonic
theorem OAI.MaxCutGames.Gadget.Parameters.harmonic_pow_two line 416
def OAI.MaxCutGames.Gadget.Parameters.rankFor line 426
Source documentation
Computable rank exceeding any prescribed rational MaxCutGames.Gadget.Harmonic.harmonic level.
```
def rankFor (level : ℚ) : ℕ := 2 ^ ⌈2 * level⌉₊
```
theorem OAI.MaxCutGames.Gadget.Parameters.rankFor_pos line 428
theorem OAI.MaxCutGames.Gadget.Parameters.le_harmonic_rankFor line 432
theorem OAI.MaxCutGames.Gadget.Parameters.harmonic_unbounded line 438
def OAI.MaxCutGames.Gadget.Parameters.genericityError line 443
Source documentation
Strictly positive genericity error meeting the MaxCutGames.Gadget.Harmonic.harmonic bad-rank budget.
```
def genericityError (r₀ : ℕ) : ℚ := 1 / (2 * (badRankCoefficient r₀ + 1))
```
theorem OAI.MaxCutGames.Gadget.Parameters.genericityError_pos line 445
theorem OAI.MaxCutGames.Gadget.Parameters.genericityError_lt_one line 450
theorem OAI.MaxCutGames.Gadget.Parameters.genericityError_budget line 456
theorem OAI.MaxCutGames.Gadget.Parameters.geometric_reciprocal_bound line 465
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.MaxCutGames.Gadget.Parameters.geometric_at_depth_le line 487
Source documentation
The chosen MaxCutGames.Gadget.Harmonic.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) ≤ MaxCutGames.Gadget.Harmonic.harmonic r₀) :
    (1 - θ) ^ depth r₀ θ ≤ p := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.harmonic
def OAI.MaxCutGames.Gadget.Parameters.initialRank line 505
Source documentation
Explicit threshold depending only on the requested nonlinear error.
```
def initialRank (p : ℚ) : ℕ := rankFor (8 * (p⁻¹ + 1))
```
Mentions: OAI.MaxCutGames.Gadget.Parameters.rankFor
theorem OAI.MaxCutGames.Gadget.Parameters.initialRank_pos line 507
theorem OAI.MaxCutGames.Gadget.Parameters.initialRank_large line 509

theorem OAI.MaxCutGames.Gadget.Parameters.effective_parameters line 513

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
…