OAI/Probability/FKMaps/CoreMetric.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Inventory.Core.matching line 14
2. def OAI.FKCRT.Inventory.Core.rotation line 19
3. def OAI.FKCRT.Inventory.Core.graph line 22
4. instance OAI.FKCRT.Inventory.Core.(instance at line 25) line 25
5. def OAI.FKCRT.Inventory.Core.entry line 27
6. def OAI.FKCRT.Inventory.Core.increment line 30

   Source documentation

   Entry-to-child-corner distance in the actual isolated core map.

   def increment (c : Core) (j : Fin c.val.length) : ℕ :=
   …

   Mentions: OAI.FKCRT.Inventory.Core

7. lemma OAI.FKCRT.Inventory.Core.distance_le line 34
8. lemma OAI.FKCRT.Inventory.Core.increment_le line 44
9. def OAI.FKCRT.Inventory.coreIncrement line 51

   Source documentation

   Spine records index the chosen child from the right. Impossible arities and slot labels are totalized by zero and never sampled by the actual law.

   def coreIncrement (z : ℕ×ℕ) (a : CoreLabel) : ℝ :=
   …

   Mentions: OAI.FKCRT.Inventory.CoreLabel

10. lemma OAI.FKCRT.Inventory.coreIncrement_nonneg line 57
11. lemma OAI.FKCRT.Inventory.coreIncrement_bound line 62
12. lemma OAI.FKCRT.Inventory.coreIncrement_integrable line 72
13. lemma OAI.FKCRT.Inventory.coreIncrement_mean_bound line 77
14. def OAI.FKCRT.Inventory.metricMean line 85

    Source documentation

    The source block-distance mean; finiteness uses only offspring variance.

    def metricMean (P : Parameters) : ℝ :=
    …

    Mentions: OAI.FKCRT.Inventory.Parameters

