OAI/Probability/DilutedSpin/ProfileHistory.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.grow_leaf_cases line 13

   Source documentation

   Growth adds exactly one new positional leaf, not just one spin value.

   theorem grow_leaf_cases (S : PrescribedTree n) (v : S.Internal) (b : (grow S v).Leaf) :
       b = newLeaf S v ∨ ∃ a, b = oldLeaf S v a := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf

2. structure OAI.DilutedSpinGlass.PrescribedTree.HistoryCover line 34

   Source documentation

   The available original positions and the already assigned colors cover all current leaves. Previously fresh leaves are assigned, never made available.

   structure HistoryCover (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
       (P : Finset C) (pos : C → S.Leaf) : Prop extends HistoryValid S U loc P pos where
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.HistoryValid

3. lemma OAI.DilutedSpinGlass.PrescribedTree.HistoryCover.pick_old line 38
4. lemma OAI.DilutedSpinGlass.PrescribedTree.HistoryCover.pick_fresh line 53
5. lemma OAI.DilutedSpinGlass.PrescribedTree.anchorHistory_cover line 67
6. lemma OAI.DilutedSpinGlass.PrescribedTree.HistoryCover.sum_available line 79

   Source documentation

   Available-old sums equal unrestricted old-leaf sums for any observable that vanishes on the protected references. No probability calculation occurs.

   lemma HistoryCover.sum_available {S : PrescribedTree n} {U : Finset ι}
       {loc : ι → S.Leaf} {P : Finset C} {pos : C → S.Leaf}
       (h : HistoryCover S U loc P pos) (F : S.Leaf → ℝ)
       (hF : ∀ c ∈ P, F (pos c) = 0) :
       (∑ i ∈ U, F (loc i)) = ∑ b : S.Leaf, F b := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.HistoryCover

7. abbrev OAI.DilutedSpinGlass.PrescribedTree.SharingIndex line 103
8. def OAI.DilutedSpinGlass.PrescribedTree.sharingProfile line 105
9. def OAI.DilutedSpinGlass.PrescribedTree.splitFromProfile line 110

   Source documentation

   Recover the complete split-depth matrix from interior sharing bits. The terminal diagonal is known from colors, not from an endpoint mark.

   def splitFromProfile (y : SharingIndex L C → Bool) (a b : C) : ℕ :=
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree.SharingIndex

10. lemma OAI.DilutedSpinGlass.PrescribedTree.splitFromProfile_eq line 114
11. def OAI.DilutedSpinGlass.PrescribedTree.requirementMap line 130
12. lemma OAI.DilutedSpinGlass.PrescribedTree.monomial_sharing line 134
13. def OAI.DilutedSpinGlass.PrescribedTree.shapeHistory line 153

    Source documentation

    Literal signed extension history with an arbitrary prescribed split-depth weight. In particular indicator weights encode exact consistent constraints.

    noncomputable def shapeHistory (T : KernelTower Ω (L+1)) (m : Fin (L+2) → ℝ)
        (F : (Option (Fin k) → Option (Fin k) → ℕ) → ℝ)
        (spinColor : Option (Fin k) → FinitePath Ω (L+1) → ℝ)
        (S : PrescribedTree (L+1)) (anchor : S.Leaf) (f : Sample Ω S → ℝ) : ℝ := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample

14. theorem OAI.DilutedSpinGlass.PrescribedTree.shapeHistory_expansion line 166

    Source documentation

    Full exact splitting constraints reduce to finitely many sharing histories, using distinct geometric positions throughout every branch.

    theorem shapeHistory_expansion (T : KernelTower Ω (L+1)) (m : Fin (L+2) → ℝ)
        (F : (Option (Fin k) → Option (Fin k) → ℕ) → ℝ)
        (spinColor : Option (Fin k) → FinitePath Ω (L+1) → ℝ)
        (S : PrescribedTree (L+1)) (anchor : S.Leaf) (f : Sample Ω S → ℝ) :
        shapeHistory T m F spinColor S anchor f =
          ∑ s : Finset (SharingIndex L (Option (Fin k))),
            BooleanPolynomial.coefficient (fun y => F (splitFromProfile y)) s *
            constrainedHistory T m (fun j => (requirementMap s j).1)
              (fun j => (requirementMap s j).2.1) (fun j => (requirementMap s j).2.2.castSucc)
              spinColor S anchor f := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.shapeHistory, OAI.DilutedSpinGlass.PrescribedTree.SharingIndex, OAI.DilutedSpinGlass.BooleanPolynomial.coefficient, OAI.DilutedSpinGlass.PrescribedTree.splitFromProfile, OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory, OAI.DilutedSpinGlass.PrescribedTree.requirementMap