FiniteActivityBridge.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite indices for the sparse-activity obstruction

Internal nodes are indexed by their depth and finite sequence of child indices. Absence of a sparse active node bounds the cardinality of active leaves, which controls the Fourier mass.

abbrev OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode line 21
Source documentation
All internal nodes of a complete tree of depth h.
```
abbrev InternalNode (α : Type*) (h : ℕ) := Σ j : Fin h, Fin (j : ℕ) → α
```
def OAI.TreeEdit.BinaryLower.FiniteActivity.sparseNode line 24
Source documentation
A bad node is active but has fewer than b active children.
```
def sparseNode {α : Type*} [Fintype α] {h : ℕ}
    (active : List α → Prop) (b : ℕ) (v : InternalNode α h) : Prop :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode
theorem OAI.TreeEdit.BinaryLower.FiniteActivity.dense_of_no_sparse line 31
Source documentation
Absence of bad nodes in the finite node indexing gives the full active leaf cardinality lower bound.
```
theorem dense_of_no_sparse {α : Type*} [Fintype α]
    (active : List α → Prop) (b h : ℕ)
    (hroot : active []) (hno : ¬ ∃ v : InternalNode α h, sparseNode active b v) :
    b ^ h ≤ (Finset.univ.filter fun f : Fin h → α => active (List.ofFn f)).card := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteActivity.sparseNode
def OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse line 50
Source documentation
Character formulation of the sparse-node predicate.
```
def characterSparse {α G : Type*} [Fintype α] [AddCommGroup G] {h : ℕ}
    (w : List α → G) (b : ℕ) (v : InternalNode α h) (χ : AddChar G ℂ) : Prop :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode
theorem OAI.TreeEdit.BinaryLower.FiniteActivity.character_dense_of_no_sparse line 57
Source documentation
For a root-active character that escapes every sparse-node test, the number of active terminal vectors is at least the branching factor to the height.
```
theorem character_dense_of_no_sparse {α G : Type*}
    [Fintype α] [AddCommGroup G]
    (w : List α → G) (b h : ℕ) (χ : AddChar G ℂ)
    (hroot : χ (w []) ≠ 1)
    (hno : ¬ ∃ v : InternalNode α h, characterSparse w b v χ) :
    (b : ℝ) ^ h ≤
      ((Finset.univ.filter fun f : Fin h → α => χ (w (List.ofFn f)) ≠ 1).card : ℝ) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse

theorem OAI.TreeEdit.BinaryLower.FiniteActivity.character_dense_of_leaf_generators line 70

Source documentation

Adapter to the actual cyclic coordinate generators used by the spectral leaf tests. The only structural identity needed here is w_leaf = e_leaf.

theorem character_dense_of_leaf_generators {α G : Type*}
    [Fintype α] [AddCommGroup G]
    (w : List α → G) (b h : ℕ) (e : (Fin h → α) → G) (χ : AddChar G ℂ)
    (hgen : ∀ f : Fin h → α, w (List.ofFn f) = e f)
    (hroot : χ (w []) ≠ 1)
    (hno : ¬ ∃ v : InternalNode α h, characterSparse w b v χ) :
    (b : ℝ) ^ h ≤
      ((Finset.univ.filter fun f : Fin h → α => χ (e f) ≠ 1).card : ℝ) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse

theorem OAI.TreeEdit.BinaryLower.FiniteActivity.internal_node_budget line 84
Source documentation
Exact sum of the reciprocal-subtree budgets over the finite internal-node index. The result is independent of the branching width.
```
theorem internal_node_budget (m h : ℕ) (hm : m ≠ 0) (C : ℝ) :
    (∑ v : InternalNode (Fin m) h, C / (m : ℝ) ^ (v.1 : ℕ)) = h * C := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode
theorem OAI.TreeEdit.BinaryLower.FiniteActivity.leaf_budget line 97
Source documentation
The leaf-coordinate edit budgets sum to exactly the word length.
```
theorem leaf_budget (m h : ℕ) (hm : m ≠ 0) (M : ℝ) :
    (∑ _f : Fin h → Fin m, M / (m : ℝ) ^ h) = M := by
…
```