OAI/Probability/DilutedSpin/HistoryGeometry.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.singleLeaf line 12

   Source documentation

   The unique labeled position in a unary tree.

   def singleLeaf : (n : ℕ) → Leaf (single n)
     | 0 => ()
     | n+1 => ⟨0, singleLeaf n⟩
   
   /-- The old paths keep their separate labels when a genuine fresh branch is added. -/

   Mentions: OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.single

2. def OAI.DilutedSpinGlass.PrescribedTree.oldLeaf line 17

   Source documentation

   The old paths keep their separate labels when a genuine fresh branch is added.

   def oldLeaf : {n : ℕ} → (S : PrescribedTree n) → (v : Internal S) →
       Leaf S → Leaf (grow S v)
     | 0, .leaf, v, _ => nomatch v
     | n+1, .node k C, v, a => by
       change Option ((i : Fin k) × Internal (C i)) at v
       cases v with
       | none => exact ⟨a.1.succ, a.2⟩
       | some v =>
         obtain ⟨i,v⟩ := v
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.grow

3. def OAI.DilutedSpinGlass.PrescribedTree.newLeaf line 33

   Source documentation

   The single distinguished newly added replica position.

   def newLeaf : {n : ℕ} → (S : PrescribedTree n) → (v : Internal S) → Leaf (grow S v)
     | 0, .leaf, v => nomatch v
     | n+1, .node k C, v => by
       change Option ((i : Fin k) × Internal (C i)) at v
       cases v with
       | none => exact ⟨0, singleLeaf n⟩
       | some v =>
         obtain ⟨i,v⟩ := v
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.singleLeaf

4. def OAI.DilutedSpinGlass.PrescribedTree.splitDepth line 46

   Source documentation

   Split depth compares positions, never the sampled spin values. Equal positions have split depth n; distinct positions split strictly before n.

   def splitDepth : {n : ℕ} → (S : PrescribedTree n) → Leaf S → Leaf S → ℕ
     | 0, .leaf, _, _ => 0
     | _+1, .node _ C, a, b => if h : a.1 = b.1 then
         1 + splitDepth (C a.1) a.2 (h.symm ▸ b.2) else 0

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf

5. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_self line 51
6. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_le line 57
7. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_eq_height line 70
8. theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_singleLeaf line 95
9. theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_node line 104
10. theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_cast line 108
11. theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_oldLeaf line 116
12. theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_newLeaf line 148
13. inductive OAI.DilutedSpinGlass.PrescribedTree.Divergence line 178

    Source documentation

    The deepest reference prefix and its forbidden reference-containing children. This describes the whole compatible choice set, including both old unused leaves and fresh divergences in reference-free subtrees.

    inductive Divergence : {n : ℕ} → PrescribedTree n → Type
      | here {n : ℕ} {k : ℕ+} {C : Fin k → PrescribedTree n}
          (excluded : Finset (Fin k)) : Divergence (.node k C)
      | descend {n : ℕ} {k : ℕ+} {C : Fin k → PrescribedTree n}
          (i : Fin k) (next : Divergence (C i)) : Divergence (.node k C)
    
    namespace Divergence

    Mentions: OAI.DilutedSpinGlass.PrescribedTree

14. def OAI.DilutedSpinGlass.PrescribedTree.Divergence.oldAllowed line 186
15. def OAI.DilutedSpinGlass.PrescribedTree.Divergence.freshAllowed line 190
16. def OAI.DilutedSpinGlass.PrescribedTree.Divergence.coefficient line 200
17. theorem OAI.DilutedSpinGlass.PrescribedTree.all_choices_total line 209

    Source documentation

    Full cancellation inside a reference-free subtree, indexed by actual leaf positions and actual internal vertices.

    theorem all_choices_total {n : ℕ} (S : PrescribedTree n) (m : Fin (n+1) → ℝ)
        (hend : m (Fin.last n) = 1) :
        (∑ _a : Leaf S, (1 : ℝ)) + (∑ v : Internal S, gamma S m v) = m 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma

