BlockRestriction.lean`

83 declarations, 0 contain sorry, 0 declared as axioms

Actual child restriction maps

A common-parent lift g gives a binary linear map from its logical character space into the dual of each quadratic block. Its kernel is literal character annihilation, so the trace calculation and the all-lifts genericity predicate apply directly to this map.

theorem OAI.MaxCutGames.Quadratic.dot_add_first_inline_BlockRestriction line 24
def OAI.MaxCutGames.Quadratic.blockCharacterLinear line 30
Source documentation
The actual trace character as a binary linear functional.
```
def blockCharacterLinear (g z : Vec F) :
    (Vec F × Vec F) →ₗ[ZMod 2] ZMod 2 where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.blockRestriction line 46
Source documentation
Restriction to one block, linear in the logical character z.
```
def blockRestriction (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) :
    S →ₗ[ZMod 2] ((U v) →ₗ[ZMod 2] ZMod 2) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.blockRestriction_apply line 67
theorem OAI.MaxCutGames.Quadratic.blockRestriction_eq_zero_iff line 73
Source documentation
Equality to zero is exactly annihilation of the underlying block.
```
theorem blockRestriction_eq_zero_iff (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) (z : S) :
    blockRestriction S g v z = 0 ↔ BlockAnnihilates (g z) z v := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.blockRestriction, OAI.MaxCutGames.Quadratic.BlockAnnihilates
theorem OAI.MaxCutGames.Quadratic.mem_ker_blockRestriction_iff line 84
Source documentation
The exact kernel formula for a nonzero logical character.
```
theorem mem_ker_blockRestriction_iff (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) {v : Vec F} (hv : v ≠ 0)
    {z : S} (hz : z ≠ 0) :
    z ∈ (blockRestriction S g v).ker ↔
      (z : Vec F) ∈ line v ∧
        dot (g z) z = squareRoot (z.val 0 * z.val 1 * z.val 2) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.blockRestriction, OAI.MaxCutGames.Quadratic.line, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.squareRoot
theorem OAI.MaxCutGames.Quadratic.blockRestriction_nonzero_kernel_unique line 95
Source documentation
Nonproportionality of a generic space makes every actual block kernel contain at most one nonzero character.
```
theorem blockRestriction_nonzero_kernel_unique
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    {v : Vec F} (hv : v ≠ 0) (hS : IsGeneric S)
    (z w : S) (hz : z ≠ 0) (hw : w ≠ 0)
    (hgz : blockRestriction S g v z = 0)
    (hgw : blockRestriction S g v w = 0) : z = w := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.blockRestriction
