HostSamplingCompatibility.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of the path sampler and protected-cell sampler

The quotient/remainder formula and finProdFinEquiv select the same coordinate, identifying path samples with the uniform-fiber sampler.

theorem OAI.Problem348.TreeSampling.atLevel_eq_mixFin line 17
Source documentation
The equivalence-based and arithmetic mixers select identical coordinates.
```
theorem atLevel_eq_mixFin (h i : ℕ) (hi : i ≤ h) (z u : Fin (2 ^ h)) :
    atLevel h i hi z u = SampledPath.mixFin h i hi z u := by
…
```
Mentions: OAI.Problem348.TreeSampling.atLevel, OAI.Problem348.SampledPath.mixFin
theorem OAI.Problem348.Construction.HostSampling.coordinate_path_position line 29
Source documentation
An actual sampled variable path point is selected by the marginal sampler.
```
theorem coordinate_path_position (h i : ℕ) (hi : i ≤ h) (sign : Bool)
    (z u : Fin (2 ^ h)) :
    coordinate z u (HostSampledPath.position h i hi sign z u) =
      offset (HostSampledPath.position h i hi sign z u) := by
…
```
Mentions: OAI.Problem348.Construction.HostSampling.coordinate, OAI.Problem348.HostSampledPath.position, OAI.Problem348.Construction.HostSampling.offset
theorem OAI.Problem348.Construction.HostSampling.coordinate_anchor line 42
Source documentation
Anchor representatives use the corresponding independent axis seed.
```
@[simp] theorem coordinate_anchor (h : ℕ) (t : Mode h) (v : Fin 64)
    (z u : Fin (2 ^ h)) :
    coordinate z u (Sum.inl (t, v, u)) = offset (Sum.inl (t, v, u)) := rfl
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.HostSampling.coordinate, OAI.Problem348.Construction.HostSampling.offset
theorem OAI.Problem348.Construction.HostSampling.coordinate_path_dummy line 47
Source documentation
The selected dummy position uses the same independent axis seed.
```
@[simp] theorem coordinate_path_dummy (h : ℕ) (z u : Fin (2 ^ h)) :
    coordinate z u (HostSampledPath.dummy h u) =
      offset (HostSampledPath.dummy h u) := rfl
```
Mentions: OAI.Problem348.Construction.HostSampling.coordinate, OAI.Problem348.HostSampledPath.dummy, OAI.Problem348.Construction.HostSampling.offset
theorem OAI.Problem348.Construction.HostSampling.selected_path_positions line 53
Source documentation
Every pair of path samples, not just the protected pairs, is selected. The two axes use different offset seeds but the same leaf seed.
```
theorem selected_path_positions (h i j : ℕ) (hi : i ≤ h) (hj : j ≤ h)
    (s t : Bool) (z u v : Fin (2 ^ h)) :
    Selected (z, u, v) (HostSampledPath.position h i hi s z u)
      (HostSampledPath.position h j hj t z v) := by
…
```
Mentions: OAI.Problem348.Construction.HostSampling.Selected, OAI.Problem348.HostSampledPath.position
theorem OAI.Problem348.Construction.HostSampling.protected_selected_path_anchor line 61
Source documentation
A path-row / selected-anchor-column pair is a selected protected cell.
```
theorem protected_selected_path_anchor (h i : ℕ) (hi : i ≤ h) (sign : Bool)
    (t : Mode h) (a : Fin 64) (z u v : Fin (2 ^ h)) :
    Protected (HostSampledPath.position h i hi sign z u) (Sum.inl (t, a, v)) ∧
      Selected (z, u, v) (HostSampledPath.position h i hi sign z u)
        (Sum.inl (t, a, v)) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.HostSampledPath.position, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.protected_selected_anchor_path line 70
Source documentation
A selected-anchor-row / path-column pair is a selected protected cell.
```
theorem protected_selected_anchor_path (h i : ℕ) (hi : i ≤ h) (sign : Bool)
    (t : Mode h) (a : Fin 64) (z u v : Fin (2 ^ h)) :
    Protected (Sum.inl (t, a, u)) (HostSampledPath.position h i hi sign z v) ∧
      Selected (z, u, v) (Sum.inl (t, a, u))
        (HostSampledPath.position h i hi sign z v) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.HostSampledPath.position, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.rowChosen_path line 79
Source documentation
Direct row-field adapter for the geometric guarded-path certificate.
```
theorem rowChosen_path {h n : ℕ} (er : Position h ≃ Fin n)
    (i : ℕ) (hi : i ≤ h) (sign : Bool) (s : TreeSampling.Seeds (2 ^ h)) :
    RowChosen er s (er (HostSampledPath.position h i hi sign s.1 s.2.1)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.Construction.HostSampling.RowChosen, OAI.Problem348.HostSampledPath.position
theorem OAI.Problem348.Construction.HostSampling.colChosen_path line 86
Source documentation
Direct column-field adapter for the geometric guarded-path certificate.
```
theorem colChosen_path {h n : ℕ} (ec : Position h ≃ Fin n)
    (i : ℕ) (hi : i ≤ h) (sign : Bool) (s : TreeSampling.Seeds (2 ^ h)) :
    ColChosen ec s (ec (HostSampledPath.position h i hi sign s.1 s.2.2)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.Construction.HostSampling.ColChosen, OAI.Problem348.HostSampledPath.position
theorem OAI.Problem348.Construction.HostSampling.rowChosen_path_dummy line 92
theorem OAI.Problem348.Construction.HostSampling.colChosen_path_dummy line 98
theorem OAI.Problem348.Construction.HostSampling.rowChosen_path_anchor line 104
theorem OAI.Problem348.Construction.HostSampling.colChosen_path_anchor line 110
theorem OAI.Problem348.Construction.HostSampling.protected_path_roots line 117
Source documentation
Both sampled roots belong to protected classes, regardless of sign.
```
theorem protected_path_roots (h : ℕ) (s t : Bool) (z u v : Fin (2 ^ h)) :
    Protected (HostSampledPath.position h 0 (Nat.zero_le h) s z u)
      (HostSampledPath.position h 0 (Nat.zero_le h) t z v) := by
…
```
Mentions: OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.HostSampledPath.position