VertexContinuity.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ConcreteReservoir.physicalBase line 18
lemma OAI.DilutedSpinGlass.ConcreteReservoir.measurable_physicalBase line 22
def OAI.DilutedSpinGlass.ConcreteReservoir.observableAt line 26
def OAI.DilutedSpinGlass.ConcreteReservoir.physicalCoefficient line 33
Source documentation
The actual canceled-anchor covariance coefficient of one independent site/mark insertion into the complete physical Poisson reservoir.
```
noncomputable def physicalCoefficient (S : PrescribedTree (L+1)) (anchor : S.Leaf)
    (M : Model p) (C H : ℝ) (N : ℕ) (u : K×ℕ → ℝ)
    (f : (S.Leaf → FinitePath (Fin N → Spin) (L+1)) → ℝ) (q : K) (k : ℕ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.q
lemma OAI.DilutedSpinGlass.ConcreteReservoir.exponent_cons_monotone line 43
lemma OAI.DilutedSpinGlass.ConcreteReservoir.exponent_cons_nonneg line 46

theorem OAI.DilutedSpinGlass.ConcreteReservoir.physical_coefficients_tendsto line 52

Source documentation

The concrete selected-score producer implies vanishing of every literal coefficient at each bounded old test, on every finite prescribed tree.

theorem physical_coefficients_tendsto (S : PrescribedTree (L+1)) (anchor : S.Leaf)
    (M : Model p) (C H : ℝ) (Ns : ℕ → ℕ) (us : ℕ → K×ℕ → ℝ)
    (f : (n : ℕ) → (S.Leaf → FinitePath (Fin (Ns n+1) → Spin) (L+1)) → ℝ)
    (hm : ∀ l, 0 < m l) (hmono : Monotone m) (hend : m (Fin.last L) = 1)
    {B : ℝ} (hB : 0 ≤ B) (hf : ∀ n x, |f n x| ≤ B)
    (hD : ∀ q σ y, |D q σ y| ≤ 1) (hE : ∀ q σ y, |E q σ y| ≤ 1)
    (hw : ∀ j, 0 < ν.real {j})
    (he : ∀ j, Tendsto (fun n => scoreError ν Q m D E M C H j (Ns n+1) (us n)) atTop (𝓝 0))
    (q : K) (k : ℕ) :
    Tendsto (fun n => physicalCoefficient ν Q m D E S anchor M C H (Ns n+1) (us n) (f n) q k)
      atTop (𝓝 0) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ConcreteReservoir.scoreError, OAI.DilutedSpinGlass.ConcreteReservoir.physicalCoefficient

lemma OAI.DilutedSpinGlass.PrescribedTree.node_family_energy_le line 100
lemma OAI.DilutedSpinGlass.PrescribedTree.unary_family_energy_le line 119
def OAI.DilutedSpinGlass.updateCoordinate line 131
Source documentation
A canonical depth update, with no caller-dependent decidable-equality instance. This is extensionally the ordinary function update.
```
noncomputable def updateCoordinate {α : Type} (q : α → ℕ) (v : α) (t : ℕ) : α → ℕ :=
…
```
Mentions: OAI.DilutedSpinGlass.q
lemma OAI.DilutedSpinGlass.updateCoordinate_self line 134
lemma OAI.DilutedSpinGlass.updateCoordinate_of_ne line 138
def OAI.DilutedSpinGlass.ReducedTopology.vertexArity line 147
lemma OAI.DilutedSpinGlass.ReducedTopology.update_root line 152
lemma OAI.DilutedSpinGlass.ReducedTopology.update_desc_root line 158
lemma OAI.DilutedSpinGlass.ReducedTopology.update_desc_same line 163
lemma OAI.DilutedSpinGlass.ReducedTopology.update_desc_other line 176
lemma OAI.DilutedSpinGlass.ReducedTopology.root_vertex_energy_le line 188
Source documentation
Root-coordinate case at the lesser endpoint, extracted from admissible schedules alone. The descendant-depth gap is a consequence, not an analytic hypothesis or a presumed continuity conclusion.
```
lemma root_vertex_energy_le {Ω : Type} [Fintype Ω]
    (H d r : ℕ) (k : ℕ+) (hk : 2 ≤ (k:ℕ)) (C : Fin k → ReducedTopology)
    (q : (node k hk C).Vertex → ℕ)
    (ha : ∀ t : Fin (r+1), Admissible (node k hk C) (updateCoordinate q none (d+t.val)) d (d+H))
    (T : KernelTower Ω H) (f : FinitePath Ω H → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    (∑ t : Fin r,
      (PrescribedTree.treeMean (realize H d (node k hk C) (updateCoordinate q none (d+t.castSucc.val))) T f-
       PrescribedTree.treeMean (realize H d (node k hk C) (updateCoordinate q none (d+t.succ.val))) T f)^2) ≤ (k:ℝ)^2 := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.updateCoordinate, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.ReducedTopology.realize
theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_vertex_energy_le line 220
Source documentation
Squared one-grid-step changes at an arbitrary vertex of a scheduled reduced topology. All other assigned depths are fixed; no ancestral context or conditional-mean contraction is supplied as a hypothesis.
```
theorem scheduled_vertex_energy_le {Ω : Type} [Fintype Ω]
    (H d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ) (v : S.Vertex)
    (lo r : ℕ)
    (ha : ∀ t : Fin (r+1), Admissible S (updateCoordinate q v (lo+t.val)) d (d+H))
    (T : KernelTower Ω H) (f : FinitePath Ω H → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    (∑ t : Fin r,
      (PrescribedTree.treeMean (realize H d S (updateCoordinate q v (lo+t.castSucc.val))) T f-
       PrescribedTree.treeMean (realize H d S (updateCoordinate q v (lo+t.succ.val))) T f)^2) ≤
      (vertexArity S v:ℝ)^2 := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.updateCoordinate, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.vertexArity
lemma OAI.DilutedSpinGlass.ReducedTopology.realize_translate line 310
theorem OAI.DilutedSpinGlass.ReducedTopology.realize_delay line 329
Source documentation
Canonical unary delay is EXACTLY the assignment with every branching vertex moved one later, not a surrogate shape.
```
theorem realize_delay (H d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (hq : ∀ v, d ≤ q v) :
    realize (H+1) d S (fun v => q v+1)=PrescribedTree.unary (realize H d S q) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.PrescribedTree.unary
theorem OAI.DilutedSpinGlass.ReducedTopology.realize_bottom line 341
Source documentation
Bottom extension preserves all assigned internal depths, and supplies precisely the old tree used opposite a delayed target in the matrix identity.
```
theorem realize_bottom (H d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (hq : Admissible S q d (d+H)) :
    realize (H+1) d S q=PrescribedTree.bottomUnary (realize H d S q) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.PrescribedTree.bottomUnary