theorem OAI.MaxCutGames.Quadratic.finrank_ker_blockRestriction_le_one line 117
Source documentation
Every actual child restriction map loses at most one binary dimension.
```
theorem finrank_ker_blockRestriction_le_one
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    {v : Vec F} (hv : v ≠ 0) (hS : IsGeneric S) :
    Module.finrank (ZMod 2) (blockRestriction S g v).ker ≤ 1 :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.blockRestriction
theorem OAI.MaxCutGames.Quadratic.finrank_blockRestriction_source_le_range_add_one line 124
def OAI.MaxCutGames.Quadratic.orientedBlockRestriction line 146
Source documentation
The actual child restriction after a choice of block orientation.
```
def orientedBlockRestriction (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) (J : B ≃ₗ[ZMod 2] U v) :
    S →ₗ[ZMod 2] (B →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.orientedBlockRestriction_apply line 152
theorem OAI.MaxCutGames.Quadratic.orientedBlockRestriction_eq_zero_iff line 158
theorem OAI.MaxCutGames.Quadratic.ker_orientedBlockRestriction line 172
Source documentation
The kernel depends on the field line and common-parent lift, not on J.
```
theorem ker_orientedBlockRestriction
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (v : Vec F) (J : B ≃ₗ[ZMod 2] U v) :
    (orientedBlockRestriction S g v J).ker = (blockRestriction S g v).ker := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U, OAI.MaxCutGames.Quadratic.orientedBlockRestriction, OAI.MaxCutGames.Quadratic.blockRestriction
theorem OAI.MaxCutGames.Quadratic.ker_orientedBlockRestriction_independent line 180
theorem OAI.MaxCutGames.Quadratic.mem_ker_orientedBlockRestriction_iff line 187
theorem OAI.MaxCutGames.Quadratic.finrank_ker_orientedBlockRestriction_le_one line 197
abbrev OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual line 212
def OAI.MaxCutGames.Gadget.BlockDescent.traceSpace line 215
Source documentation
Coordinates of a binary character subspace under the trace pairing.
```
def traceSpace (S : Submodule (ZMod 2) (BinaryDual (F := F))) :
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
def OAI.MaxCutGames.Gadget.BlockDescent.traceSpaceEquiv line 218
theorem OAI.MaxCutGames.Gadget.BlockDescent.traceSpace_finrank line 224
theorem OAI.MaxCutGames.Gadget.BlockDescent.traceSpaceEquiv_apply_val line 229
theorem OAI.MaxCutGames.Gadget.BlockDescent.traceSpaceEquiv_symm_val line 234
def OAI.MaxCutGames.Gadget.BlockDescent.traceLift line 243
Source documentation
One binary-linear lift on the trace-coordinate domain, obtained from the single common parent map. It is fixed before the outgoing line/orientation.
```
def traceLift (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
theorem OAI.MaxCutGames.Gadget.BlockDescent.childCharacter_comp_traceSpaceEquiv line 248
Source documentation
Equality of actual child maps after a change of logical coordinates.
```
theorem childCharacter_comp_traceSpaceEquiv
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
theorem OAI.MaxCutGames.Gadget.BlockDescent.childCharacter_range_eq line 268
Source documentation
The child logical image is unchanged by the trace-coordinate domain isomorphism. This is equality of subspaces, not merely equality of ranks.
```
theorem childCharacter_range_eq
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
theorem OAI.MaxCutGames.Gadget.BlockDescent.childCharacter_range_eq_dual_pullback line 279
Source documentation
Before the orientation is revealed, the un-oriented image is fixed; the fresh isomorphism acts only by dual pullback on this fixed image.
```
theorem childCharacter_range_eq_dual_pullback
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
theorem OAI.MaxCutGames.Gadget.BlockDescent.childCharacter_rank_independent line 289
Source documentation
The rank is independent of the fresh orientation.
```
theorem childCharacter_rank_independent
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.MaxCutGames.Gadget.BlockDescent.BinaryDual
def OAI.MaxCutGames.Gadget.Descent.commonGamma line 311
theorem OAI.MaxCutGames.Gadget.Descent.commonGamma_spec line 317
def OAI.MaxCutGames.Gadget.Descent.childDomain line 323
def OAI.MaxCutGames.Gadget.Descent.childLift line 327
def OAI.MaxCutGames.Gadget.Descent.childSection line 333
theorem OAI.MaxCutGames.Gadget.Descent.childSection_rightInverse line 340
theorem OAI.MaxCutGames.Gadget.Descent.childLift_spec line 349
theorem OAI.MaxCutGames.Gadget.Descent.child_detection line 358
theorem OAI.MaxCutGames.Gadget.Descent.child_rank_le line 366

def OAI.MaxCutGames.Gadget.Descent.leafRank line 373

Source documentation

Terminal logical rank along the actual recursively sampled path. The final uniform symbol is ignored by this rank function.

noncomputable def leafRank
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J)) (Q : X → B) :
    (n : ℕ) → (S : Submodule k (B →ₗ[k] k)) →
    Lift (Stage.iterate J hJ Q n) S → (Stage.iterate J hJ Q n).Noise → ℕ
  | 0, S, _, _ => Module.finrank k S
  | n + 1, S, L, t => leafRank J hJ Q n
      (childDomain J hJ Q (Stage.iterate J hJ Q n) S L t.1)
      (childLift J hJ Q (Stage.iterate J hJ Q n) S L t.1) t.2

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.iterate, OAI.MaxCutGames.Gadget.Descent.childDomain, OAI.MaxCutGames.Gadget.Descent.childLift

theorem OAI.MaxCutGames.Gadget.Descent.leafRank_le line 382
def OAI.MaxCutGames.Quadratic.characterFieldLine line 410
Source documentation
A total projective-line map; the default is irrelevant on nonzero characters.
```
def characterFieldLine (A₀ : FieldLine F) (z : Vec F) : FieldLine F := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.characterFieldLine_eq_of_mem line 415
def OAI.MaxCutGames.Quadratic.fieldLineRestrictions line 424
Source documentation
All maps have the same binary dual codomain, despite their different blocks.
```
def fieldLineRestrictions (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A) :
    FieldLine F → S →ₗ[ZMod 2] (Vec F →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation
theorem OAI.MaxCutGames.Quadratic.alignedCharacters_eq_alignmentEvent line 430
Source documentation
The alignment event written with the displayed three-coordinate dot product.
```
theorem alignedCharacters_eq_alignmentEvent
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F) :
    alignedCharacters (fun z : S =>
      dot (g z) z = squareRoot (z.val 0 * z.val 1 * z.val 2)) =
      alignmentEvent (fun z : S => (z : Vec F)) g
        (fun z : S => alignmentRightHandSide (z : Vec F)) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.alignedCharacters, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.squareRoot, OAI.MaxCutGames.Quadratic.alignmentEvent, OAI.MaxCutGames.Quadratic.alignmentRightHandSide
