EarliestChildDepth.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ReducedTopology.earliestChildDepth line 15
Source documentation
First available proper-child branching depth, with terminal value L when every proper child is a leaf. This handles the induction endpoint.
```
noncomputable def earliestChildDepth (C : ι → ReducedTopology)
    (q : (j : ι) → (C j).Vertex → Fin L) : ℕ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex
lemma OAI.DilutedSpinGlass.ReducedTopology.earliestChildDepth_le_horizon line 20
lemma OAI.DilutedSpinGlass.ReducedTopology.earliestChildDepth_le line 25
lemma OAI.DilutedSpinGlass.ReducedTopology.lt_earliestChildDepth line 33