ScheduledTopology.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.DilutedSpinGlass.ReducedTopology line 14
Source documentation
Finite rooted topology with unary vertices suppressed. Children have fixed distinct positions, hence leaves remain labeled throughout realization.
```
inductive ReducedTopology : Type
  | leaf : ReducedTopology
  | node (k : ℕ+) (hk : 2 ≤ (k:ℕ)) (C : Fin k → ReducedTopology) : ReducedTopology

namespace ReducedTopology
```
def OAI.DilutedSpinGlass.ReducedTopology.Vertex line 20
def OAI.DilutedSpinGlass.ReducedTopology.Leaf line 24
instance OAI.DilutedSpinGlass.ReducedTopology.vertexFintype line 28
instance OAI.DilutedSpinGlass.ReducedTopology.leafFintype line 34

def OAI.DilutedSpinGlass.ReducedTopology.Admissible line 41

Source documentation

Strict ancestry and the genuine terminal grid horizon.

def Admissible : (S : ReducedTopology) → (S.Vertex → ℕ) → ℕ → ℕ → Prop
  | .leaf, _, _, _ => True
  | .node _ _ C, q, lo, hi =>
    lo ≤ q none ∧ q none < hi ∧
      ∀ i, Admissible (C i) (fun v => q (some ⟨i,v⟩)) (q none+1) hi

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q

lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_mono_lower line 47
lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_lower line 53
lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_upper line 62
def OAI.DilutedSpinGlass.ReducedTopology.realize line 74
Source documentation
Expand a depth assignment into the actual leveled prescribed tree. Outside admissible assignments this is still total; no such assignment is used in the geometry or analytic theorems below.
```
def realize : (r : ℕ) → (d : ℕ) → (S : ReducedTopology) →
    (S.Vertex → ℕ) → PrescribedTree r
  | 0, _, _, _ => .leaf
  | r+1, d, .leaf, q => PrescribedTree.unary (realize r (d+1) .leaf q)
  | r+1, d, .node k hk C, q =>
    if d < q none then PrescribedTree.unary (realize r (d+1) (.node k hk C) q)
    else .node k (fun i => realize r (d+1) (C i) (fun v => q (some ⟨i,v⟩)))
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.unary
lemma OAI.DilutedSpinGlass.ReducedTopology.realize_leaves line 82
theorem OAI.DilutedSpinGlass.ReducedTopology.realize_branchingCount line 112
Source documentation
Actual vertex multiplicities, with assigned absolute depths. Aligned copies may repeat a coordinate but never merge their branching vertices.
```
theorem realize_branchingCount (r d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (h : Admissible S q d (d+r)) (P : ℕ → Prop) :
    PrescribedTree.branchingCount (realize r d S q) (fun u => P (d+u)) =
      ∑ v : S.Vertex, if P (q v) then 1 else 0 := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.ReducedTopology.realize