HostRootLeaf.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Root bits and shared-leaf entries of the exact canonical construction.

theorem OAI.Problem348.Construction.node_eq_zero_of_depth_zero line 10
Source documentation
At the root, all uniform coordinates name node zero.
```
theorem node_eq_zero_of_depth_zero {h : ℕ} (v : VariablePosition h)
    (hv : depth v = 0) : node v = 0 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.node
theorem OAI.Problem348.Construction.depth_root_plus line 17
Source documentation
The even class zero is the plus root.
```
@[simp] theorem depth_root_plus {h : ℕ} (x : Fin (2 ^ h)) :
    depth ((0 : Fin (2 * h + 1)), x) = 0 := by
…
```
Mentions: OAI.Problem348.Construction.depth
theorem OAI.Problem348.Construction.plus_root_plus line 21
theorem OAI.Problem348.Construction.variableEntry_root_plus line 26
Source documentation
All entries between the two plus-root blocks are one.
```
theorem variableEntry_root_plus {h : ℕ} (x y : Fin (2 ^ h)) :
    variableEntry ((0 : Fin (2 * h + 1)), x)
      ((0 : Fin (2 * h + 1)), y) = true := by
…
```
Mentions: OAI.Problem348.Construction.variableEntry
theorem OAI.Problem348.Construction.depth_root_minus line 36
Source documentation
Class one is the minus root when the tree has positive height.
```
@[simp] theorem depth_root_minus {h : ℕ} (hh : 1 ≤ h) (x : Fin (2 ^ h)) :
    depth ((⟨1, by omega⟩ : Fin (2 * h + 1)), x) = 0 := by
…
```
Mentions: OAI.Problem348.Construction.depth
theorem OAI.Problem348.Construction.plus_root_minus line 40

theorem OAI.Problem348.Construction.variableEntry_root_minus line 45

Source documentation

All entries between the minus-root blocks are zero.

theorem variableEntry_root_minus {h : ℕ} (hh : 1 ≤ h) (x y : Fin (2 ^ h)) :
    variableEntry ((⟨1, by omega⟩ : Fin (2 * h + 1)), x)
      ((⟨1, by omega⟩ : Fin (2 * h + 1)), y) = false := by
…

Mentions: OAI.Problem348.Construction.variableEntry

theorem OAI.Problem348.Construction.depth_shared_leaf line 55
Source documentation
The last class is the single shared leaf class.
```
@[simp] theorem depth_shared_leaf {h : ℕ} (x : Fin (2 ^ h)) :
    depth (Fin.last (2 * h), x) = h := by
…
```
Mentions: OAI.Problem348.Construction.depth
theorem OAI.Problem348.Construction.node_shared_leaf line 59
theorem OAI.Problem348.Construction.variableEntry_shared_leaf line 64
Source documentation
Entry values at shared leaves, including the minus diagonal.
```
theorem variableEntry_shared_leaf {h : ℕ} (x y : Fin (2 ^ h)) :
    variableEntry (Fin.last (2 * h), x) (Fin.last (2 * h), y) =
      decide (x.val ≤ y.val) := by
…
```
Mentions: OAI.Problem348.Construction.variableEntry

theorem OAI.Problem348.Construction.host_root_plus line 70

Source documentation

Exact unchanged plus root bit on the full host.

theorem host_root_plus {h : ℕ} (x y : Fin (2 ^ h)) :
    host (Sum.inr (Sum.inl ((0 : Fin (2 * h + 1)), x)))
      (Sum.inr (Sum.inl ((0 : Fin (2 * h + 1)), y))) = true :=
…

Mentions: OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.host_root_minus line 76

Source documentation

Exact unchanged minus root bit on the full host.

theorem host_root_minus {h : ℕ} (hh : 1 ≤ h) (x y : Fin (2 ^ h)) :
    host (Sum.inr (Sum.inl ((⟨1, by omega⟩ : Fin (2 * h + 1)), x)))
      (Sum.inr (Sum.inl ((⟨1, by omega⟩ : Fin (2 * h + 1)), y))) = false :=
…

Mentions: OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.host_shared_leaf_diagonal line 82

Source documentation

The shared-leaf diagonal consists of ones.

theorem host_shared_leaf_diagonal {h : ℕ} (x : Fin (2 ^ h)) :
    host (Sum.inr (Sum.inl (Fin.last (2 * h), x)))
      (Sum.inr (Sum.inl (Fin.last (2 * h), x))) = true := by
…

Mentions: OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.variableEntry_root_plus_of_atLevel line 88
Source documentation
Constructor-free form of the positive root entry.
```
theorem variableEntry_root_plus_of_atLevel {h : ℕ} (hh : 1 ≤ h)
    (r c : VariablePosition h) (hr : AtLevel 0 true r) (hc : AtLevel 0 true c) :
    variableEntry r c = true := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.Construction.variableEntry
theorem OAI.Problem348.Construction.variableEntry_root_minus_of_atLevel line 98
Source documentation
Constructor-free form of the negative root entry.
```
theorem variableEntry_root_minus_of_atLevel {h : ℕ} (hh : 1 ≤ h)
    (r c : VariablePosition h) (hr : AtLevel 0 false r) (hc : AtLevel 0 false c) :
    variableEntry r c = false := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.Construction.variableEntry
theorem OAI.Problem348.Construction.node_eq_coordinate_of_leaf line 108
Source documentation
Every shared-leaf node is its coordinate.
```
theorem node_eq_coordinate_of_leaf {h : ℕ} (r : VariablePosition h)
    (hr : depth r = h) : node r = r.2.val := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.node
theorem OAI.Problem348.Construction.variableEntry_leaf_of_depth line 113
Source documentation
Constructor-free shared-leaf threshold formula.
```
theorem variableEntry_leaf_of_depth {h : ℕ} (r c : VariablePosition h)
    (hr : depth r = h) (hc : depth c = h) :
    variableEntry r c = decide (r.2.val ≤ c.2.val) := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.variableEntry