OAI/Probability/CriticalZ3/Relay.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LatticeRelay.Vertex line 11
2. def OAI.LatticeRelay.Rect line 13
3. def OAI.LatticeRelay.Cube line 14
4. def OAI.LatticeRelay.Expand line 15
5. def OAI.LatticeRelay.DirectedInterval line 16
6. def OAI.LatticeRelay.QuarterFace line 19
7. def OAI.LatticeRelay.inward line 23
8. def OAI.LatticeRelay.Prism line 25
9. theorem OAI.LatticeRelay.inward_endpoint_bound line 29
10. theorem OAI.LatticeRelay.inward_interval_bound line 34
11. theorem OAI.LatticeRelay.quarterFace_subset_cube line 39
12. theorem OAI.LatticeRelay.quarterFace_nonempty line 53
13. theorem OAI.LatticeRelay.contraction_face line 63

    Source documentation

    Generic form of one of the three contraction steps.

    theorem contraction_face {r a : ℤ} (hr : 0 ≤ r) (ha : 0 ≤ a) (h : Fin 3)
        {u : Vertex}
        (hu : ∀ i, |u i| ≤ if i < h then 2*r+a else 4*r+a) :
        QuarterFace u (2*r) h (inward u) ⊆
          Rect 0 (fun i => if i ≤ h then 2*r+a else 4*r+a) := by
    …

    Mentions: OAI.LatticeRelay.Vertex, OAI.LatticeRelay.QuarterFace, OAI.LatticeRelay.inward, OAI.LatticeRelay.Rect

14. theorem OAI.LatticeRelay.contraction_cube line 85
15. def OAI.LatticeRelay.axisCenter line 105
16. def OAI.LatticeRelay.forwardInward line 107
17. theorem OAI.LatticeRelay.translation_face line 112

    Source documentation

    Generic form of each of the ten translation steps, including the final length 2r+1 step.

    theorem translation_face {a s w : ℤ} (hs : s ≤ w) {u : Vertex}
        (hu : u ∈ Cube (axisCenter a) w) :
        QuarterFace u s 0 (forwardInward u) ⊆ Cube (axisCenter (a+s)) w := by
    …

    Mentions: OAI.LatticeRelay.Vertex, OAI.LatticeRelay.Cube, OAI.LatticeRelay.axisCenter, OAI.LatticeRelay.QuarterFace, OAI.LatticeRelay.forwardInward

18. theorem OAI.LatticeRelay.translation_cube line 127
19. def OAI.LatticeRelay.contractionWidths line 148
20. def OAI.LatticeRelay.HasInterface line 151
21. theorem OAI.LatticeRelay.contraction_interface line 155
22. theorem OAI.LatticeRelay.translation_interface line 181
23. def OAI.LatticeRelay.routeCenter line 194
24. def OAI.LatticeRelay.routeWidths line 196
25. def OAI.LatticeRelay.P line 199
26. theorem OAI.LatticeRelay.axisCenter_zero line 201
27. theorem OAI.LatticeRelay.routeCenter_translation line 203
28. theorem OAI.LatticeRelay.routeWidths_translation line 211
29. def OAI.LatticeRelay.stepSize line 220
30. theorem OAI.LatticeRelay.routeCenter_next line 222
31. theorem OAI.LatticeRelay.thirteen_interfaces line 238
32. theorem OAI.LatticeRelay.P_zero line 273
33. theorem OAI.LatticeRelay.P_thirteen_subset line 279
34. theorem OAI.LatticeRelay.expanded_route_subset_prism line 289