OAI/Computability/MaxCut/Games/HarmonicLoss.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Harmonic loss for the actual quadratic child maps

The probabilistic hypotheses of the MaxCutGames.Gadget.Harmonic.harmonic accounting lemmas are discharged here by the proved field-line kernel criterion and genericity count.

  1. theorem OAI.MaxCutGames.Quadratic.exists_nonzero_kernel_of_range_rank_lt_inline_HarmonicLoss line 20
  2. theorem OAI.MaxCutGames.Quadratic.probability_rank_drop_le_loss_count_inline_HarmonicLoss line 37
  3. def OAI.MaxCutGames.Quadratic.fieldLineTheta line 64
  4. theorem OAI.MaxCutGames.Quadratic.fieldLineTheta_eq line 68
  5. def OAI.MaxCutGames.Quadratic.nextBlockRank line 73

    Source documentation

    The image dimension of the actual oriented child restriction map.

    def nextBlockRank (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A)
    (A : FieldLine F) : ℕ :=
…

    Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation

  6. theorem OAI.MaxCutGames.Quadratic.nextBlockRank_le line 78
  7. theorem OAI.MaxCutGames.Quadratic.nextBlockRank_independent line 84

    Source documentation

    Changing the binary orientation of every child leaves its logical image rank unchanged.

    theorem nextBlockRank_independent (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J J' : ∀ A : FieldLine F, BlockOrientation A)
    (A : FieldLine F) : nextBlockRank S g J A = nextBlockRank S g J' A := by
…

    Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation, OAI.MaxCutGames.Quadratic.nextBlockRank

  8. theorem OAI.MaxCutGames.Quadratic.generic_nextBlockRank_dichotomy line 96
  9. theorem OAI.MaxCutGames.Quadratic.generic_block_loss_probability_le line 108
  10. theorem OAI.MaxCutGames.Quadratic.generic_block_harmonic_loss_le line 124

    Source documentation

    Actual generic block restrictions have rank-independent expected MaxCutGames.Gadget.Harmonic.harmonic loss.

    theorem generic_block_harmonic_loss_le (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A)
    (hS : IsGeneric S) :
    average (fun A => MaxCutGames.Gadget.Harmonic.harmonic (Module.finrank (ZMod 2) S) -
      MaxCutGames.Gadget.Harmonic.harmonic (nextBlockRank S g J A)) ≤ 3 * fieldLineTheta F := by
…

    Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Quadratic.nextBlockRank, OAI.MaxCutGames.Quadratic.fieldLineTheta

  11. theorem OAI.MaxCutGames.Quadratic.card_loss_fieldLineRestrictions_le_nonzero line 146
  12. theorem OAI.MaxCutGames.Quadratic.arbitrary_block_loss_probability_le line 161
  13. theorem OAI.MaxCutGames.Quadratic.arbitrary_block_harmonic_loss_le line 181
  14. def OAI.MaxCutGames.Gadget.OutgoingHarmonic.outgoingLoss line 212
  15. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.outgoingLoss_eq_line_average line 219

    Source documentation

    Averaging all binary orientations reduces exactly to the actual line-law rank experiment, after transporting logical characters by the trace pairing.

    theorem outgoingLoss_eq_line_average
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  16. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.generic_outgoing_loss_le line 240

    Source documentation

    The generic all-lifts bound applies to the actual common parent map.

    theorem generic_outgoing_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  17. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.arbitrary_outgoing_loss_le line 249

    Source documentation

    Nongeneric actual child maps satisfy the fallback MaxCutGames.Gadget.Harmonic.harmonic charge.

    theorem arbitrary_outgoing_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  18. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.badRankCoefficient_mono line 257
  19. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.outgoing_harmonic_loss_le line 266

    Source documentation

    Combined conditional law with a coefficient frozen at the initial rank. The bad predicate is exactly the nongeneric trace-coordinate domain.

    theorem outgoing_harmonic_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  20. theorem OAI.MaxCutGames.Gadget.OutgoingHarmonic.descendant_harmonic_loss_le line 287

    Source documentation

    Direct instantiation of DescentProbability.expected_terminal_loss's outgoing-step hypothesis for the concrete child domain of every actual lift.

    theorem descendant_harmonic_loss_le
    [DecidableEq (BlockOrientationIndex F)] [Nonempty (BlockOrientationIndex F)] :
    let J : BlockOrientationIndex F → Vec F →ₗ[ZMod 2] Vec F × Vec F :=
…
  21. def OAI.MaxCutGames.Quadratic.nongenericFraction line 321

    Source documentation

    The actual uniform fraction of nongeneric rank-r binary subspaces.

    def nongenericFraction (F : Type*) [Field F] [Fintype F] [CharP F 2]
    [Algebra (ZMod 2) F] (r : ℕ) : ℚ :=
…
  22. def OAI.MaxCutGames.Gadget.FreshGenericity.rankSpaceEquiv line 345

    Source documentation

    A fixed coordinate equivalence transports the complete rank-indexed Grassmannian bijectively, so it preserves its uniform distribution.

    def rankSpaceEquiv (e : V ≃ₗ[K] W) (r : ℕ) : RankSpace K V r ≃ RankSpace K W r :=
…
  23. theorem OAI.MaxCutGames.Gadget.FreshGenericity.rankSpaceEquiv_apply line 350
  24. def OAI.MaxCutGames.Gadget.FreshGenericity.bad line 374

    Source documentation

    Nongenericity includes the universal lift quantifier in IsGeneric. The field's simultaneous bound includes rank zero as well.

    def bad (S : Submodule (ZMod 2) (BinaryDual (F := F))) : Prop :=
…
  25. theorem OAI.MaxCutGames.Gadget.FreshGenericity.mean_bad_rankSpace line 377
  26. theorem OAI.MaxCutGames.Gadget.FreshGenericity.mean_fresh_bad_at_line line 396
  27. theorem OAI.MaxCutGames.Gadget.FreshGenericity.unoriented_rank_le line 420
  28. theorem OAI.MaxCutGames.Gadget.FreshGenericity.fresh_bad_at_line_le line 431

    Source documentation

    The field error bound applies to the actual fresh descendant rank, even though that rank depends on the earlier lift and the selected line.

    theorem fresh_bad_at_line_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  29. theorem OAI.MaxCutGames.Gadget.FreshGenericity.fresh_bad_le line 446

    Source documentation

    Fresh nongenericity bound over the actual full child index. The parent family and the common-parent map are arbitrary fixed inputs, so the result applies at every adaptive history without a future-lift independence premise.

    theorem fresh_bad_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
  30. theorem OAI.MaxCutGames.Gadget.FreshGenericity.descendant_bad_le line 464

    Source documentation

    The fresh bound for the deterministic descendant of an actual parent lift. The common-parent map is chosen from the whole lift before sampling the child index, exactly as required by the adaptive finite-history experiment.

    theorem descendant_bad_le
    [DecidableEq (BlockOrientationIndex F)] [Nonempty (BlockOrientationIndex F)] :
    let J := orientedBlockLinear (F := F)
…
  31. instance OAI.MaxCutGames.Gadget.DescentProbability.noiseFintype line 504
  32. def OAI.MaxCutGames.Gadget.DescentProbability.terminalPotential line 510
  33. theorem OAI.MaxCutGames.Gadget.DescentProbability.terminalPotential_zero line 515
  34. theorem OAI.MaxCutGames.Gadget.DescentProbability.terminalPotential_succ line 523
  35. theorem OAI.MaxCutGames.Gadget.DescentProbability.expected_terminal_loss line 539

    Source documentation

    The only geometric inputs are the outgoing MaxCutGames.Gadget.Harmonic.harmonic loss estimate for every lift and the fresh-orientation bound for every child image. The lift may depend on every previous orientation; the proof never declares it independent.

    theorem expected_terminal_loss
    (bad : Submodule k (B →ₗ[k] k) → Prop) [DecidablePred bad]
    (r₀ : ℕ) (C θ ε : ℚ) (hC : 0 ≤ C) (hθ : 0 ≤ θ) (hsmall : C * ε ≤ 1)
    (hstep : ∀ (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
      (L : Lift (Stage.next J hJ Q s) S), Module.finrank k S ≤ r₀ →
      average (fun i => MaxCutGames.Gadget.Harmonic.harmonic (Module.finrank k S) -
        MaxCutGames.Gadget.Harmonic.harmonic (Module.finrank k (childDomain J hJ Q s S L i))) ≤
          3 * θ + C * θ * if bad S then 1 else 0)
    (hfresh : ∀ (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
      (L : Lift (Stage.next J hJ Q s) S), Module.finrank k S ≤ r₀ →
      probability (fun i => bad (childDomain J hJ Q s S L i)) ≤ ε)
    (n : ℕ) (S : Submodule k (B →ₗ[k] k)) (L : Lift (Stage.iterate J hJ Q n) S)
…

    Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.next, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.Stage.iterate

  36. def OAI.MaxCutGames.Gadget.LeafDetection.survivalProbability line 600
  37. def OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability line 605
  38. theorem OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability_nonneg line 612
  39. theorem OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability_restrict_le line 621

    Source documentation

    Restricting the logical domain can only remove detecting characters.

    theorem detectionProbability_restrict_le (n : ℕ)
    (S T : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2)) (hST : S ≤ T)
    (L : Lift (Stage.iterate J hJ Q n) T) :
    detectionProbability J hJ Q n S (L.restrict hST) ≤
      detectionProbability J hJ Q n T L := by
…

    Mentions: OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.iterate, OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability

  40. theorem OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability_zero_of_rank_pos line 632
  41. theorem OAI.MaxCutGames.Gadget.LeafDetection.survivalProbability_zero line 657
  42. theorem OAI.MaxCutGames.Gadget.LeafDetection.survivalProbability_succ line 667
  43. theorem OAI.MaxCutGames.Gadget.LeafDetection.average_child_detection_le line 682
  44. theorem OAI.MaxCutGames.Gadget.LeafDetection.half_survival_le_detection line 703

    Source documentation

    Detection by the root lift is at least one half the actual terminal-rank survival probability, on precisely the recursively generated noise sample.

    theorem half_survival_le_detection (n : ℕ)
    (S : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2))
    (L : Lift (Stage.iterate J hJ Q n) S) :
    (1 / 2 : ℚ) * survivalProbability J hJ Q n S L ≤
      detectionProbability J hJ Q n S L := by
…

    Mentions: OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.iterate, OAI.MaxCutGames.Gadget.LeafDetection.survivalProbability, OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability

  45. theorem OAI.MaxCutGames.Gadget.LeafDetection.quarter_detection_of_terminal_potential line 728

    Source documentation

    Actual quarter detection follows from retaining half the initial MaxCutGames.Gadget.Harmonic.harmonic potential; all leaf-to-root event containments are already proved.

    theorem quarter_detection_of_terminal_potential (n : ℕ)
    (S : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2))
    (L : Lift (Stage.iterate J hJ Q n) S)
    (hrank : 0 < Module.finrank (ZMod 2) S)
    (hpotential : MaxCutGames.Gadget.Harmonic.harmonic (Module.finrank (ZMod 2) S) / 2 ≤
      terminalPotential J hJ Q n S L) :
    (1 / 4 : ℚ) ≤ detectionProbability J hJ Q n S L := by
…

    Mentions: OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.iterate, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability

  46. theorem OAI.MaxCutGames.Gadget.LeafDetection.quarter_detection_of_restricted_terminal_potential line 743

    Source documentation

    The fixed generic top subspace may be chosen inside a full logical family; the resulting quarter bound still concerns the original lift.

    theorem quarter_detection_of_restricted_terminal_potential (n : ℕ)
    (S T : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2)) (hST : S ≤ T)
    (L : Lift (Stage.iterate J hJ Q n) T)
    (hrank : 0 < Module.finrank (ZMod 2) S)
    (hpotential : MaxCutGames.Gadget.Harmonic.harmonic (Module.finrank (ZMod 2) S) / 2 ≤
      terminalPotential J hJ Q n S (L.restrict hST)) :
    (1 / 4 : ℚ) ≤ detectionProbability J hJ Q n T L :=
…

    Mentions: OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.iterate, OAI.MaxCutGames.Gadget.Harmonic.harmonic, OAI.MaxCutGames.Gadget.LeafDetection.detectionProbability