ScheduledRootMultileaf.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_root_multileaf line 19

Source documentation

Root-averaged genuine old/delayed multileaf induction. The only signed term is ONE centered root matrix covariance, exactly the term controlled by physical_matrix_selection. All remaining errors are actual proper children or the single-copy h_N; the target projection error is eliminated.

theorem scheduled_root_multileaf {Z : Type} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (Ω : Z → Type) [∀ z, Fintype (Ω z)]
    (H r 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)) (ha : (Q a).val=r+1+d)
    (hQ : ∀ j v, (Q a).val+1≤(Q (e j v)).val)
    (K : (z : Z) → KernelTower (Ω z) (H+1+1+r+1+d))
    (f : (z : Z) → FinitePath (Ω z) (H+1+1+r+1+d) → Fin N → ℝ)
    (hf : ∀ z x i, |f z x i|≤1) :
    let L := H+1+1+r+1+d
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath

def OAI.DilutedSpinGlass.ReducedTopology.regularShapeDomain line 126
Source documentation
The literal single-copy depth domain: one evaluation coordinate, the branching coordinates, their strict ancestry and the regular interior cube.
```
def regularShapeDomain (S : ReducedTopology) (L : ℕ) [NeZero L] (η : ℝ)
    (Q : Option S.Vertex → Fin L) : Prop :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology
def OAI.DilutedSpinGlass.ReducedTopology.childCoordinates line 132
Source documentation
A proper child retains the first branching coordinate as its evaluation coordinate, and precisely its own internal branching coordinates.
```
def childCoordinates {k : ℕ+} {hk : 2≤(k:ℕ)} {C : Fin k → ReducedTopology}
    (j : Fin k) : Option (C j).Vertex → Option (ReducedTopology.node k hk C).Vertex
  | none => some none
  | some v => some (some ⟨j,v⟩)
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex
lemma OAI.DilutedSpinGlass.ReducedTopology.childCoordinates_injective line 137
lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_shift_same_upper line 142
theorem OAI.DilutedSpinGlass.ReducedTopology.regular_child_projection line 155
Source documentation
Both the old and all-coordinates-delayed proper child lie in the SAME admissible regular domain. Rotation is genuinely +1 here: no wraparound is silently admitted at the terminal level.
```
theorem regular_child_projection {L : ℕ} [NeZero L] {η : ℝ}
    (hη : 0<η) (hlarge : 4<η*(L:ℝ))
    {k : ℕ+} {hk : 2≤(k:ℕ)} {C : Fin k → ReducedTopology}
    (j : Fin k) (s : Bool) {Q : Option (ReducedTopology.node k hk C).Vertex → Fin L}
    (hQ : regularShapeDomain (.node k hk C) L η Q) :
    regularShapeDomain (C j) L (η/2)
      (coordinateProjection (childCoordinates (hk := hk) j) (fun _ => shiftPerm s) Q) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.regularShapeDomain, OAI.DilutedSpinGlass.ReducedTopology.childCoordinates
theorem OAI.DilutedSpinGlass.ReducedTopology.regular_scheduled_child_moment line 176