theorem OAI.MaxCutGames.Quadratic.card_loss_fieldLineRestrictions_le line 443
Source documentation
The exact line-loss count, valid for every choice of orientations and every binary-linear lift, including one chosen adaptively from earlier information.
```
theorem card_loss_fieldLineRestrictions_le
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (J : ∀ A : FieldLine F, BlockOrientation A) (hS : IsGeneric S)
    (A₀ : FieldLine F) :
    (lossIndices (fieldLineRestrictions S g J)).card ≤
      3 * Module.finrank (ZMod 2) S := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.lossIndices, OAI.MaxCutGames.Quadratic.fieldLineRestrictions
theorem OAI.MaxCutGames.Quadratic.card_loss_fieldLineRestrictions_le_three_rank line 462
Source documentation
The fallback line is only used to totalize the counting map.
```
theorem card_loss_fieldLineRestrictions_le_three_rank
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (J : ∀ A : FieldLine F, BlockOrientation A) (hS : IsGeneric S) :
    (lossIndices (fieldLineRestrictions S g J)).card ≤
      3 * Module.finrank (ZMod 2) S := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.lossIndices, OAI.MaxCutGames.Quadratic.fieldLineRestrictions
def OAI.MaxCutGames.Gadget.Harmonic.harmonic line 482
Source documentation
The finite harmonic potential, by its exact rational recurrence.
```
def harmonic : ℕ → ℚ
  | 0 => 0
  | r + 1 => harmonic r + (↑(r + 1))⁻¹
```
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_zero line 486
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_succ line 488
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_eq_sum line 491
def OAI.MaxCutGames.Gadget.Harmonic.average line 498
Source documentation
Rational expectation under uniform sampling on a finite space.
```
def average (f : Ω → ℚ) : ℚ := Finset.univ.expect f
```
def OAI.MaxCutGames.Gadget.Harmonic.probability line 501
Source documentation
Probability of a decidable event in the finite experiment.
```
def probability (p : Ω → Prop) [DecidablePred p] : ℚ :=
…
```
theorem OAI.MaxCutGames.Gadget.Harmonic.average_mono line 504
theorem OAI.MaxCutGames.Gadget.Harmonic.average_nonneg line 508
theorem OAI.MaxCutGames.Gadget.Harmonic.average_const line 512
theorem OAI.MaxCutGames.Gadget.Harmonic.average_add line 516
theorem OAI.MaxCutGames.Gadget.Harmonic.average_sub line 520
theorem OAI.MaxCutGames.Gadget.Harmonic.average_mul_left line 524
theorem OAI.MaxCutGames.Gadget.Harmonic.probability_nonneg line 528
theorem OAI.MaxCutGames.Gadget.Harmonic.probability_le_one line 534
theorem OAI.MaxCutGames.Gadget.Harmonic.probability_mono line 543
theorem OAI.MaxCutGames.Gadget.Harmonic.probability_not line 552
theorem OAI.MaxCutGames.Gadget.Harmonic.probability_eq_half_of_swap line 564
Source documentation
A bijection swapping an event with its complement proves exact half probability. At a leaf the bijection is translation by a symbol on which a nonzero binary character is one.
```
theorem probability_eq_half_of_swap [Nonempty Ω]
    (p : Ω → Prop) [DecidablePred p] (e : Ω ≃ Ω)
    (hswap : ∀ ω, p (e ω) ↔ ¬ p ω) : probability p = 1 / 2 := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability
theorem OAI.MaxCutGames.Gadget.Harmonic.binary_character_detection_probability line 576
Source documentation
Every nonzero binary additive character detects precisely half of uniform symbols. The witness may depend on the previously sampled path.
```
theorem binary_character_detection_probability [AddGroup Ω]
    (χ : Ω →+ ZMod 2) (v : Ω) (hv : χ v ≠ 0) :
    probability (fun ω => χ ω ≠ 0) = 1 / 2 := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability
