CenterRouteExposure.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.CenterRouteExposure.routeFrom_congr_at line 16

Source documentation

Equality of all node decisions at two samples identifies their entire routes, even when the two decision functions have different parameter spaces.

theorem routeFrom_congr_at {ι : Type u_ι} {X : Type u_X} {Y : Type u_Y}
    (chooseX : List ι → X → ι) (chooseY : List ι → Y → ι)
    (x : X) (y : Y) (h : ∀ P, chooseX P x = chooseY P y)
    (n : ℕ) (P : List ι) :
    routeFrom chooseX n P x = routeFrom chooseY n P y := by
…

theorem OAI.Problem310.CenterRouteExposure.route_decision_congr_at line 26

Source documentation

The decision at every stage is also fixed by the node-decision data.

theorem route_decision_congr_at {ι : Type u_ι} {X : Type u_X} {Y : Type u_Y}
    (chooseX : List ι → X → ι) (chooseY : List ι → Y → ι)
    (x : X) (y : Y) (h : ∀ P, chooseX P x = chooseY P y)
    (n : ℕ) (P : List ι) :
    chooseX (routeFrom chooseX n P x) x =
      chooseY (routeFrom chooseY n P y) y := by
…

def OAI.Problem310.CenterRouteExposure.FirstDefaultAt line 36

Source documentation

The event that the first default occurs at a specified stage.

def FirstDefaultAt {ι : Type u_ι} {X : Type u_X} (choose : List ι → X → ι)
    (default : ι) (d k : ℕ) (P : List ι) (x : X) : Prop :=
…

theorem OAI.Problem310.CenterRouteExposure.firstDefaultAt_congr line 42

Source documentation

Full center exposure fixes whether a given stage is the first default.

theorem firstDefaultAt_congr {ι : Type u_ι} {X : Type u_X} {Y : Type u_Y}
    (chooseX : List ι → X → ι) (chooseY : List ι → Y → ι)
    (x : X) (y : Y) (h : ∀ P, chooseX P x = chooseY P y)
    (default : ι) (d k : ℕ) (P : List ι) :
    FirstDefaultAt chooseX default d k P x ↔
      FirstDefaultAt chooseY default d k P y := by
…

Mentions: OAI.Problem310.CenterRouteExposure.FirstDefaultAt

def OAI.Problem310.CenterRouteExposure.centerExposure line 53
Source documentation
The full deterministic center exposure: one bit for every selector table.
```
def centerExposure {M d : ℕ} (b : Node M d → Fin M → ℕ) (x : ℝ)
    (ω : SelectorTable b) : Node M d × Fin M → Bool :=
…
```
def OAI.Problem310.CenterRouteExposure.centerCompletion line 59
Source documentation
Complete any exposure assignment by setting all unexposed bits to false. This is only a deterministic representative of an atom, not a probability law.
```
def centerCompletion {M d : ℕ} (b : Node M d → Fin M → ℕ) (x : ℝ)
    (ξ : Node M d × Fin M → Bool) : SelectorTable b :=
…
```
theorem OAI.Problem310.CenterRouteExposure.centerExposure_completion line 64
theorem OAI.Problem310.CenterRouteExposure.centerExposure_surjective line 71
Source documentation
Every exposure assignment has a representative selector table.
```
theorem centerExposure_surjective {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) :
    Function.Surjective (centerExposure b x) :=
…
```
Mentions: OAI.Problem310.CenterRouteExposure.centerExposure

theorem OAI.Problem310.CenterRouteExposure.selectorValue_eq_of_centerExposure_eq line 78

Source documentation

Even the extended selector function is fixed by center exposure: invalid nodes use the same constant false value in both outcomes.

