MultileafMatrixPointwise.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.externalHistory line 15

Source documentation

The actual old full reservoir is tilted first; the constrained history then samples only its physical paths, with no fresh prior marks left.

noncomputable def externalHistory (S : PrescribedTree (L+1)) (anchorLeaf : S.Leaf)
    (T : KernelTower Ω (L+1)) (m : Fin (L+2) → ℝ)
    (base : FinitePath Ω (L+1) → ℝ) (roots : Fin n → (Spec L×ℕ)×Z)
    (old : (i : (Spec L×ℕ)×Z) → FinitePath Ω (L+1) → FinitePath (Alphabet i.1.1) (L+1) → ℝ)
    (read : Z → FinitePath Ω (L+1) → Spin) (v : Z)
    (a b : Fin r → Option (Fin k)) (d : Fin r → Fin L) (spinAnchor : Bool)
    (f : (S.Leaf → FinitePath Ω (L+1)) → ℝ) : ℝ :=
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.Alphabet, OAI.DilutedSpinGlass.Spin

theorem OAI.DilutedSpinGlass.UniversalDictionary.externalHistory_polarization line 30
def OAI.DilutedSpinGlass.PrescribedTree.splitFrame line 74
Source documentation
The complete old experiment: two entire sides separating at depth d, with their first internal split after another r unary transitions.
```
def splitFrame (S : PrescribedTree n) (r d : ℕ) : PrescribedTree (n+r+1+d) :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
def OAI.DilutedSpinGlass.PrescribedTree.splitFrameLeaf line 77
def OAI.DilutedSpinGlass.PrescribedTree.splitFrameVertex line 80
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFrame_split line 83
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFrame_fresh_split line 92
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFrame_gamma line 96
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFrame_gamma_grid line 103
theorem OAI.DilutedSpinGlass.PrescribedTree.multileaf_matrix_pointwise line 114
Source documentation
Literal multileaf covariance estimate with the FULL signed matrix history. Every old path, every allowed history, the protected charge J and both physical projection errors are retained. The only remaining target error is its explicitly coupled single-copy matrixProjectionError.
```
theorem multileaf_matrix_pointwise (k : ℕ+) (C : Fin k → PrescribedTree n)
    (b : (PrescribedTree.node k C).Leaf) (r d : ℕ)
    (Target : PrescribedTree (n+1+r+1+d)) (q : I → Target.Leaf) (hq : Function.Bijective q)
    (Q : Finset ℕ) (hS : branchingCount (splitFrame (.node k C) r d) (· ∈ Q)=0)
    (K : KernelTower Ω (n+1+r+1+d)) (a c : I) (hac : a≠c)
    (cs : List I) (hcs : cs.Nodup) (hdis : ∀ j ∈ cs, j ∉ insert c ({a}:Finset I))
    (hfull : insert c ({a}:Finset I) ∪ cs.toFinset=Finset.univ)
    (hqd : splitDepth Target (q a) (q c)=d)
    (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i| ≤ 1) :
    let L := n+1+r+1+d
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.splitFrame, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.FinitePath