15. lemma OAI.FKCRT.Inventory.metricMean_integrable line 88
16. lemma OAI.FKCRT.Inventory.metricMean_nonneg line 93
17. theorem OAI.FKCRT.Inventory.actual_uniform_metric_spine line 98

    Source documentation

    Actual all-core labels satisfy the previously proved marked finite-variance uniform ancestral law, not a bounded-size or exponential-moment substitute.

    theorem actual_uniform_metric_spine (P : Parameters)
        {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
        {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B μ) {ε : ℝ} (hε : 0<ε) :
        Tendsto (fun n => ((actualOffspring P).markedCodeLaw
          (fun k => (CoreLabel.markLaw P k).toMeasure) n).real {x | ∃ v : Fin (2*n+1),
            ε*Real.sqrt ((2*n+1:ℕ):ℝ) < |markedSpineSum coreIncrement x.1 v.isLt.le x.2-
              metricMean P*height x.1.val v.val|}) atTop (𝓝 0) :=
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.coreIncrement, OAI.FKCRT.Inventory.metricMean

18. lemma OAI.FKCRT.Inventory.vertex_perm_apply line 121
19. lemma OAI.FKCRT.Inventory.StackMatching.reachable_first line 124
20. theorem OAI.FKCRT.Inventory.StackMatching.connected line 137

    Source documentation

    A genuine successful matching's cyclic tour connects its actual rotation vertices by original edges; disconnected-distance default values never enter any isolated-core metric.

    theorem StackMatching.connected [Fintype α] {w : α→TypedLetter} {l : List α}
        (M : StackMatching w l) (hn : l.Nodup) (hall : ∀ x,x∈l) (hne : l≠[]) :
        (dartGraph M.mate (l.formPerm*turns M.first)).Connected := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching

21. lemma OAI.FKCRT.Inventory.Core.graph_connected line 166
22. lemma OAI.FKCRT.Inventory.Core.distance_eq_nat line 173
23. lemma OAI.FKCRT.Inventory.StackMatching.distance_comm line 189
24. theorem OAI.FKCRT.Inventory.StackMatching.core_distance_eq line 195

    Source documentation

    Fix one canonical isolated core matching; deleting all its successful corner intervals gives its distances simultaneously at every pair of darts.

    theorem StackMatching.core_distance_eq {w : α→TypedLetter}
        (l : List (α×List α)) (M : StackMatching w (dartInsert l))
        (hn : (dartInsert l).Nodup)
        (he : ∀ c∈l,stackTypedRun (c.2.map w) []=some [])
        (D : StackMatching w (l.map Prod.fst)) (x y : α)
        (hx : x∈l.map Prod.fst) (hy : y∈l.map Prod.fst) :
        M.distance x y=D.distance x y := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.dartInsert, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

25. theorem OAI.FKCRT.Inventory.StackMatching.interval_distance_sum line 207

    Source documentation

    Exact gate additivity in the actual full graph with the inserted component replaced only by its genuine isolated matching.

    theorem StackMatching.interval_distance_sum {w : α→TypedLetter}
        (u L z : List α) (a b : α) (R : List α)
        (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R)
        (D : StackMatching w (a::L)) (x y : α) (hx : x∈a::L) (hy : y∉a::L) :
        M.distance y x=M.distance y b+D.distance a x := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map, OAI.FKCRT.Inventory.D

26. theorem OAI.FKCRT.Inventory.StackMatching.corner_distance_sum line 227

    Source documentation

    One recursive step of the source pole-distance identity, with literal core and child darts and all other children still present.

    theorem StackMatching.corner_distance_sum {w : α→TypedLetter}
        (l : List (α×List α)) (M : StackMatching w (dartInsert l))
        (hn : (dartInsert l).Nodup)
        (he : ∀ c∈l,stackTypedRun (c.2.map w) []=some [])
        (D : StackMatching w (l.map Prod.fst))
        (u L z : List α) (a b : α) (R : List α)
        (hword : dartInsert l=u++((a::L)++z))
        (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R)
        (Q : StackMatching w (a::L)) (x r : α) (hx : x∈a::L)
        (hr : r∈l.map Prod.fst) (hrv : r∉a::L) (hb : b∈l.map Prod.fst) :
        M.distance r x=D.distance r b+Q.distance a x := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.dartInsert, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D, OAI.FKCRT.Inventory.StackMatching.map

27. abbrev OAI.FKCRT.Inventory.oneLinkCore line 258
28. def OAI.FKCRT.Inventory.oneLinkMatching line 260
29. lemma OAI.FKCRT.Inventory.oneLink_rotation line 269
30. lemma OAI.FKCRT.Inventory.oneLink_mate line 275
31. lemma OAI.FKCRT.Inventory.oneLink_increment line 279
32. lemma OAI.FKCRT.Inventory.coreIncrement_oneLink line 295
33. lemma OAI.FKCRT.Inventory.coreIncrement_mean_pos line 301
34. theorem OAI.FKCRT.Inventory.metricMean_pos line 322

    Source documentation

    Strict positivity follows from the positive-mass one-link block and its nontrivial corner, not from an assumed metric scaling constant.

    theorem metricMean_pos (P : Parameters) : 0 < metricMean P := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.metricMean

35. def OAI.FKCRT.Inventory.CoreTree.Dart line 346

    Source documentation

    Literal darts of the recursively substituted word; no quotient identifies any darts of distinct blocks.

    def Dart : CoreTree → Type
      | .leaf => Empty
      | .branch c ts => Fin c.val.length ⊕ (Σ i : Fin c.val.length, Dart (ts i))

    Mentions: OAI.FKCRT.Inventory.CoreTree

36. instance OAI.FKCRT.Inventory.CoreTree.(instance at line 350) line 350
37. instance OAI.FKCRT.Inventory.CoreTree.(instance at line 357) line 357
38. def OAI.FKCRT.Inventory.CoreTree.dartLabel line 359
39. def OAI.FKCRT.Inventory.CoreTree.childDart line 364
40. def OAI.FKCRT.Inventory.CoreTree.coreDart line 367
41. lemma OAI.FKCRT.Inventory.CoreTree.childDart_injective line 370
42. lemma OAI.FKCRT.Inventory.CoreTree.coreDart_injective line 375
43. def OAI.FKCRT.Inventory.CoreTree.darts line 378
44. def OAI.FKCRT.Inventory.CoreTree.dartCorners line 383
45. lemma OAI.FKCRT.Inventory.CoreTree.darts_branch line 387
46. lemma OAI.FKCRT.Inventory.CoreTree.darts_word line 391
47. lemma OAI.FKCRT.Inventory.CoreTree.darts_mem line 401
48. lemma OAI.FKCRT.Inventory.CoreTree.darts_nodup line 412
49. def OAI.FKCRT.Inventory.CoreTree.matching line 437
50. lemma OAI.FKCRT.Inventory.CoreTree.child_empty line 440
51. lemma OAI.FKCRT.Inventory.CoreTree.core_darts line 446
52. theorem OAI.FKCRT.Inventory.CoreTree.core_distance line 451

    Source documentation

    Exact original graph metric on core darts before/after all substitutions.

    theorem core_distance (c : Core) (ts : Fin c.val.length→ CoreTree)
        (i j : Fin c.val.length) :
        (branch c ts).matching.distance (coreDart ts i) (coreDart ts j)=c.matching.distance i j := by
    …

    Mentions: OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.CoreTree.coreDart

53. lemma OAI.FKCRT.Inventory.dartInsert_append line 483
54. theorem OAI.FKCRT.Inventory.corner_complement_head line 489

    Source documentation

    The entry dart following a child interval is exactly the next isolated core dart in cyclic order, including the last-slot wrap to the root.

    theorem corner_complement_head (A B : List (α×List α)) (d : α) (v : List α)
        (hn : (dartInsert (A++(d,v)::B)).Nodup) :
        ∃ R,dartInsert B++(dartInsert A++[d])=
          ((A++(d,v)::B).map Prod.fst).formPerm d::R := by
    …

    Mentions: OAI.FKCRT.Inventory.dartInsert

55. theorem OAI.FKCRT.Inventory.StackMatching.selected_corner_distance line 520

    Source documentation

    The exact selected-slot gate formula, with the cyclic successor computed in the original isolated core order.

    theorem StackMatching.selected_corner_distance {w : α→TypedLetter}
        (A B : List (α×List α)) (d a : α) (L : List α)
        (M : StackMatching w (dartInsert (A++(d,a::L)::B)))
        (hn : (dartInsert (A++(d,a::L)::B)).Nodup)
        (he : ∀ p∈A++(d,a::L)::B,stackTypedRun (p.2.map w) []=some [])
        (D : StackMatching w ((A++(d,a::L)::B).map Prod.fst))
        (Q : StackMatching w (a::L)) (r x : α)
        (hr : r∈(A++(d,a::L)::B).map Prod.fst) (hrv : r∉a::L) (hx : x∈a::L) :
        M.distance r x=D.distance r (((A++(d,a::L)::B).map Prod.fst).formPerm d)+Q.distance a x := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.dartInsert, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D, OAI.FKCRT.Inventory.StackMatching.map

56. def OAI.FKCRT.Inventory.CoreTree.nextSlot line 546
57. lemma OAI.FKCRT.Inventory.CoreTree.core_next line 549
58. theorem OAI.FKCRT.Inventory.CoreTree.child_distance_sum line 555

    Source documentation

    Exact all-edge ancestor step for arbitrary literal child darts.

    theorem child_distance_sum (c : Core) (ts : Fin c.val.length → CoreTree)
        (i r : Fin c.val.length) (a x : (ts i).Dart) (L : List (ts i).Dart)
        (hhead : (ts i).darts=a::L) :
        (branch c ts).matching.distance (coreDart ts r) (childDart ts i x)=
          c.matching.distance r (nextSlot c i)+(ts i).matching.distance a x := by
    …

    Mentions: OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.CoreTree.Dart, OAI.FKCRT.Inventory.CoreTree.darts, OAI.FKCRT.Inventory.CoreTree.coreDart, OAI.FKCRT.Inventory.CoreTree.childDart, OAI.FKCRT.Inventory.CoreTree.nextSlot