theorem selectorValue_eq_of_centerExposure_eq {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) {ω ω' : SelectorTable b}
    (h : centerExposure b x ω = centerExposure b x ω')
    (P : List (Child M)) (i : Fin M) :
    selectorValue b ω P i x = selectorValue b ω' P i x := by
…

Mentions: OAI.Problem310.CenterRouteExposure.centerExposure

def OAI.Problem310.CenterRouteExposure.centerChoice line 89
Source documentation
The actual first-success choice made by a selector table at a fixed center.
```
def centerChoice {M d : ℕ} (b : Node M d → Fin M → ℕ) (x : ℝ)
    (P : List (Child M)) (ω : SelectorTable b) : Child M :=
…
```
theorem OAI.Problem310.CenterRouteExposure.centerChoice_eq_of_centerExposure_eq line 93

theorem OAI.Problem310.CenterRouteExposure.centerRoute_eq_of_centerExposure_eq line 100

Source documentation

Every center route is constant on each full exposure atom.

theorem centerRoute_eq_of_centerExposure_eq {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) {ω ω' : SelectorTable b}
    (h : centerExposure b x ω = centerExposure b x ω')
    (n : ℕ) (P : List (Child M)) :
    routeFrom (centerChoice b x) n P ω = routeFrom (centerChoice b x) n P ω' :=
…

Mentions: OAI.Problem310.CenterRouteExposure.centerExposure, OAI.Problem310.CenterRouteExposure.centerChoice

theorem OAI.Problem310.CenterRouteExposure.centerRoute_decision_eq_of_centerExposure_eq line 108

Source documentation

The decision made at every center-route stage is constant on the atom.

theorem centerRoute_decision_eq_of_centerExposure_eq {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) {ω ω' : SelectorTable b}
    (h : centerExposure b x ω = centerExposure b x ω')
    (n : ℕ) (P : List (Child M)) :
    centerChoice b x (routeFrom (centerChoice b x) n P ω) ω =
      centerChoice b x (routeFrom (centerChoice b x) n P ω') ω' :=
…

Mentions: OAI.Problem310.CenterRouteExposure.centerExposure, OAI.Problem310.CenterRouteExposure.centerChoice

theorem OAI.Problem310.CenterRouteExposure.firstDefaultAt_centerCompletion line 117
Source documentation
First-default events can be defined entirely on the finite exposure space.
```
theorem firstDefaultAt_centerCompletion {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ω : SelectorTable b)
    (k : ℕ) (P : List (Child M)) :
    FirstDefaultAt (centerChoice b x) (Fin.last M) d k P ω ↔
      FirstDefaultAt (centerChoice b x) (Fin.last M) d k P
        (centerCompletion b x (centerExposure b x ω)) := by
…
```
Mentions: OAI.Problem310.CenterRouteExposure.FirstDefaultAt, OAI.Problem310.CenterRouteExposure.centerChoice, OAI.Problem310.CenterRouteExposure.centerCompletion, OAI.Problem310.CenterRouteExposure.centerExposure

theorem OAI.Problem310.CenterRouteExposure.firstDefaultData_on_atom line 129

Source documentation

A good exposure atom has one fixed first-default stage and node, uniformly for every completion of all unexposed selector coordinates.

theorem firstDefaultData_on_atom {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ξ : Node M d × Fin M → Bool)
    (hgood : ∃ k < d, centerChoice b x
      (routeFrom (centerChoice b x) k [] (centerCompletion b x ξ))
        (centerCompletion b x ξ) = Fin.last M) :
    ∃ k : ℕ, ∃ U : List (Child M), k < d ∧
      ∀ ω : SelectorTable b, centerExposure b x ω = ξ →
        routeFrom (centerChoice b x) k [] ω = U ∧
        FirstDefaultAt (centerChoice b x) (Fin.last M) d k [] ω := by
…

Mentions: OAI.Problem310.CenterRouteExposure.centerChoice, OAI.Problem310.CenterRouteExposure.centerCompletion, OAI.Problem310.CenterRouteExposure.centerExposure, OAI.Problem310.CenterRouteExposure.FirstDefaultAt

theorem OAI.Problem310.CenterRouteExposure.firstDefaultNode_on_atom line 151

Source documentation

Version of the atomwise first-default witness with the actual bounded node and stage types required to index the finite selector tables and window data.

theorem firstDefaultNode_on_atom {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ξ : Node M d × Fin M → Bool)
    (hgood : ∃ k < d, centerChoice b x
      (routeFrom (centerChoice b x) k [] (centerCompletion b x ξ))
        (centerCompletion b x ξ) = Fin.last M) :
    ∃ k : Fin d, ∃ U : Node M d, U.val.length = k.val ∧
      ∀ ω : SelectorTable b, centerExposure b x ω = ξ →
        routeFrom (centerChoice b x) k.val [] ω = U.val ∧
        FirstDefaultAt (centerChoice b x) (Fin.last M) d k.val [] ω := by
…

def OAI.Problem310.CenterRouteExposure.GoodExposure line 168
Source documentation
The good atoms are those whose (equivalently, every) center route has a default.
```
def GoodExposure {M d : ℕ} (b : Node M d → Fin M → ℕ) (x : ℝ)
    (ξ : Node M d × Fin M → Bool) : Prop :=
…
```
theorem OAI.Problem310.CenterRouteExposure.goodExposure_centerExposure_iff line 175
Source documentation
The finite-atom good predicate is exactly the actual center-path default event.
```
theorem goodExposure_centerExposure_iff {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ω : SelectorTable b) :
    GoodExposure b x (centerExposure b x ω) ↔
      ∃ k < d, centerChoice b x (routeFrom (centerChoice b x) k [] ω) ω = Fin.last M := by
…
```
Mentions: OAI.Problem310.CenterRouteExposure.GoodExposure, OAI.Problem310.CenterRouteExposure.centerExposure, OAI.Problem310.CenterRouteExposure.centerChoice
theorem OAI.Problem310.CenterRouteExposure.badExposure_centerExposure_iff line 189
Source documentation
This is the event identity used to transport the no-default probability estimate to the bad atoms of the full center-exposure partition.
```
theorem badExposure_centerExposure_iff {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ω : SelectorTable b) :
    ¬ GoodExposure b x (centerExposure b x ω) ↔
      ∀ k < d, centerChoice b x (routeFrom (centerChoice b x) k [] ω) ω ≠ Fin.last M := by
…
```
Mentions: OAI.Problem310.CenterRouteExposure.GoodExposure, OAI.Problem310.CenterRouteExposure.centerExposure, OAI.Problem310.CenterRouteExposure.centerChoice