18. theorem OAI.DilutedSpinGlass.PrescribedTree.divergence_choice_total line 226

    Source documentation

    The signed normalizing sum of ALL eligible old-or-fresh choices with a specified deepest reference prefix is independent of all unused old branches. Unlike reference_total, this is stated on the actual global choice indices.

    theorem divergence_choice_total {n : ℕ} {S : PrescribedTree n}
        (D : Divergence S) (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) :
        (∑ a : Leaf S, if D.oldAllowed a then (1 : ℝ) else 0) +
          (∑ v : Internal S, if D.freshAllowed v then gamma S m v else 0) = D.coefficient m := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Divergence, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma

19. def OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth line 304

    Source documentation

    Positional split depth of a genuinely fresh branch from an old reference.

    def freshSplitDepth : {n : ℕ} → (S : PrescribedTree n) → Internal S → Leaf S → ℕ
      | 0, .leaf, v, _ => nomatch v
      | _+1, .node k C, v, a =>
        match (v : Option ((i : Fin k) × Internal (C i))) with
        | none => 0
        | some ⟨i,v⟩ => if h : a.1 = i then 1 + freshSplitDepth (C i) v (h ▸ a.2) else 0

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf

20. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_cast line 311
21. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_new_old line 318

    Source documentation

    Fresh splitting refers to the enlarged tree's actual labeled positions.

    theorem splitDepth_new_old {n : ℕ} (S : PrescribedTree n) (v : Internal S) (a : Leaf S) :
        splitDepth (grow S v) (newLeaf S v) (oldLeaf S v a) = freshSplitDepth S v a := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth

22. def OAI.DilutedSpinGlass.PrescribedTree.childRefs line 352
23. theorem OAI.DilutedSpinGlass.PrescribedTree.mem_childRefs line 356
24. def OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence line 363

    Source documentation

    A proposed fresh split at depth d along a reference path. Every child containing any reference through the chosen prefix is forbidden.

    noncomputable def referenceDivergence : {n : ℕ} → (S : PrescribedTree n) →
        (a : Leaf S) → (d : ℕ) → d < n → Finset (Leaf S) → Divergence S
      | 0, .leaf, _, d, hd, _ => (Nat.not_lt_zero d hd).elim
      | _+1, .node _ _, _, 0, _, R => .here (R.image (fun a => a.1))
      | n+1, .node _ C, a, d+1, hd, R => .descend a.1
          (referenceDivergence (C a.1) a.2 d (by omega) (childRefs R a.1))
    
    /-- Shared-prefix equations determine the same allowed old-or-fresh set as
    references; this positional definition does not examine any spin values. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Divergence, OAI.DilutedSpinGlass.PrescribedTree.childRefs, OAI.DilutedSpinGlass.spin

25. def OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile line 372

    Source documentation

    Shared-prefix equations determine the same allowed old-or-fresh set as references; this positional definition does not examine any spin values.

    def matchesOldProfile {n : ℕ} (S : PrescribedTree n) (R : Finset (Leaf S))
        (a : Leaf S) (d : ℕ) (b : Leaf S) : Prop :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf

26. def OAI.DilutedSpinGlass.PrescribedTree.matchesFreshProfile line 376
27. theorem OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile_not_mem line 381

    Source documentation

    A reference itself is never an eligible old leaf.

    theorem matchesOldProfile_not_mem {n : ℕ} (S : PrescribedTree n) (R : Finset (Leaf S))
        (a b : Leaf S) {d : ℕ} (hd : d < n) (h : matchesOldProfile S R a d b) : b ∉ R := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile

28. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_same_child line 394
29. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_diff_child line 400
30. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_node_zero line 406
31. theorem OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence_oldAllowed line 420

    Source documentation

    Ancestry constraints with ALL existing references, not merely a local subtree, are exactly the global eligible-old-leaf selector.

    theorem referenceDivergence_oldAllowed {n : ℕ} (S : PrescribedTree n)
        (a : Leaf S) (d : ℕ) (hd : d < n) (R : Finset (Leaf S)) (ha : a ∈ R) (b : Leaf S) :
        (referenceDivergence S a d hd R).oldAllowed b ↔ matchesOldProfile S R a d b := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence, OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile

32. theorem OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth_same_child line 483
33. theorem OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth_diff_child line 489
34. theorem OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth_node_zero line 495
35. theorem OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence_freshAllowed line 509

    Source documentation

    Fresh divergences satisfy exactly the same all-reference positional profile as the old-choice selector; the profile is also the actual new leaf's profile in the enlarged tree, by splitDepth_new_old.

    theorem referenceDivergence_freshAllowed {n : ℕ} (S : PrescribedTree n)
        (a : Leaf S) (d : ℕ) (hd : d < n) (R : Finset (Leaf S)) (ha : a ∈ R) (v : Internal S) :
        (referenceDivergence S a d hd R).freshAllowed v ↔ matchesFreshProfile S R a d v := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence, OAI.DilutedSpinGlass.PrescribedTree.matchesFreshProfile

36. theorem OAI.DilutedSpinGlass.PrescribedTree.reference_profile_total line 588

    Source documentation

    The reference-path normalizing identity over globally admissible old or fresh labels. No conditioning on sampled spin values occurs in the selector.

    theorem reference_profile_total {n : ℕ} (S : PrescribedTree n)
        (a : Leaf S) (d : ℕ) (hd : d < n) (R : Finset (Leaf S)) (ha : a ∈ R)
        (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) :
        (∑ b : Leaf S, if matchesOldProfile S R a d b then (1 : ℝ) else 0) +
          (∑ v : Internal S, if matchesFreshProfile S R a d v then gamma S m v else 0) =
          (referenceDivergence S a d hd R).coefficient m := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.matchesFreshProfile, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence

37. theorem OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth_lt line 604

    Source documentation

    Freshness is positional and survives deterministic or atomic spin laws.

    theorem freshSplitDepth_lt {n : ℕ} (S : PrescribedTree n) (v : Internal S) (a : Leaf S) :
        freshSplitDepth S v a < n := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth

38. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_old_old line 624

    Source documentation

    Old leaves retain their pairwise positional ancestry under actual grow.

    theorem splitDepth_old_old {n : ℕ} (S : PrescribedTree n) (v : Internal S) (a b : Leaf S) :
        splitDepth (grow S v) (oldLeaf S v a) (oldLeaf S v b) = splitDepth S a b := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf

39. theorem OAI.DilutedSpinGlass.PrescribedTree.oldLeaf_injective line 676
40. theorem OAI.DilutedSpinGlass.PrescribedTree.newLeaf_ne_oldLeaf line 682
41. theorem OAI.DilutedSpinGlass.PrescribedTree.card_image_of_same_kernel line 698

    Source documentation

    A finite number of represented equivalence classes depends only on the kernel relation, not on their ambient set of representatives.

    theorem card_image_of_same_kernel {ι α β : Type*} [DecidableEq ι]
        [DecidableEq α] [DecidableEq β] (R : Finset ι) (f : ι → α) (g : ι → β)
        (h : ∀ i ∈ R, ∀ j ∈ R, f i = f j ↔ g i = g j) :
        (R.image f).card = (R.image g).card := by
    …

