PhysicalSingleton.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.physicalSingletonEnergy line 16
Source documentation
The manuscript's singleton conditional spatial covariance density, under the actual tilted reservoir, averaged over roots and the d-coordinate prefix.
```
noncomputable def physicalSingletonEnergy (m : Fin (L+1) → ℝ) (M : Model p) (C H : ℝ)
    (N : ℕ) (u : Spec L×ℕ → ℝ) (d : ℕ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec
def OAI.DilutedSpinGlass.UniversalDictionary.singletonOldTest line 26
lemma OAI.DilutedSpinGlass.UniversalDictionary.singletonOldTest_bound line 31

theorem OAI.DilutedSpinGlass.UniversalDictionary.physical_singleton_bound line 37

Source documentation

Exact one-color singleton estimate at every N, before taking any limit. The error is the literal physical prescribed-shape covariance already selected by the universal perturbation, not a newly imposed covariance hypothesis.

theorem physical_singleton_bound (m : Fin (L+1) → ℝ) (hm : ∀ j, 0 ≤ m j)
    (hmono : Monotone m) (hend : m (Fin.last L) = 1)
    (M : Model p) (C H : ℝ) (N : ℕ) (u : Spec L×ℕ → ℝ) (d : ℕ) (hd : d < L+1) :
    (2*(Fin.cons 0 m : Fin (L+2) → ℝ) ⟨d+1,by omega⟩-(Fin.cons 0 m : Fin (L+2) → ℝ) ⟨d,by omega⟩) *
      physicalSingletonEnergy m M C H N u d ≤
    ((Fin.cons 0 m : Fin (L+2) → ℝ) ⟨d+1,by omega⟩-(Fin.cons 0 m : Fin (L+2) → ℝ) ⟨d,by omega⟩) +
      physicalShapeCovariance m (forkAt (L+1) d hd) (forkAtLeaf (L+1) d hd 0)
        M C H N u (pairSplitTest d) true (singletonOldTest d hd N) := by
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.physicalSingletonEnergy, OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeCovariance, OAI.DilutedSpinGlass.UniversalDictionary.pairSplitTest, OAI.DilutedSpinGlass.UniversalDictionary.singletonOldTest