CornerMass.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.Inventory.CoreTree.nodeIndex_injective line 13
def OAI.FKCRT.Inventory.CoreTree.nodeEquiv line 38
Source documentation
The literal preorder indexing is an equivalence, including the root.
```
def nodeEquiv (t : CoreTree) : t.Node ≃ Fin t.labels.length :=
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree
def OAI.FKCRT.Inventory.CoreTree.VertexConstant line 44
lemma OAI.FKCRT.Inventory.CoreTree.child_vertexConstant line 47
lemma OAI.FKCRT.Inventory.CoreTree.child_root_value line 60
theorem OAI.FKCRT.Inventory.CoreTree.sum_poles line 77
Source documentation
Exact original degree incidence counting. The extra preorder root has one additional root atom; no size-biased measure is postulated.
```
theorem sum_poles {A : Type*} [AddCommMonoid A] (t : CoreTree) (f : t.Dart → A)
    (hf : t.VertexConstant f) (r : A) :
    (∑ v : t.Node,((t.pole v).map f).getD r)=
      (t.rootDart.map f).getD r+∑ d : t.Dart,f d := by
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree
def OAI.FKCRT.PermutationWedge.dartVertexEquiv line 122
Source documentation
Exact quotient-graph relabelling for arbitrary finite dart carriers.
```
def dartVertexEquiv (f : α ≃ β) {p : Perm α} {q : Perm β}
    (hp : ∀ x,q (f x)=f (p x)) : Vertex p ≃ Vertex q :=
…
```
Mentions: OAI.FKCRT.PermutationWedge.Vertex
lemma OAI.FKCRT.PermutationWedge.dartVertexEquiv_apply line 126
def OAI.FKCRT.PermutationWedge.dartGraphIso line 130
lemma OAI.FKCRT.dartGraph_eq_spanning line 166
def OAI.FKCRT.matchingCanonical line 175
Source documentation
The canonical inverse word has the literal, uniquely determined stack matching edge and vertex permutations.
```
def matchingCanonical {n : ℕ} (w : SuccessfulWord n)
    (D : StackMatching w.val (List.finRange (2*(n+1)))) : CanonicalTreeMap n where
…
```
Mentions: OAI.FKCRT.SuccessfulWord, OAI.FKCRT.CanonicalTreeMap
lemma OAI.FKCRT.matchingCanonical_word line 186
lemma OAI.FKCRT.matchingCanonical_eq line 193
theorem OAI.FKCRT.matching_rooted_intertwine line 201
Source documentation
The quotient representative used by the main statement is a genuine rooted relabelling of the matching map, not merely a map with the same size or law.
```
theorem matching_rooted_intertwine {n : ℕ} (w : SuccessfulWord n)
    (D : StackMatching w.val (List.finRange (2*(n+1)))) :
    let M := ((rootedWordEquiv n).symm w).1
…
```
Mentions: OAI.FKCRT.SuccessfulWord, OAI.FKCRT.rootedWordEquiv
def OAI.FKCRT.Inventory.listDartEquiv line 227
lemma OAI.FKCRT.Inventory.listDartEquiv_get line 234
lemma OAI.FKCRT.Inventory.listDartEquiv_list line 238
lemma OAI.FKCRT.Inventory.listDartEquiv_labels line 245

theorem OAI.FKCRT.Inventory.StackMatching.word_intertwine line 259

Source documentation

Literal finite-word normalization simultaneously intertwines edge and vertex permutations of the original multigraph.

theorem StackMatching.word_intertwine {v : α → TypedLetter} {l : List α}
    (M : StackMatching v l) (hn : l.Nodup) (hl : ∀ d,d∈l) {n : ℕ}
    (w : FKCRT.SuccessfulWord n) (hw : l.map v=List.ofFn w.val)
    (D : StackMatching w.val (List.finRange (2*(n+1)))) :
    ∃ e : FKCRT.Dart n ≃ α,
      (∀ i,M.mate (e i)=e (D.mate i)) ∧
      (∀ i,(l.formPerm*turns M.first) (e i)=
        e (((List.finRange (2*(n+1))).formPerm*turns D.first) i)) := by
…

Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.Inventory.D, OAI.FKCRT.Dart

theorem OAI.FKCRT.Inventory.CoreTree.realized_intertwine line 301
Source documentation
The actual FK representative and the recursively glued literal map are isomorphic on their original darts, simultaneously for edges and vertices.
```
theorem realized_intertwine (t : CoreTree) {n : ℕ} (w : FKCRT.SuccessfulWord n)
    (hw : t.word=List.ofFn w.val) :
    let M := ((FKCRT.rootedWordEquiv n).symm w).1
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.rootedWordEquiv
theorem OAI.FKCRT.Inventory.CoreTree.realized_distance line 328
Source documentation
Original all-edge graph distances are preserved exactly by the finite word/core realization; no block metric is substituted.
```
theorem realized_distance (t : CoreTree) {n : ℕ} (w : FKCRT.SuccessfulWord n)
    (hw : t.word=List.ofFn w.val) :
    let M := ((FKCRT.rootedWordEquiv n).symm w).1
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.rootedWordEquiv
lemma OAI.FKCRT.Inventory.CoreTree.pole_root line 362
def OAI.FKCRT.Inventory.CoreTree.wordNodeEquiv line 365
Source documentation
Preorder nodes indexed at the true total word length.
```
def wordNodeEquiv (t : CoreTree) : t.Node ≃ Fin (t.word.length+1) :=
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree
lemma OAI.FKCRT.Inventory.CoreTree.wordNodeEquiv_root line 368
theorem OAI.FKCRT.Inventory.CoreTree.sum_nonroot_poles line 374
Source documentation
Dropping precisely the preorder root leaves the exact multiset of all original dart vertices. This is the degree measure's incidence identity.
```
theorem sum_nonroot_poles {A : Type*} [AddCancelCommMonoid A]
    (t : CoreTree) (f : t.Dart → A) (hf : t.VertexConstant f) (r : A) :
    (∑ i : Fin t.word.length,((t.pole (t.wordNodeEquiv.symm i.succ)).map f).getD r)=
      ∑ d : t.Dart,f d := by
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree
lemma OAI.FKCRT.Inventory.CoreTree.vertexConstant_of_intertwine line 386
def OAI.FKCRT.Inventory.CoreTree.realizedPole line 408
def OAI.FKCRT.Inventory.CoreTree.nonrootVertex line 412
lemma OAI.FKCRT.Inventory.CoreTree.realizedPole_some line 416
theorem OAI.FKCRT.Inventory.CoreTree.nonroot_dirac_eq line 423
Source documentation
Exact uniform nonroot-preorder mass equals original uniform dart mass. The finite root atom is cancelled, not ignored asymptotically.
```
theorem nonroot_dirac_eq (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n)
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d)) :
    let : MeasurableSpace (FKCRT.Vertex M) := ⊤
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.rotation, OAI.FKCRT.Vertex
theorem OAI.FKCRT.Inventory.CoreTree.nonrootVertex_surjective line 461
Source documentation
Every original vertex is reached by a nonroot pole, even in the presence of loops and coincident poles.
```
theorem nonrootVertex_surjective (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n)
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d)) :
    Function.Surjective (t.nonrootVertex M e) := by
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.rotation