Road.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

The road seen from the input. This representation can truncate the play at transfers.

inductive OAI.FourierLLogL.Dyadic.Procedure.Pace line 15
Source documentation
Unary pace: entering the static system, or starting a new plateau
```
inductive Pace
| renew | cross deriving DecidableEq
```
def OAI.FourierLLogL.Dyadic.Procedure.Scene.pace line 18
lemma OAI.FourierLLogL.Dyadic.Procedure.pace_mass line 21
lemma OAI.FourierLLogL.Dyadic.Procedure.pace_actor line 22
inductive OAI.FourierLLogL.Dyadic.Procedure.Turn line 24
def OAI.FourierLLogL.Dyadic.Procedure.Turn.fork line 28
lemma OAI.FourierLLogL.Dyadic.Procedure.Turn.source line 31
inductive OAI.FourierLLogL.Dyadic.Procedure.Road line 33
def OAI.FourierLLogL.Dyadic.Procedure.Road.trace line 41
Source documentation
extend means continuing into the static system.
```
def trace (throughCold : Bool) {s : Scene M} (t : Play j M s) : Road j M s :=
…
```
Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Play, OAI.FourierLLogL.Dyadic.Procedure.Road
def OAI.FourierLLogL.Dyadic.Procedure.Road.pace_ok line 53
def OAI.FourierLLogL.Dyadic.Procedure.Road.turn_ok line 55
def OAI.FourierLLogL.Dyadic.Procedure.Road.Trusted line 61
Source documentation
f and J ambient original data.
```
def Trusted (J : ℕ) (f : Grid M → ℝ) {s : Scene M} (r : Road j M s) : Prop :=
…
```
Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Road
lemma OAI.FourierLLogL.Dyadic.Procedure.Road.traced line 67
lemma OAI.FourierLLogL.Dyadic.Procedure.Road.rootSafe line 86
lemma OAI.FourierLLogL.Dyadic.Procedure.Road.branchTrusted line 89
inductive OAI.FourierLLogL.Dyadic.Procedure.Event line 101
Source documentation
One edge actually seen.
```
inductive Event (j M : ℕ)
| march (s : Scene M) (v : Turn j s) (b : Bool) : Event j M
| pace (s : Scene M) (v : Pace) : Event j M
```
Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Turn, OAI.FourierLLogL.Dyadic.Procedure.Pace
def OAI.FourierLLogL.Dyadic.Procedure.Event.dest line 105
def OAI.FourierLLogL.Dyadic.Procedure.Event.src line 107
structure OAI.FourierLLogL.Dyadic.Procedure.Journal line 110
def OAI.FourierLLogL.Dyadic.Procedure.Journal.prepend line 116
def OAI.FourierLLogL.Dyadic.Procedure.Journal.fee line 117
lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.fee_pre line 119
def OAI.FourierLLogL.Dyadic.Procedure.Road.hike line 127

lemma OAI.FourierLLogL.Dyadic.Procedure.Road.travel line 136

Source documentation

True induction along the observed path.

lemma travel {f : Grid M → ℝ} {good : Scene M → Journal j M → Prop}
    (he : ∀ s b, Safe s j J f → (if b then s.openHere j J f ∧ s.retire j else ¬ s.openHere j J f) →
       0 < s.mass → good s ⟨s,b,[]⟩)
    (h1 : ∀ (s : Scene M) (v : Pace), Safe s j J f → s.openHere j J f → pace_ok s v j →
      ∀ l : Journal j M, good (s.pace v) l → good s (l.prepend (Event.pace s v)))
    (h2 : ∀ (s : Scene M) (v : Turn j s), Safe s j J f → s.work j J f → turn_ok v →
      v.fork.TrueLaw →
      ∀ b : Bool, 0 < v.fork.probs b → ∀ l, good (v.fork.dst b) l → good s (l.prepend (.march s v b)))
    (t : Road j M s) (h : t.Trusted J f) (hm : 0 < s.mass) {x : Grid M} (hx : 0 < s.actor x) :
    good s (t.hike x) := by
…

Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Journal, OAI.FourierLLogL.Dyadic.Procedure.Pace, OAI.FourierLLogL.Dyadic.Procedure.Road.pace_ok, OAI.FourierLLogL.Dyadic.Procedure.Turn, OAI.FourierLLogL.Dyadic.Procedure.Road.turn_ok, OAI.FourierLLogL.Dyadic.Procedure.Road

def OAI.FourierLLogL.Dyadic.Procedure.Road.expHike line 157
lemma OAI.FourierLLogL.Dyadic.Procedure.Road.Ex_hike_fork line 160
lemma OAI.FourierLLogL.Dyadic.Procedure.Road.Ex_hike_push line 170