PhysicalGridMultileaf.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.UniversalDictionary.physical_grid_root_multileaf line 20
Source documentation
Physical specialization of the non-singleton induction step. The only signed history is literally the covariance controlled by joint_grid_selection; all other errors are the single-copy shift error and proper-child root energies. The evaluation depth is positive, as it is on the regular depth domain.
```
theorem physical_grid_root_multileaf (M : Model p) (θB hB : ℝ) (N H r d : ℕ)
    (u : Spec (H+1+1+r+1+d) × ℕ → ℝ)
    (k : ℕ+) (hk : 2≤(k:ℕ)) (a : α) (C : Fin k → ReducedTopology)
    (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+(d+1))) (ha : (Q a).val=r+1+(d+1))
    (had : ∀ j, ReducedTopology.Admissible (C j) (fun v => (Q (e j v)).val) (r+1+(d+1)+1) (r+1+(d+1)+1+H))
    {η : ℝ} (hlarge : 1<η*(H+1+1+r+1+(d+1):ℕ)) (hr : DepthAverage.Regular η Q) :
    let L₀ := H+1+1+r+1+d
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular