IntervalFamily.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

A concrete finite family of separated internal dyadic intervals

At depth 2D use the cells with indices 2i+1. The bound 2D < 2^(2D) leaves room at the right endpoint. Each adjacent selected pair has a positive gap. The finite occurrence type remembers parents and their children without requiring an injectivity premise for the family.

def OAI.ThompsonNonamenability.selectedInterval line 22
Source documentation
The actual ith selected dyadic cell at common depth 2D.
```
def selectedInterval (D : ℕ) (i : Fin D) : BasicInterval where
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.selectedInterval_internal line 29
theorem OAI.ThompsonNonamenability.selectedInterval_before line 43
def OAI.ThompsonNonamenability.StrictlySeparated line 53
Source documentation
Strict separation permits either orientation and always has a positive gap.
```
def StrictlySeparated (I J : BasicInterval) : Prop := I.Before J ∨ J.Before I
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.StrictlySeparated.symm line 55
theorem OAI.ThompsonNonamenability.selectedInterval_separated line 58
theorem OAI.ThompsonNonamenability.selected_siblings_separated line 64
theorem OAI.ThompsonNonamenability.selected_child_parent_separated line 73
Source documentation
A descendant is separated from every parent except its own parent.
```
theorem selected_child_parent_separated {D : ℕ} (i j k : Fin D) (hki : k ≠ i) :
    StrictlySeparated ((selectedInterval D i).comp (selectedInterval D j))
      (selectedInterval D k) := by
…
```
Mentions: OAI.ThompsonNonamenability.StrictlySeparated, OAI.ThompsonNonamenability.selectedInterval
abbrev OAI.ThompsonNonamenability.IntervalIndex line 81
def OAI.ThompsonNonamenability.familyInterval line 84
Source documentation
Actual parent and second-generation intervals indexed by their occurrences.
```
def familyInterval (D : ℕ) : IntervalIndex D → BasicInterval
  | .inl i => selectedInterval D i
  | .inr (i, j) => (selectedInterval D i).comp (selectedInterval D j)
```
Mentions: OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.selectedInterval
theorem OAI.ThompsonNonamenability.familyInterval_internal line 88
def OAI.ThompsonNonamenability.intervalFamily line 96
Source documentation
The actual finite interval set used by the single admissibility condition.
```
def intervalFamily (D : ℕ) : Finset BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.familyInterval_mem line 99
def OAI.ThompsonNonamenability.firstIndex line 103
def OAI.ThompsonNonamenability.secondIndex line 106
theorem OAI.ThompsonNonamenability.reference_before line 109