ComparatorChallenges/BenjaminiSchramm.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

45 declarations, 3 contain sorry, 0 declared as axioms

  1. abbrev OAI.Percolation.BondGraph line 12

    Also declared: ComparatorChallenges/CayleyPercolation.lean:14 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:14 (same declaration text).

  2. def OAI.Percolation.Adj line 14

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:17 (same declaration text).

  3. def OAI.Percolation.LocallyFinite line 16

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:20 (same declaration text).

  4. def OAI.Percolation.Connected line 18

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:23 (same declaration text).

  5. def OAI.Percolation.IsAut line 21

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:27 (same declaration text).

  6. def OAI.Percolation.QuasiTransitive line 24

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:31 (same declaration text).

  7. def OAI.Percolation.vertexBoundary line 28

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:36 (same declaration text).

  8. def OAI.Percolation.hV line 31

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:40 (same declaration text).

  9. def OAI.Percolation.Conn line 35

    Also declared: ComparatorChallenges/CayleyPercolation.lean:16 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:45 (same declaration text).

  10. def OAI.Percolation.cluster line 38

    Also declared: ComparatorChallenges/CayleyPercolation.lean:19 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:48 (same declaration text).

  11. def OAI.Percolation.infiniteClusters line 41

    Also declared: ComparatorChallenges/CayleyPercolation.lean:22 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:52 (same declaration text).

  12. def OAI.Percolation.law line 44

    Also declared: ComparatorChallenges/CayleyPercolation.lean:25 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:56 (same declaration text).

  13. def OAI.Percolation.pc line 47

    Also declared: ComparatorChallenges/CayleyPercolation.lean:28 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:59 (same declaration text).

  14. def OAI.Percolation.pu line 50

    Also declared: ComparatorChallenges/CayleyPercolation.lean:31 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:62 (same declaration text).

  15. def OAI.Percolation.twoPoint line 53

    Also declared: ComparatorChallenges/CayleyPercolation.lean:34 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:65 (same declaration text).

  16. abbrev OAI.Percolation.Hilbert line 56

    Also declared: ComparatorChallenges/CayleyPercolation.lean:37 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:68 (same declaration text).

  17. def OAI.Percolation.HasKernel line 58

    Also declared: ComparatorChallenges/CayleyPercolation.lean:39 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:71 (same declaration text).

  18. def OAI.Percolation.OperatorBounded line 63

    Also declared: ComparatorChallenges/CayleyPercolation.lean:44 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:76 (same declaration text).

  19. def OAI.Percolation.operatorNorm line 67

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:81 (same declaration text).

  20. def OAI.Percolation.ptwo line 72

    Also declared: ComparatorChallenges/CayleyPercolation.lean:48 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:86 (same declaration text).

  21. def OAI.Percolation.labelLaw line 75

    Also declared: ComparatorChallenges/CayleyPercolation.lean:51 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:90 (same declaration text).

  22. def OAI.Percolation.openEdges line 78

    Also declared: ComparatorChallenges/CayleyPercolation.lean:54 (same declaration text), OAI/Probability/UnimodularPercolation/Graph/Basic.lean:93 (same declaration text).

  23. def OAI.Percolation.MainConclusion line 81

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Basic.lean:97 (same declaration text).

  24. def OAI.Percolation.openSimpleGraph line 99

    Also declared: OAI/Probability/UnimodularPercolation/Graph/Paths.lean:32 (same declaration text).

  25. def OAI.Percolation.susceptibility line 115

    Also declared: OAI/Probability/UnimodularPercolation/Clusters/KernelMoments.lean:789 (same declaration text).

  26. def OAI.Percolation.BenjaminiSchramm.triangleDiagram line 127

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:22 (same declaration text).

  27. def OAI.Percolation.BenjaminiSchramm.graphDistance line 131

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:26 (same declaration text).

  28. def OAI.Percolation.BenjaminiSchramm.ExponentialDecay line 134

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:29 (same declaration text).

  29. def OAI.Percolation.BenjaminiSchramm.pexp line 138

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:33 (same declaration text).

  30. def OAI.Percolation.BenjaminiSchramm.PowerTail line 141

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:36 (same declaration text).

  31. def OAI.Percolation.BenjaminiSchramm.volumeEvent line 145

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:40 (same declaration text).

  32. def OAI.Percolation.BenjaminiSchramm.intrinsicRadiusEvent line 148

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:43 (same declaration text).

  33. def OAI.Percolation.BenjaminiSchramm.extrinsicRadiusEvent line 151

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:46 (same declaration text).

  34. def OAI.Percolation.BenjaminiSchramm.criticalTail line 154

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:49 (same declaration text).

  35. def OAI.Percolation.BenjaminiSchramm.CriticalTailLaws line 158

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:53 (same declaration text).

  36. def OAI.Percolation.BenjaminiSchramm.SusceptibilityLaw line 163

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:58 (same declaration text).

  37. def OAI.Percolation.BenjaminiSchramm.percolationProbability line 169

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:64 (same declaration text).

  38. def OAI.Percolation.BenjaminiSchramm.PercolationProbabilityLaw line 172

    Also declared: OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean:67 (same declaration text).

  39. def OAI.Percolation.BenjaminiSchramm.CriticalLawsConclusion line 186

    Also declared: OAI/Probability/BenjaminiSchramm/Consequences.lean:52 (same declaration text).

  40. abbrev OAI.Percolation.BenjaminiSchramm.CayleyEdge line 202

    Also declared: OAI/Probability/BenjaminiSchramm/Cayley.lean:14 (same declaration text).

  41. def OAI.Percolation.BenjaminiSchramm.cayleyBond line 204

    Also declared: OAI/Probability/BenjaminiSchramm/Cayley.lean:16 (same declaration text).

  42. def OAI.Percolation.BenjaminiSchramm.FolnerAmenable line 206

    Also declared: OAI/Probability/BenjaminiSchramm/Cayley.lean:89 (same declaration text).

  43. theorem OAI.Percolation.BenjaminiSchramm.full_main Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs sorry line 217

    Source documentation

    Critical operator boundedness, the threshold gap, and simultaneous nonuniqueness.

    L4DEL explanation

    Critical operator boundedness, the threshold gap, and simultaneous nonuniqueness.

    1. This explanation is a condensed rendering of this declaration's own doc comment at the pinned source commit.
    2. The linked formalization note covers 2 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    3. The repository's comparator configuration selects OAI.Probability.BenjaminiSchramm.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/BenjaminiSchramm/Main.lean:9 (different declaration text). Qualify references as OAI.Percolation.BenjaminiSchramm.full_main@path.

    theorem full_main {V : Type u} {E : Type v} [Infinite V]
    (G : BondGraph V E) (hc : Connected G) (hl : LocallyFinite G)
    (hq : QuasiTransitive G) (hh : 0 < hV G) : MainConclusion G := by