theorem OAI.MaxCutGames.Gadget.Harmonic.binary_family_detection_ge_half line 595
Source documentation
A surviving family contains a nonzero character, so its detection event contains an event of exact half probability.
```
theorem binary_family_detection_ge_half [AddGroup Ω]
    (detects : Ω → Prop) [DecidablePred detects]
    (χ : Ω →+ ZMod 2) (v : Ω) (hv : χ v ≠ 0)
    (hcontains : ∀ ω, χ ω ≠ 0 → detects ω) :
    (1 / 2 : ℚ) ≤ probability detects := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_nonneg line 603
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_mono line 608
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_pos line 616
theorem OAI.MaxCutGames.Gadget.Harmonic.harmonic_sub_predecessor line 621
theorem OAI.MaxCutGames.Gadget.Harmonic.generic_drop_identity line 628
Source documentation
A generic rank-r space loses either zero or one dimension. Its harmonic drop is exactly the loss indicator times 1/r.
```
theorem generic_drop_identity (r : ℕ) (next : Ω → ℕ) (hr : 0 < r)
    (hstep : ∀ ω, next ω = r ∨ next ω = r - 1) :
    average (fun ω => harmonic r - harmonic (next ω)) =
      (r : ℚ)⁻¹ * probability (fun ω => next ω < r) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.Harmonic.probability
theorem OAI.MaxCutGames.Gadget.Harmonic.generic_expected_drop_le line 644
Source documentation
The generic loss probability 3rθ becomes the rank-independent harmonic loss bound 3θ.
```
theorem generic_expected_drop_le (r : ℕ) (next : Ω → ℕ) (θ : ℚ)
    (hr : 0 < r) (hstep : ∀ ω, next ω = r ∨ next ω = r - 1)
    (hloss : probability (fun ω => next ω < r) ≤ 3 * r * θ) :
    average (fun ω => harmonic r - harmonic (next ω)) ≤ 3 * θ := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability, OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic
theorem OAI.MaxCutGames.Gadget.Harmonic.arbitrary_expected_drop_le line 658
Source documentation
Without genericity, charge the entire harmonic potential only on paths where some rank is lost.
```
theorem arbitrary_expected_drop_le (r : ℕ) (next : Ω → ℕ) (p : ℚ)
    (hstep : ∀ ω, next ω ≤ r)
    (hloss : probability (fun ω => next ω < r) ≤ p) :
    average (fun ω => harmonic r - harmonic (next ω)) ≤ harmonic r * p := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability, OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic

theorem OAI.MaxCutGames.Gadget.Harmonic.expected_drop_le_four_theta line 679

Source documentation

Averaging a conditional rank-loss estimate uses only a bound on the bad space's probability, even when the selected lift depends on that space.

theorem expected_drop_le_four_theta [Nonempty Ω]
    (drop : Ω → ℚ) (bad : Ω → Prop) [DecidablePred bad] (C θ ε : ℚ)
    (hC : 0 ≤ C) (hθ : 0 ≤ θ)
    (hconditional : ∀ ω, drop ω ≤ 3 * θ + C * θ * if bad ω then 1 else 0)
    (hbad : probability bad ≤ ε) (hsmall : C * ε ≤ 1) :
    average drop ≤ 4 * θ := by
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability, OAI.MaxCutGames.Gadget.Harmonic.average

def OAI.MaxCutGames.Gadget.Harmonic.badRankCoefficient line 696
theorem OAI.MaxCutGames.Gadget.Harmonic.badRankCoefficient_nonneg line 698
def OAI.MaxCutGames.Gadget.Harmonic.depth line 701
theorem OAI.MaxCutGames.Gadget.Harmonic.depth_budget line 703

theorem OAI.MaxCutGames.Gadget.Harmonic.expected_total_drop_le line 713

Source documentation

Expected harmonic losses telescope. The ranks may be arbitrary functions of the full path; this assertion introduces no independence premise.

theorem expected_total_drop_le [Nonempty Ω] (rank : ℕ → Ω → ℕ)
    (r₀ s : ℕ) (θ : ℚ) (hinitial : ∀ ω, rank 0 ω = r₀)
    (hstep : ∀ j < s,
      average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) ≤ 4 * θ) :
    harmonic r₀ - average (fun ω => harmonic (rank s ω)) ≤ 4 * s * θ := by
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic

