QueryCombinators.lean`

88 declarations, 0 contain sorry, 0 declared as axioms

Finite query combinators and transparent Bernoulli operations.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

abbrev OAI.ExactDerandomization.Arena.Sight line 22
abbrev OAI.ExactDerandomization.Arena.Kiwi line 23
abbrev OAI.ExactDerandomization.Arena.Pier.StampX line 30
lemma OAI.ExactDerandomization.Arena.Pier.seal0 line 31
lemma OAI.ExactDerandomization.Arena.Pier.seal1 line 34
lemma OAI.ExactDerandomization.Arena.Pier.seal_bit line 37
lemma OAI.ExactDerandomization.Arena.Pier.seal_mark line 41
structure OAI.ExactDerandomization.Arena.Pier.Liaison line 50
Source documentation
A reserved opaque motion; synaptic grab may also return "no". (motion called only at address clock=0; enclosing data operations strip their shot clock while keeping bounded record).
```
structure Liaison (x:ℕ) (u:ℕ)(t i:ℕ) : Prop where
…
```
def OAI.ExactDerandomization.Arena.Pier.onyx line 56
lemma OAI.ExactDerandomization.Arena.Pier.onyxK line 58
def OAI.ExactDerandomization.Arena.Pier.walk line 60
lemma OAI.ExactDerandomization.Arena.Pier.shares line 68
lemma OAI.ExactDerandomization.Arena.Pier.stroll line 83
lemma OAI.ExactDerandomization.Arena.Pier.street line 99
def OAI.ExactDerandomization.Arena.Pier.escort line 103
lemma OAI.ExactDerandomization.Arena.Pier.cups line 108
lemma OAI.ExactDerandomization.Arena.Pier.bowls line 116
abbrev OAI.ExactDerandomization.Arena.Iris.matchQ line 133
def OAI.ExactDerandomization.Arena.Iris.through line 134
def OAI.ExactDerandomization.Arena.Iris.dial line 137
lemma OAI.ExactDerandomization.Arena.Iris.remise line 140
lemma OAI.ExactDerandomization.Arena.Iris.rosary line 152
lemma OAI.ExactDerandomization.Arena.Iris.parcel line 156
def OAI.ExactDerandomization.Arena.Flash.search line 178
Source documentation
Probe a pure function of (info, cursor) before any descent.
```
def search (g:Cub (ℕ×ℕ) ℕ):Cog :=
…
```
lemma OAI.ExactDerandomization.Arena.Flash.found line 184
def OAI.ExactDerandomization.Arena.Flash.plumb line 193
lemma OAI.ExactDerandomization.Arena.Flash.pureQ line 194
abbrev OAI.ExactDerandomization.Arena.Flash.chose line 197
abbrev OAI.ExactDerandomization.Arena.Flash.win line 198
lemma OAI.ExactDerandomization.Arena.Flash.picks line 199
abbrev OAI.ExactDerandomization.Arena.Flash.demand line 206
lemma OAI.ExactDerandomization.Arena.Flash.wanted line 207
lemma OAI.ExactDerandomization.Arena.Flash.win_stamped line 213
lemma OAI.ExactDerandomization.Arena.Flash.brilliant line 215
lemma OAI.ExactDerandomization.Arena.Flash.gild line 219
Source documentation
Two threshold constants compiled as motions.Literal recipes are regenerated without using the cursor.
```
lemma gild (u v:ℕ)(_:u ≤ v):1 ≤  v+1:= Nat.le_add_left _ _
```
abbrev OAI.ExactDerandomization.Arena.Flash.clan line 220
abbrev OAI.ExactDerandomization.Arena.Flash.garnish line 222

lemma OAI.ExactDerandomization.Arena.Flash.maskB line 226

Source documentation

one visit interpreted as a boolean at the endpoint, payload already rebased.

lemma maskB {h:Harp}{v:Harp.Wick}{b i x q:ℕ}{f:Option (ℕ×ℕ)}{C:Cub ℕ (ℕ×ℕ×NoteM)}
    (hu:v.d.Suite u)(hx:x∈v.d.P)(hc:2 ≤ c)(hh:v.d.W b+v.d.D u ≤ v.d.W u)
    (hz:v.Veil h b){m:NoteM}(hr:C.f v.d.x q=(b,i,m))(he:v.Ok m)
    (hf:v.r.Flora h.p b i x f)(a:Bool)
    (ha:match f with
        | none=>a=false
        | some (_,y) => ∀ p,v.d.r.proper p→ h.lit v.d.x m y p=(a,p)):
   (v.d.chord u x q).rite c (Dome.Bullet.snap (garnish C)) (enc a) :=by
…

Mentions: OAI.ExactDerandomization.Arena.Flash.garnish

structure OAI.ExactDerandomization.Arena.Gate line 250
abbrev OAI.ExactDerandomization.Arena.Gate.reach line 258
def OAI.ExactDerandomization.Arena.Gate.garden line 259
def OAI.ExactDerandomization.Arena.Gate.openE line 263
structure OAI.ExactDerandomization.Arena.Gate.Crest line 267
lemma OAI.ExactDerandomization.Arena.Gate.Crest.asleep line 276
lemma OAI.ExactDerandomization.Arena.Gate.Crest.morning line 280
abbrev OAI.ExactDerandomization.Arena.Amber.Tear line 306
Source documentation
Enter a transparent Bernoulli coin (pure rational expression).
```
abbrev Tear:=Cub History Coin
```
abbrev OAI.ExactDerandomization.Arena.Amber.here line 307
abbrev OAI.ExactDerandomization.Arena.Amber.moonF line 309
abbrev OAI.ExactDerandomization.Arena.Amber.opaque0 line 310
abbrev OAI.ExactDerandomization.Arena.Amber.syrup line 311
abbrev OAI.ExactDerandomization.Arena.Amber.first0 line 312
abbrev OAI.ExactDerandomization.Arena.Amber.awry line 313
lemma OAI.ExactDerandomization.Arena.Amber.occlude line 316
lemma OAI.ExactDerandomization.Arena.Amber.scalingF line 324
lemma OAI.ExactDerandomization.Arena.Amber.normalizeF line 327
abbrev OAI.ExactDerandomization.Arena.Amber.shade line 334
abbrev OAI.ExactDerandomization.Arena.Amber.petal line 335
abbrev OAI.ExactDerandomization.Arena.Amber.blossoms line 336
lemma OAI.ExactDerandomization.Arena.Amber.cast line 337
lemma OAI.ExactDerandomization.Arena.Amber.pour line 343
lemma OAI.ExactDerandomization.Arena.Amber.seeds line 349
abbrev OAI.ExactDerandomization.Arena.Amber.roost line 363
Source documentation
Ballot compilation including explicit reset to desired output exponent. (Called only on successful gate, fallback zero separately).
```
abbrev roost (r:Knob)(f:Lyric)(v:ℕ) : Cog:= Lyric.choir r (reset f v)
```
lemma OAI.ExactDerandomization.Arena.Amber.onQ line 364
abbrev OAI.ExactDerandomization.Arena.Amber.snow line 370
lemma OAI.ExactDerandomization.Arena.Amber.steam line 371
abbrev OAI.ExactDerandomization.Arena.Song.provided line 391
def OAI.ExactDerandomization.Arena.Song.pleas line 392
lemma OAI.ExactDerandomization.Arena.Song.picked line 393
lemma OAI.ExactDerandomization.Arena.Song.park line 394
lemma OAI.ExactDerandomization.Arena.Song.parks line 397
lemma OAI.ExactDerandomization.Arena.Song.pinTrue line 400
lemma OAI.ExactDerandomization.Arena.Song.pinFalse line 404
abbrev OAI.ExactDerandomization.Arena.Song.ein line 410
Source documentation
Constant scalar polymer. fourth powers of rising
```
abbrev ein:= kohn 1
```
abbrev OAI.ExactDerandomization.Arena.Song.deuce line 411
abbrev OAI.ExactDerandomization.Arena.Song.divN line 412
def OAI.ExactDerandomization.Arena.Song.sQ line 413
def OAI.ExactDerandomization.Arena.Song.quat line 414
def OAI.ExactDerandomization.Arena.Song.takeF line 415
def OAI.ExactDerandomization.Arena.Song.faded line 416
def OAI.ExactDerandomization.Arena.Song.boostR line 418
def OAI.ExactDerandomization.Arena.Song.gammaR line 419
lemma OAI.ExactDerandomization.Arena.Song.Paint.divideF line 424
lemma OAI.ExactDerandomization.Arena.Song.Paint.between0 line 429
lemma OAI.ExactDerandomization.Arena.Song.Paint.quadrat line 431
lemma OAI.ExactDerandomization.Arena.Song.Paint.tapS line 433
lemma OAI.ExactDerandomization.Arena.Song.Paint.went line 436
lemma OAI.ExactDerandomization.Arena.Song.Paint.boosted line 440
lemma OAI.ExactDerandomization.Arena.Song.Paint.gammed line 443