…

    Mentions: OAI.Percolation.BondGraph, OAI.Percolation.Connected, OAI.Percolation.LocallyFinite, OAI.Percolation.QuasiTransitive, OAI.Percolation.hV, OAI.Percolation.MainConclusion

  44. theorem OAI.Percolation.BenjaminiSchramm.critical_laws Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs sorry line 223

    Source documentation

    Critical mean-field laws and uniform exponential connectivity below the operator threshold.

    L4DEL explanation

    Critical mean-field laws and uniform exponential connectivity below the operator threshold.

    1. This explanation is a condensed rendering of this declaration's own doc comment at the pinned source commit.
    2. The linked formalization note covers 2 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    3. The repository's comparator configuration selects OAI.Probability.BenjaminiSchramm.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/BenjaminiSchramm/Main.lean:14 (different declaration text). Qualify references as OAI.Percolation.BenjaminiSchramm.critical_laws@path.

    theorem critical_laws {V : Type u} {E : Type v} [Infinite V]
    (G : BondGraph V E) (hc : Connected G) (hl : LocallyFinite G)
    (hq : QuasiTransitive G) (hh : 0 < hV G) : CriticalLawsConclusion G := by
…

    Mentions: OAI.Percolation.BondGraph, OAI.Percolation.Connected, OAI.Percolation.LocallyFinite, OAI.Percolation.QuasiTransitive, OAI.Percolation.hV, OAI.Percolation.BenjaminiSchramm.CriticalLawsConclusion

  45. theorem OAI.Percolation.BenjaminiSchramm.cayley_main Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs sorry line 229

    Source documentation

    Nonuniqueness for every prescribed finite symmetric Cayley generating set.

    L4DEL explanation

    Nonuniqueness for every prescribed finite symmetric Cayley generating set.

    1. This explanation is a condensed rendering of this declaration's own doc comment at the pinned source commit.
    2. The linked formalization note covers 2 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    3. The repository's comparator configuration selects OAI.Probability.BenjaminiSchramm.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/BenjaminiSchramm/CayleyTheorem.lean:14 (different declaration text). Qualify references as OAI.Percolation.BenjaminiSchramm.cayley_main@path.

    theorem cayley_main {Λ : Type u} [Group Λ]
    (S : Finset Λ) (hsym : ∀ s ∈ S, s⁻¹ ∈ S) (_hone : 1 ∉ S)
    (hgen : Subgroup.closure (S : Set Λ) = ⊤) (hna : ¬ FolnerAmenable Λ) :
    OperatorBounded (cayleyBond S) (pc (cayleyBond S)) ∧
      MainConclusion (cayleyBond S) ∧
      ∀ p : unitInterval, pc (cayleyBond S) < p → p < pu (cayleyBond S) →
        ∀ᵐ ω ∂law p, (infiniteClusters (cayleyBond S) ω).Infinite := by
…

    Mentions: OAI.Percolation.BenjaminiSchramm.FolnerAmenable, OAI.Percolation.OperatorBounded, OAI.Percolation.BenjaminiSchramm.cayleyBond, OAI.Percolation.pc, OAI.Percolation.MainConclusion, OAI.Percolation.pu, OAI.Percolation.law, OAI.Percolation.infiniteClusters