OAI/Probability/CriticalZ3/SeedQuality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalZ3.Model.BasicAdj line 13
2. def OAI.CriticalZ3.Model.VertexOpen line 17
3. def OAI.CriticalZ3.Model.SeedReaches line 21
4. theorem OAI.CriticalZ3.Model.seedReaches_bond line 25
5. theorem OAI.CriticalZ3.Model.seedReaches_site line 28
6. theorem OAI.CriticalZ3.Model.seedReaches_mono line 31
7. theorem OAI.CriticalZ3.Box.contains_cube_iff line 40
8. theorem OAI.CriticalZ3.Box.cube_bonds_eq line 43
9. theorem OAI.CriticalZ3.Box.cube_sites_eq line 48
10. theorem OAI.CriticalZ3.Model.seedReaches_determined line 56
11. theorem OAI.CriticalZ3.LatticeGraph.basicAdj_lift line 72
12. theorem OAI.CriticalZ3.LatticeGraph.seedReaches_conn line 84

    Source documentation

    Exact finite-graph continuation of the quarter-face seed event.

    theorem seedReaches_conn {c : Vertex} {a b : ℕ} (hab : a ≤ b)
        (hB : G.ContainsBox (Box.cube c b)) (T : Set Vertex) {ω : m.Config}
        {v : G.Node} (hv : v.1 = c)
        (hO : ω ∈ allValue ((Box.cube c a).bits m) true)
        (hE : ω ∈ m.SeedReaches c a b T) : G.Meets m ω v T := by
    …

    Mentions: OAI.CriticalZ3.Vertex, OAI.CriticalZ3.Box.cube, OAI.CriticalZ3.LatticeGraph.bits

13. theorem OAI.CriticalZ3.LatticeGraph.seed_conditional_quality line 113
14. theorem OAI.CriticalZ3.Box.successBits_contained line 143
15. def OAI.CriticalZ3.LatticeGraph.relayNode line 159
16. theorem OAI.CriticalZ3.LatticeGraph.bad_success_mass line 165

    Source documentation

    A single bad-success mass has the extra factor q for crossing bonds.

    theorem bad_success_mass (p : m.Bit → Set.Icc (0 : ℝ) 1) (q : Set.Icc (0 : ℝ) 1)
        (C : Box) (r : ℕ) (hw : ∀ i, C.lower i+r ≤ C.upper i-r)
        {y : Vertex} (hy : C.Exterior y)
        (hp : ∀ e ∈ (C.expand 1).bits m, p e = q)
        (F : Set m.Config) (hF : ProductCylinder.DeterminedBy (F := Prop) (C.bits m) (fun ω => ω ∈ F))
    …

    Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.LatticeGraph.bits, OAI.ProductCylinder.DeterminedBy

17. theorem OAI.CriticalZ3.LatticeGraph.measurableSet_meets_goodRelays line 206
18. theorem OAI.CriticalZ3.LatticeGraph.fixed_bad_success_mass line 217

    Source documentation

    Outside reveals preserve joint seed/quality statistics, as quality is an interior function rather than an outside-conditional prediction.

    theorem fixed_bad_success_mass (p : m.Bit → Set.Icc (0 : ℝ) 1) (q : Set.Icc (0 : ℝ) 1)
        (C : Box) (r : ℕ) (hw : ∀ i, C.lower i+r ≤ C.upper i-r)
        {y : Vertex} (hy : C.Exterior y) (ξ : m.Config)
        (hp : ∀ e ∈ (C.expand 1).bits m, p e = q)
        (F : Set m.Config) (hF : ProductCylinder.DeterminedBy (F := Prop) (C.bits m) (fun ω => ω ∈ F))
    …

    Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.LatticeGraph.bits, OAI.ProductCylinder.DeterminedBy