theorem OAI.MaxCutGames.Gadget.Harmonic.survival_probability_ge_half_of_potential line 736
Source documentation
The potential-to-survival step needs only the final finite experiment, allowing earlier levels to have different path sample spaces.
```
theorem survival_probability_ge_half_of_potential (rank : Ω → ℕ) (r₀ : ℕ)
    (hr₀ : 0 < r₀) (hterminal : ∀ ω, rank ω ≤ r₀)
    (hmean : harmonic r₀ / 2 ≤ average (fun ω => harmonic (rank ω))) :
    (1 / 2 : ℚ) ≤ probability (fun ω => 0 < rank ω) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.probability

theorem OAI.MaxCutGames.Gadget.Harmonic.survival_probability_ge_half line 760

Source documentation

At depth s with 4sθ ≤ H(r₀)/2, at least half the paths have nonzero terminal rank. The terminal bound follows from rank monotonicity in the actual gadget, and is kept explicit here.

theorem survival_probability_ge_half [Nonempty Ω] (rank : ℕ → Ω → ℕ)
    (r₀ s : ℕ) (θ : ℚ) (hr₀ : 0 < r₀)
    (hinitial : ∀ ω, rank 0 ω = r₀)
    (hterminal : ∀ ω, rank s ω ≤ r₀)
    (hstep : ∀ j < s,
      average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) ≤ 4 * θ)
    (hdepth : 4 * s * θ ≤ harmonic r₀ / 2) :
    (1 / 2 : ℚ) ≤ probability (fun ω => 0 < rank s ω) := by
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.Harmonic.probability

theorem OAI.MaxCutGames.Gadget.Harmonic.survival_of_adaptive_step_law line 776

Source documentation

Direct assembly of the adaptive calculation. conditionalDrop is the conditional mean after fixing the history; hmean is the finite averaging identity. The only assertion about bad orientations is their probability bound, so a future lift is allowed to depend on the incoming orientation.

theorem survival_of_adaptive_step_law [Nonempty Ω]
    (rank : ℕ → Ω → ℕ) (bad : ℕ → Ω → Prop)
    [∀ j, DecidablePred (bad j)] (conditionalDrop : ℕ → Ω → ℚ)
    (r₀ : ℕ) (θ ε : ℚ) (hr₀ : 0 < r₀) (hθ : 0 < θ)
    (hinitial : ∀ ω, rank 0 ω = r₀)
    (hterminal : ∀ ω, rank (depth r₀ θ) ω ≤ r₀)
    (hmean : ∀ j < depth r₀ θ,
      average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) =
        average (conditionalDrop j))
    (hconditional : ∀ j < depth r₀ θ, ∀ ω,
      conditionalDrop j ω ≤ 3 * θ + badRankCoefficient r₀ * θ *
        if bad j ω then 1 else 0)
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.depth, OAI.MaxCutGames.Gadget.Harmonic.average, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.Harmonic.badRankCoefficient

theorem OAI.MaxCutGames.Gadget.Harmonic.detection_probability_ge_quarter line 802

Source documentation

A final independent uniform symbol detects a surviving character with probability at least one half. Multiplying this conditional bound by the surviving-path probability gives the required quarter.

theorem detection_probability_ge_quarter [Nonempty Ω]
    (survives : Ω → Prop) [DecidablePred survives] (conditionalDetection : Ω → ℚ)
    (hsurvival : (1 / 2 : ℚ) ≤ probability survives)
    (hnonneg : ∀ ω, 0 ≤ conditionalDetection ω)
    (hdetect : ∀ ω, survives ω → (1 / 2 : ℚ) ≤ conditionalDetection ω) :
    (1 / 4 : ℚ) ≤ average conditionalDetection := by
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability, OAI.MaxCutGames.Gadget.Harmonic.average

theorem OAI.MaxCutGames.Gadget.Harmonic.probability_product line 823
Source documentation
Uniform paths and a separately sampled uniform terminal symbol have the product law used in the leaf-noise experiment.
```
theorem probability_product {Ξ : Type*} [Fintype Ξ]
    (detects : Ω × Ξ → Prop) [DecidablePred detects] :
    probability detects = average (fun ω => probability (fun ξ => detects (ω, ξ))) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability, OAI.MaxCutGames.Gadget.Harmonic.average
theorem OAI.MaxCutGames.Gadget.Harmonic.product_detection_probability_ge_quarter line 831

theorem OAI.MaxCutGames.Gadget.Harmonic.binary_product_detection_probability_ge_quarter line 846

Source documentation

Terminal family detection with actual binary characters rather than an assumed conditional probability bound. A character can be selected separately on every surviving path.

theorem binary_product_detection_probability_ge_quarter [Nonempty Ω]
    {Ξ : Type*} [Fintype Ξ] [AddGroup Ξ]
    (survives : Ω → Prop) [DecidablePred survives]
    (detects : Ω × Ξ → Prop) [DecidablePred detects]
    (hsurvival : (1 / 2 : ℚ) ≤ probability survives)
    (hcharacter : ∀ ω, survives ω → ∃ χ : Ξ →+ ZMod 2, ∃ v : Ξ,
      χ v ≠ 0 ∧ ∀ ξ, χ ξ ≠ 0 → detects (ω, ξ)) :
    (1 / 4 : ℚ) ≤ probability detects := by
…

Mentions: OAI.MaxCutGames.Gadget.Harmonic.probability