ScheduledCovariance.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy line 16
Source documentation
The actual single-copy conditional covariance of a reduced topology at a specified evaluation depth, with all unary grid transitions retained. Outside the available evaluation horizon it is zero; all induction applications are inside the literal admissible regular-depth domain.
```
noncomputable def scheduledShapeEnergy (L d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_nonneg line 23
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_eq_realize line 31
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_heightCast line 45
lemma OAI.DilutedSpinGlass.ReducedTopology.descendantEnergyAt_eq_scheduled line 56
Source documentation
Exact retained-coordinate identification used by the fiber estimate. The child covariance at the later first split is precisely this same energy family, not a separately selected experiment and not a two-copy depth average.
```
lemma descendantEnergyAt_eq_scheduled (n r d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (T : KernelTower Ω (n+1+r+1+d)) (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) :
    descendantEnergyAt (realize n (r+1+d+1) S q) r d T f =
      scheduledShapeEnergy (n+1+r+1+d) (r+1+d) S q T f := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_node line 65
Source documentation
The left side of the multileaf step belongs to the same literal scheduled covariance family as its proper-child energies.
```
lemma scheduledShapeEnergy_node (n r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (C : Fin k → ReducedTopology) (q : (j : Fin k) → (C j).Vertex → ℕ)
    (hq : ∀ j v, r+1+d+1≤q j v)
    (T : KernelTower Ω (n+1+r+1+d)) (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) :
    scheduledShapeEnergy (n+1+r+1+d) d (.node k hk C) (rootSchedule (r+1+d) q) T f =
      shapeEnergyAt (stem (.node k (fun j => realize n (r+1+d+1) (C j) (q j))) r) d T f := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy, OAI.DilutedSpinGlass.ReducedTopology.rootSchedule, OAI.DilutedSpinGlass.ReducedTopology.realize