QueryTree.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.CubeShuffle.QueryTree line 15
Source documentation
A finite adaptive experiment. A force instruction aborts on the wrong bit; it carries likelihood-ratio weight 2 on success. Ordinary queries have no cost. Freshness is a theorem hypothesis BELOW ON THE ACTUAL QUERY TREE, not an independence assumption about a subsequently selected event.
```
inductive QueryTree (ι : Type*)
  | reject : QueryTree ι
  | accept : QueryTree ι
  | branch (i : ι) (zero one : QueryTree ι) : QueryTree ι
  | force (i : ι) (b : Bool) (next : QueryTree ι) : QueryTree ι

namespace QueryTree

variable {ι : Type*} [DecidableEq ι]
```
def OAI.CubeShuffle.QueryTree.queries line 25

def OAI.CubeShuffle.QueryTree.Fresh line 32

Source documentation

No coin is requested twice along any branch of the experiment.

def Fresh : QueryTree ι → Prop
  | reject => True
  | accept => True
  | branch i zero one => i ∉ queries zero ∧ i ∉ queries one ∧ Fresh zero ∧ Fresh one
  | force i _ next => i ∉ queries next ∧ Fresh next

Mentions: OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.QueryTree.queries

def OAI.CubeShuffle.QueryTree.weighted line 38
lemma OAI.CubeShuffle.QueryTree.weighted_nonneg line 45
lemma OAI.CubeShuffle.QueryTree.weighted_congr line 52
lemma OAI.CubeShuffle.QueryTree.weighted_flip_of_not_mem line 67
lemma OAI.CubeShuffle.QueryTree.mean_weighted_le_one line 75
Source documentation
Sequential forcing identity/inequality. Its weight is determined by the realized trace; there is no conditioning on a favorable choice of certificate.
```
lemma mean_weighted_le_one [Fintype ι] (T : QueryTree ι) (hT : T.Fresh) :
    finiteMean T.weighted ≤ 1 := by
…
```
Mentions: OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.finiteMean
def OAI.CubeShuffle.QueryTree.succeeds line 109

def OAI.CubeShuffle.QueryTree.charge line 116

Source documentation

Number of successful forced fresh-bit queries along the realized trace.

def charge : QueryTree ι → (ι → Bool) → ℕ
  | reject, _ => 0
  | accept, _ => 0
  | branch i zero one, ω => if ω i then charge one ω else charge zero ω
  | force i b next, ω => if ω i = b then charge next ω + 1 else 0

omit [DecidableEq ι] in

Mentions: OAI.CubeShuffle.QueryTree

lemma OAI.CubeShuffle.QueryTree.weighted_eq line 123
lemma OAI.CubeShuffle.QueryTree.success_probability_le line 140
Source documentation
Acceptance probability is at most 2^(-K) whenever every accepted trace contains at least K forced fresh bits; unsuccessful shorter traces need not make K queries. This is precisely the stopping-threshold issue in the fixed certificate proof (10-network.tex:84).
```
lemma success_probability_le [Fintype ι] (T : QueryTree ι) (hT : T.Fresh)
    (K : ℕ) (hK : ∀ ω, T.succeeds ω = true → K ≤ T.charge ω) :
    finiteMean (fun ω => if T.succeeds ω then (1 : ℝ) else 0) ≤ 1 / (2 : ℝ) ^ K := by
…
```
Mentions: OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.finiteMean

def OAI.CubeShuffle.QueryTree.memo line 166

Source documentation

Eliminate repeated queries against an explicit exposure record. Repeated forced bits test compatibility but acquire no likelihood-ratio factor.

def memo : QueryTree ι → Finset ι → (ι → Bool) → QueryTree ι
  | reject, _, _ => reject
  | accept, _, _ => accept
  | branch i zero one, R, η =>
      if i ∈ R then (if η i then memo one R η else memo zero R η) else
      branch i (memo zero (insert i R) (Function.update η i false))
        (memo one (insert i R) (Function.update η i true))
  | force i b next, R, η =>
      if i ∈ R then (if η i = b then memo next R η else reject) else
      force i b (memo next (insert i R) (Function.update η i b))

Mentions: OAI.CubeShuffle.QueryTree

lemma OAI.CubeShuffle.QueryTree.memo_queries_disjoint line 177
lemma OAI.CubeShuffle.QueryTree.memo_fresh line 200
lemma OAI.CubeShuffle.QueryTree.update_agrees line 226
lemma OAI.CubeShuffle.QueryTree.memo_succeeds line 237

def OAI.CubeShuffle.QueryTree.freshCharge line 267

Source documentation

Forced bits counted only when fresh; ordinary path queries insert their bits into the same record, so subsequent closures cannot charge them twice.

def freshCharge : QueryTree ι → Finset ι → (ι → Bool) → ℕ
  | reject, _, _ => 0
  | accept, _, _ => 0
  | branch i zero one, R, ω => if ω i then freshCharge one (insert i R) ω else freshCharge zero (insert i R) ω
  | force i b next, R, ω => if ω i = b then
      freshCharge next (insert i R) ω + (if i ∈ R then 0 else 1) else 0

Mentions: OAI.CubeShuffle.QueryTree

lemma OAI.CubeShuffle.QueryTree.memo_charge line 274
lemma OAI.CubeShuffle.QueryTree.mean_freshCharge_le_one line 304
Source documentation
Adaptive weighted closing constraints remain valid with arbitrary repeated ordinary/closing queries, after accounting exactly for exposed coins.
```
lemma mean_freshCharge_le_one [Fintype ι] (T : QueryTree ι) :
    finiteMean (fun ω : ι → Bool =>
      if T.succeeds ω then (2:ℝ) ^ T.freshCharge ∅ ω else 0) ≤ 1 := by
…
```
Mentions: OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.finiteMean

def OAI.CubeShuffle.QueryTree.followPath line 325

Source documentation

Query just the switches on one actual butterfly route, then pass its endpoint to a continuation. The index map permits parallel sub-butterflies.

def followPath : (d : ℕ) → (SwitchIndex d → ι) → Card d →
    (Card d → QueryTree ι) → QueryTree ι
  | 0, _, x, k => k x
  | d + 1, e, x, k => followPath d (fun i => e (Sum.inr (x 0,i))) (Fin.tail x)
      (fun y => branch (e (Sum.inl y))
        (k (Fin.cons (Bool.xor (x 0) false) y))
        (k (Fin.cons (Bool.xor (x 0) true) y)))

omit [DecidableEq ι] in

Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card, OAI.CubeShuffle.QueryTree

lemma OAI.CubeShuffle.QueryTree.followPath_succeeds line 334
lemma OAI.CubeShuffle.QueryTree.followPath_charge line 350
def OAI.CubeShuffle.QueryTree.forceList line 384
Source documentation
Force a finite list of coin requirements; compatibility with previous ordinary or forced queries is handled by memo.
```
def forceList : List ι → (ι → Bool) → QueryTree ι → QueryTree ι
  | [], _, k => k
  | i :: L, v, k => force i (v i) (forceList L v k)

omit [DecidableEq ι] in
```
Mentions: OAI.CubeShuffle.QueryTree
lemma OAI.CubeShuffle.QueryTree.forceList_succeeds line 389
lemma OAI.CubeShuffle.QueryTree.forceList_charge line 398

def OAI.CubeShuffle.QueryTree.staleCharge line 433

Source documentation

The number of forced queries already determined by earlier exposures.

def staleCharge : QueryTree ι → Finset ι → (ι → Bool) → ℕ
  | reject, _, _ => 0
  | accept, _, _ => 0
  | branch i zero one, R, ω => if ω i then staleCharge one (insert i R) ω
      else staleCharge zero (insert i R) ω
  | force i b next, R, ω => if ω i = b then
      staleCharge next (insert i R) ω + (if i ∈ R then 1 else 0) else 0

Mentions: OAI.CubeShuffle.QueryTree

lemma OAI.CubeShuffle.QueryTree.fresh_add_stale line 441
lemma OAI.CubeShuffle.QueryTree.followPath_raw_charge line 456
lemma OAI.CubeShuffle.QueryTree.forceList_raw_charge line 473
def OAI.CubeShuffle.QueryTree.closePath line 485
Source documentation
A closing path has a specified endpoint rather than an adaptively chosen one. It issues exactly the route's coin requirements.
```
noncomputable def closePath (d : ℕ) (x y : Card d) (k : QueryTree (SwitchIndex d)) :
    QueryTree (SwitchIndex d) :=
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.SwitchIndex
lemma OAI.CubeShuffle.QueryTree.closePath_succeeds line 489
lemma OAI.CubeShuffle.QueryTree.closePath_raw_charge line 497
lemma OAI.CubeShuffle.QueryTree.closePath_fresh_charge line 504
lemma OAI.CubeShuffle.QueryTree.closePath_stale_charge line 513

def OAI.CubeShuffle.QueryTree.seekCycle line 527

Source documentation

Inspect one proposed length-(r+1) cycle. Every queried input must be in S and must not have appeared in an earlier slot or earlier in this cycle.

noncomputable def seekCycle (d : ℕ) (S : Finset (Card d)) (a : Card d) :
    ℕ → Card d → Finset (Card d) → (Finset (Card d) → QueryTree (SwitchIndex d)) →
      QueryTree (SwitchIndex d)
  | 0, x, V, k => if x ∈ S ∧ x ∉ V then closePath d x a (k (insert x V)) else reject
  | r + 1, x, V, k => if x ∈ S ∧ x ∉ V then followPath d id x
      (fun y => seekCycle d S a r y (insert x V) k) else reject

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.QueryTree.closePath, OAI.CubeShuffle.QueryTree.followPath

lemma OAI.CubeShuffle.QueryTree.seekCycle_raw_charge line 534
def OAI.CubeShuffle.QueryTree.seekCycles line 556
Source documentation
Distinguishable cycle slots, with each requested length encoded as r+1. Later factorial-moment counting divides by precisely these rotation counts.
```
noncomputable def seekCycles (d : ℕ) (S : Finset (Card d)) :
    List (Card d × ℕ) → Finset (Card d) → QueryTree (SwitchIndex d)
  | [], _ => accept
  | (a,r) :: L, V => seekCycle d S a r a V (fun V => seekCycles d S L V)
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.QueryTree.seekCycle
lemma OAI.CubeShuffle.QueryTree.seekCycles_raw_charge line 561
lemma OAI.CubeShuffle.QueryTree.cycles_weighted_success line 578
Source documentation
The actual fixed-start weighted exploration inequality in FAC.3. The stale charge counts exposed closing-path switches exactly, not a postulated conditional-independence bound. Failure includes repeats, short cycles and visiting outside the marked subset, and can occur at ANY earlier query.
```
lemma cycles_weighted_success (d : ℕ) (S : Finset (Card d)) (L : List (Card d × ℕ)) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
      if (seekCycles d S L ∅).succeeds ω then
        ((2:ℝ)^d)^L.length / (2:ℝ)^(seekCycles d S L ∅).staleCharge ∅ ω else 0) ≤ 1 := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.QueryTree.seekCycles, OAI.CubeShuffle.QueryTree.succeeds, OAI.CubeShuffle.QueryTree.staleCharge