TwoPointLabeling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.exists_equiv_two_points line 11
Source documentation
Finite labeling can pin both protected leaves without changing the full leaf set; this is not an assumed identification of the two tree experiments.
```
lemma exists_equiv_two_points {α β : Type} [Fintype α] [Fintype β]
    (hcard : Fintype.card α=Fintype.card β) (a b : α) (c d : β)
    (hab : a≠b) (hcd : c≠d) : ∃ e : α ≃ β, e a=c ∧ e b=d := by
…
```
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFrame_canonical_labeling line 28
Source documentation
Every split frame has a canonical Option/Fin dictionary labeling with none and the FIRST inserted label at the protected corresponding twin leaves.
```
lemma splitFrame_canonical_labeling {n : ℕ} (S : PrescribedTree n) (r d t : ℕ)
    (b : S.Leaf) (hcard : Fintype.card (splitFrame S r d).Leaf=t+2) :
    ∃ q : Option (Fin (t+1)) ≃ (splitFrame S r d).Leaf,
      q none=splitFrameLeaf S r d 0 b ∧
      q (some (Fin.last t))=splitFrameLeaf S r d 1 b := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.splitFrame, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitFrameLeaf