RootMatrixTriple.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.root_matrix_three_copy line 17

Source documentation

The full shifted-matrix/three-copy estimate after root averaging. The only analytic errors are actual target and old single-copy L2 projection errors. The prescribed-tree identity appears as ONE centered root covariance, not any stronger conditional or absolute pointwise concentration claim.

theorem root_matrix_three_copy {Z : Type} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (Ω : Z → Type) [∀ z, Fintype (Ω z)]
    (hL : 0 < L) (Q : Finset ℕ) (T S : PrescribedTree L)
    (q : C → T.Leaf) (hq : Function.Bijective q) (hS : branchingCount S (· ∈ Q) = 0)
    (K : (z : Z) → KernelTower (Ω z) L)
    (a c : C) (hac : a ≠ c) (cs : List C) (hcs : cs.Nodup)
    (hdis : ∀ b ∈ cs, b ∉ insert c ({a} : Finset C))
    (hfull : insert c ({a} : Finset C) ∪ cs.toFinset = Finset.univ)
    (x y : S.Leaf) (v : S.Internal) (d : ℕ) (hd : d < L)
    (hqd : splitDepth T (q a) (q c) = d) (hxy : splitDepth S x y = d)
    (hxv : freshSplitDepth S v x = d) (hyv : freshSplitDepth S v y = d)
    (X : (z : Z) → FinitePath (Ω z) L → Fin N → ℝ) (hX : ∀ z w i, |X z w i| ≤ 1)
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.FinitePath

lemma OAI.DilutedSpinGlass.PrescribedTree.partialKappa_grid_pair line 87
theorem OAI.DilutedSpinGlass.PrescribedTree.protectedKappa_grid_lower line 95
Source documentation
The separation vertex is the protected pair factor, leaving exactly the powers charged at the shifted internal branching vertices.
```
theorem protectedKappa_grid_lower (hL : 0 < L) (T : PrescribedTree L)
    (a b : T.Leaf) (hab : a ≠ b) (η : ℝ) (hη : 0 ≤ η)
    (hr : BranchRegular T (grid L 0 L) η) (k : ℕ)
    (hk : branchingCount T (fun _ => True) = k+1) :
    (L:ℝ)⁻¹^k*η^(branchExcess T) ≤
      |partialKappa T (grid L 0 L) Finset.univ / partialKappa T (grid L 0 L) {b,a}| := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.BranchRegular, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.branchExcess, OAI.DilutedSpinGlass.PrescribedTree.partialKappa
theorem OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge_relative_bound line 110
Source documentation
The manuscript's relative absolute-cost bound. Its dimensional power of L cancels EXACTLY, including distinct target vertices sharing a depth.
```
theorem shiftedCharge_relative_bound (hL : 0 < L) (Q : Finset ℕ)
    (T S : PrescribedTree L) (k : ℕ) (a b : T.Leaf) (hab : a ≠ b)
    (η : ℝ) (hη : 0 < η) (hr : BranchRegular T (grid L 0 L) η)
    (hb : branchingCount T (fun _ => True) = branchingCount T (· ∈ Q)+1) :
    shiftedCharge Q T S k /
        |partialKappa T (grid L 0 L) Finset.univ / partialKappa T (grid L 0 L) {b,a}| ≤
      chargeBound (2*(leaves S+k:ℕ)) ((Q.card:ℝ)*(leaves S+k:ℕ)) k
        (branchingCount T (· ∈ Q)) / η^(branchExcess T) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.BranchRegular, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge, OAI.DilutedSpinGlass.PrescribedTree.partialKappa, OAI.DilutedSpinGlass.PrescribedTree.chargeBound, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.branchExcess
def OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq line 144
theorem OAI.DilutedSpinGlass.FiniteLaw.covariance_projection_transfer line 149
Source documentation
Exact three-copy transfer for a coupled true vector and projected vector. This prevents the invalid inference from only projected covariance energy.
```
theorem covariance_projection_transfer (P : FiniteLaw Ω) (X Y : Ω → Fin N → ℝ) :
    P.covarianceEnergy X ≤
      P.expect (fun x => P.expect (fun y => P.expect (fun z =>
        (dot (Y x) (Y y)-dot (Y x) (Y z))^2)))+4*pairProjectionSq P X Y := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq
lemma OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq_eq_l2 line 174
lemma OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq_le_l2 line 182
Source documentation
Since both contractions are in [-1,1], their squared L2 error is at most twice their L2 error. This is the linear error used in the induction.
```
lemma pairProjectionSq_le_l2 (P : FiniteLaw Ω) (X Y : Ω → Fin N → ℝ)
    (hX : ∀ z i, |X z i| ≤ 1) (hY : ∀ z i, |Y z i| ≤ 1) :
    pairProjectionSq P X Y ≤ 2*(P.bind (fun _ => P)).l2
      (fun z => dot (X z.1) (X z.2)-dot (Y z.1) (Y z.2)) := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq, OAI.DilutedSpinGlass.FiniteLaw.l2, OAI.DilutedSpinGlass.FiniteLaw.dot