OAI/Probability/CriticalZ3/Main.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CriticalZ3.bond_critical_origin line 13

   Source documentation

   Vanishing origin order parameter at the exact bond critical infimum.

   theorem bond_critical_origin : bondLaw bondCritical (bondInfiniteAt 0) = 0 := by
   …

   Mentions: OAI.CriticalZ3.bondLaw, OAI.CriticalZ3.bondCritical, OAI.CriticalZ3.bondInfiniteAt

2. theorem OAI.CriticalZ3.site_critical_origin line 23

   Source documentation

   Vanishing origin order parameter at the separate site critical infimum.

   theorem site_critical_origin : siteLaw siteCritical (siteInfiniteAt 0) = 0 := by
   …

   Mentions: OAI.CriticalZ3.siteLaw, OAI.CriticalZ3.siteCritical, OAI.CriticalZ3.siteInfiniteAt

3. theorem OAI.CriticalZ3.SignedSymmetry.bondConnected_map line 34
4. theorem OAI.CriticalZ3.SignedSymmetry.siteConnected_map line 38
5. theorem OAI.CriticalZ3.SignedSymmetry.bondInfiniteAt_map line 42
6. theorem OAI.CriticalZ3.SignedSymmetry.siteInfiniteAt_map line 55
7. theorem OAI.CriticalZ3.bondInfiniteAt_probability line 69
8. theorem OAI.CriticalZ3.siteInfiniteAt_probability line 80
9. theorem OAI.CriticalZ3.bond_critical_no_infinite line 92

   Source documentation

   Nearest-neighbor bond percolation on Z³ has almost surely no infinite cluster at criticality.

   theorem bond_critical_no_infinite :
       ∀ᵐ ω ∂bondLaw bondCritical, ∀ x : Vertex, (bondCluster ω x).Finite := by
   …

   Mentions: OAI.CriticalZ3.bondLaw, OAI.CriticalZ3.bondCritical, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.bondCluster

10. theorem OAI.CriticalZ3.site_critical_no_infinite line 100

    Source documentation

    Nearest-neighbor site percolation on Z³ has almost surely no infinite cluster at its own criticality.

    theorem site_critical_no_infinite :
        ∀ᵐ ω ∂siteLaw siteCritical, ∀ x : Vertex, (siteCluster ω x).Finite := by
    …

    Mentions: OAI.CriticalZ3.siteLaw, OAI.CriticalZ3.siteCritical, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.siteCluster

11. theorem OAI.CriticalZ3.critical_no_infinite line 107

    Distinct definitions of this name: ComparatorChallenges/CriticalZ3.lean:56 (same statement text; different proof or body). Qualify references as OAI.CriticalZ3.critical_no_infinite@path.