42. abbrev OAI.DilutedSpinGlass.PrescribedTree.ChildLabels line 725

    Source documentation

    Reference labels in a particular child, preserving their identities.

    abbrev ChildLabels {n : ℕ} {k : ℕ+} {C : Fin k → PrescribedTree n}
        {ι : Type} (r : ι → Leaf (.node k C)) (i : Fin k) := {l : ι // (r l).1 = i}

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf

43. def OAI.DilutedSpinGlass.PrescribedTree.childLabelLeaf line 728
44. theorem OAI.DilutedSpinGlass.PrescribedTree.sigma_cast_snd line 732
45. theorem OAI.DilutedSpinGlass.PrescribedTree.childLabelLeaf_embed line 740

    Source documentation

    Returning a restricted reference label to its original tree.

    theorem childLabelLeaf_embed {n : ℕ} {k : ℕ+} {C : Fin k → PrescribedTree n}
        {ι : Type} (r : ι → Leaf (.node k C)) (i : Fin k) (l : ChildLabels r i) :
        (⟨i,childLabelLeaf r i l⟩ : Leaf (.node k C)) = r l.val := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ChildLabels, OAI.DilutedSpinGlass.PrescribedTree.childLabelLeaf

46. theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_image line 746

    Source documentation

    The child reference set really is the image of the child-restricted labels.

    theorem childRefs_image {n : ℕ} {k : ℕ+} {C : Fin k → PrescribedTree n}
        {ι : Type} [Fintype ι] (r : ι → Leaf (.node k C)) (i : Fin k) :
        childRefs (Finset.univ.image r) i =
          Finset.univ.image (childLabelLeaf r i) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.childRefs, OAI.DilutedSpinGlass.PrescribedTree.childLabelLeaf

47. theorem OAI.DilutedSpinGlass.PrescribedTree.reference_coefficient_invariant line 769

    Source documentation

    One-step signed reference normalization is determined by the entire labeled splitting matrix, not by the unused old leaves of its realization.

    theorem reference_coefficient_invariant {n : ℕ} (S T : PrescribedTree n)
        {ι : Type} [Fintype ι] (r : ι → Leaf S) (s : ι → Leaf T) (a : ι)
        (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
        (d : ℕ) (hd : d < n) (m : Fin (n+1) → ℝ) :
        (referenceDivergence S (r a) d hd (Finset.univ.image r)).coefficient m =
          (referenceDivergence T (s a) d hd (Finset.univ.image s)).coefficient m := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence

48. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_symm line 842
49. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_ultrametric line 855

    Source documentation

    Positional ancestry is an ultrametric similarity, independently of spins.

    theorem splitDepth_ultrametric {n : ℕ} (S : PrescribedTree n) (a b c : Leaf S) :
        min (splitDepth S a b) (splitDepth S b c) ≤ splitDepth S a c := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

50. theorem OAI.DilutedSpinGlass.PrescribedTree.deepest_reference_profile line 876
51. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_lt_of_ne line 884
52. theorem OAI.DilutedSpinGlass.PrescribedTree.exists_deepest_reference line 891

    Source documentation

    A deepest reference exists among any finite nonempty set of labels.

    theorem exists_deepest_reference {n : ℕ} (S : PrescribedTree n)
        {ι : Type} [Fintype ι] [Nonempty ι] (r : ι → Leaf S) (b : Leaf S) :
        ∃ a, ∀ i, splitDepth S b (r i) ≤ splitDepth S b (r a) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

53. def OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch line 905

    Source documentation

    Full ancestry selector for using an old unused path as the next color.

    def labeledOldMatch {n : ℕ} (S T : PrescribedTree n) {ι : Type}
        (r : ι → Leaf S) (s : ι → Leaf T) (b : Leaf T) (x : Leaf S) : Prop :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf

54. def OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch line 910

    Source documentation

    Full ancestry selector for a genuinely fresh path as the next color.

    def labeledFreshMatch {n : ℕ} (S T : PrescribedTree n) {ι : Type}
        (r : ι → Leaf S) (s : ι → Leaf T) (b : Leaf T) (v : Internal S) : Prop :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Internal

55. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch_profile line 914
56. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch_profile line 929
57. theorem OAI.DilutedSpinGlass.PrescribedTree.labeled_choice_total line 946

    Source documentation

    Every eligible old or fresh choice is counted once. Its signed total depends only on the prescribed reference splitting matrix.

    theorem labeled_choice_total {n : ℕ} (S T : PrescribedTree n)
        {ι : Type} [Fintype ι] (r : ι → Leaf S) (s : ι → Leaf T) (b : Leaf T) (a : ι)
        (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
        (hne : b ≠ s a) (hmax : ∀ i, splitDepth T b (s i) ≤ splitDepth T b (s a))
        (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) :
        (∑ x : Leaf S, if labeledOldMatch S T r s b x then (1:ℝ) else 0) +
          (∑ v : Internal S, if labeledFreshMatch S T r s b v then gamma S m v else 0) =
          (referenceDivergence T (s a) (splitDepth T b (s a))
            (splitDepth_lt_of_ne T b (s a) hne) (Finset.univ.image s)).coefficient m := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence, OAI.DilutedSpinGlass.PrescribedTree.splitDepth_lt_of_ne

58. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch_unused line 963

    Source documentation

    Eligible old leaves are unused, since the target color is new.

    theorem labeledOldMatch_unused {n : ℕ} (S T : PrescribedTree n) {ι : Type}
        (r : ι → Leaf S) (s : ι → Leaf T) (b : Leaf T) (x : Leaf S)
        (hne : ∀ i, b ≠ s i) (h : labeledOldMatch S T r s b x) : ∀ i, x ≠ r i := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch

59. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch_cons line 972

    Source documentation

    On adding an eligible old color, ALL reference ancestries are retained.

    theorem labeledOldMatch_cons {n p : ℕ} (S T : PrescribedTree n)
        (r : Fin p → Leaf S) (s : Fin p → Leaf T) (b : Leaf T) (x : Leaf S)
        (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
        (h : labeledOldMatch S T r s b x) : ∀ i j : Fin (p+1),
          splitDepth S ((Fin.cons x r : Fin (p+1) → Leaf S) i) ((Fin.cons x r : Fin (p+1) → Leaf S) j) =
            splitDepth T ((Fin.cons b s : Fin (p+1) → Leaf T) i) ((Fin.cons b s : Fin (p+1) → Leaf T) j) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch

60. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch_cons line 987

    Source documentation

    On adding an eligible fresh color, ALL reference ancestries are retained.

    theorem labeledFreshMatch_cons {n p : ℕ} (S T : PrescribedTree n)
        (r : Fin p → Leaf S) (s : Fin p → Leaf T) (b : Leaf T) (v : Internal S)
        (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
        (h : labeledFreshMatch S T r s b v) : ∀ i j : Fin (p+1),
          splitDepth (grow S v) ((Fin.cons (newLeaf S v) (oldLeaf S v ∘ r) : Fin (p+1) → Leaf (grow S v)) i)
            ((Fin.cons (newLeaf S v) (oldLeaf S v ∘ r) : Fin (p+1) → Leaf (grow S v)) j) =
            splitDepth T ((Fin.cons b s : Fin (p+1) → Leaf T) i) ((Fin.cons b s : Fin (p+1) → Leaf T) j) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf

61. theorem OAI.DilutedSpinGlass.PrescribedTree.reference_coefficient_neg line 1013

    Source documentation

    The one-step coefficient cannot vanish for a genuine reference divergence and strictly increasing cavity exponents.

    theorem reference_coefficient_neg {n : ℕ} (S : PrescribedTree n)
        (a : Leaf S) (d : ℕ) (hd : d < n) (R : Finset (Leaf S)) (ha : a ∈ R)
        (m : Fin (n+1) → ℝ) (hm : StrictMono m) (hnonneg : ∀ j, 0 ≤ m j) :
        (referenceDivergence S a d hd R).coefficient m < 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence

62. inductive OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan line 1043

    Source documentation

    A finite color prescription. The deepest-reference witness is only positional data; exists_deepest_reference supplies it for every new leaf.

    inductive ReferencePlan {n : ℕ} (T : PrescribedTree n) :
        {p : ℕ} → (Fin (p+1) → Leaf T) → Type
      | nil {p : ℕ} {s : Fin (p+1) → Leaf T} : ReferencePlan T s
      | cons {p : ℕ} {s : Fin (p+1) → Leaf T} (b : Leaf T) (a : Fin (p+1))
          (fresh : ∀ i, b ≠ s i)
          (deepest : ∀ i, splitDepth T b (s i) ≤ splitDepth T b (s a))
          (next : ReferencePlan T (Fin.cons b s)) : ReferencePlan T s
    
    /-- The deterministic product of one-step reference factors. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

63. def OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer line 1052

    Source documentation

    The deterministic product of one-step reference factors.

    noncomputable def referencePlanNormalizer {n : ℕ} (T : PrescribedTree n)
        (m : Fin (n+1) → ℝ) : {p : ℕ} → {s : Fin (p+1) → Leaf T} → ReferencePlan T s → ℝ
      | _, _, .nil => 1
      | _, s, .cons b a hne _ next =>
          (referenceDivergence T (s a) (splitDepth T b (s a))
            (splitDepth_lt_of_ne T b (s a) (hne a)) (Finset.univ.image s)).coefficient m *
              referencePlanNormalizer T m next
    
    /-- The signed sum over the actual sequential old-or-fresh choices. Every
    fresh choice changes the entire current tree with grow, and transports all
    previous references. No constant normalization is built into this recursion. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.referenceDivergence, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.splitDepth_lt_of_ne, OAI.DilutedSpinGlass.PrescribedTree.grow

64. def OAI.DilutedSpinGlass.PrescribedTree.referenceHistoryTotal line 1063

    Source documentation

    The signed sum over the actual sequential old-or-fresh choices. Every fresh choice changes the entire current tree with grow, and transports all previous references. No constant normalization is built into this recursion.

    noncomputable def referenceHistoryTotal {n : ℕ} (T : PrescribedTree n)
        (m : Fin (n+1) → ℝ) : {p : ℕ} → {s : Fin (p+1) → Leaf T} → ReferencePlan T s →
          (S : PrescribedTree n) → (Fin (p+1) → Leaf S) → ℝ
      | _, _, .nil, _, _ => 1
      | _, s, .cons b _ _ _ next, S, r =>
          (∑ x : Leaf S, if labeledOldMatch S T r s b x then
            referenceHistoryTotal T m next S (Fin.cons x r) else 0) +
          (∑ v : Internal S, if labeledFreshMatch S T r s b v then
            gamma S m v * referenceHistoryTotal T m next (grow S v)
              (Fin.cons (newLeaf S v) (oldLeaf S v ∘ r)) else 0)
    
    /-- Reference-path totals for any finite number of colors and any old tree.

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf

65. theorem OAI.DilutedSpinGlass.PrescribedTree.reference_history_total line 1076

    Source documentation

    Reference-path totals for any finite number of colors and any old tree. The histories have globally consistent splitting matrices at every step.

    theorem reference_history_total {n p : ℕ} (T : PrescribedTree n)
        (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1)
        {s : Fin (p+1) → Leaf T} (P : ReferencePlan T s) (S : PrescribedTree n)
        (r : Fin (p+1) → Leaf S)
        (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j)) :
        referenceHistoryTotal T m P S r = referencePlanNormalizer T m P := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.referenceHistoryTotal, OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer

66. theorem OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer_ne_zero line 1108

    Source documentation

    In particular division by the reference normalization is legitimate.

    theorem referencePlanNormalizer_ne_zero {n p : ℕ} (T : PrescribedTree n)
        (m : Fin (n+1) → ℝ) (hm : StrictMono m) (hnonneg : ∀ j, 0 ≤ m j)
        {s : Fin (p+1) → Leaf T} (P : ReferencePlan T s) :
        referencePlanNormalizer T m P ≠ 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer