OAI/AlgebraicGeometry/CharacterVarieties/Cutting/FreshGallery.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Ranked galleries with fresh parents

This formalizes the band reconstruction for filtered surface local systems in Integral points on character varieties of curves.

  1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.freshRank line 17

    Source documentation

    The main parent has its own occurrence label. All secondary facet labels remain available without any distinctness requirement.

    def freshRank {F : Type} (N : ℕ) (r : F → ℕ) : Option F → ℕ
  | none => N
  | some a => r a

variable {F : Type} {N : ℕ} {r : F → ℕ}
  2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_some line 23
  3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.Fresh line 28

    Source documentation

    A property of an actual ranked program, not an assumed property of a band chosen from its weaker original specification.

    def RankedChain.Fresh {a b : List (Option F)}
    (c : RankedChain (freshRank N r) none a b) : Prop :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.freshRank

  4. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.exists_fresh_congr line 36
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.fresh_trans line 44
  6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.fresh_single line 52
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.fresh_split line 57
  8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.fresh_merge line 77
  9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.fresh_passage line 97
  10. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery line 112

    Source documentation

    A finite genuine ranked gallery with a verified fresh-parent decoration at every vertex. This is constructed below, not included as a main hypothesis.

    def FreshGallery (N : ℕ) (r : F → ℕ) (a b : List F) : Prop :=
…
  11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.refl line 116
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.trans line 117
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.split line 123
  14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.merge line 127
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.passage line 131
  16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.refine_rows line 136
  17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.permutation line 161

    Source documentation

    Freshness is retained under adjacent interchanges even when names repeat. The later common-splitting argument additionally uses a no-recrossing order.

    lemma permutation {m : ℕ} (σ : Equiv.Perm (Fin m)) :
    ∀ (f : Fin m → F), N = listRank r (List.ofFn f) →
      FreshGallery N r (List.ofFn f) (List.ofFn (f ∘ σ.symm)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery

  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.equivalence line 186
  19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.rectangular line 193
  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery.two_flag_gallery line 204
  21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.Fresh line 237

    Source documentation

    Genuine secondary-name witnesses at every vertex of the walk.

    def Fresh (w : OrderedWalk none a b) : Prop :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk

  22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.fresh_cons line 241
  23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.fresh_headIdentity line 251
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.realize_fresh line 261
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.walk_fresh line 269
  26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.exists_fresh_congr line 277
  27. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.fresh_ranked_two_flag_band line 293

    Source documentation

    A rank-conservative band whose secondary parents and children are all disjoint from its fresh main parent.

    theorem fresh_ranked_two_flag_band {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
    (grid : Fin m → Fin n → F) (hp : N = ∑ i, r (row i))
    (hr : ∀ i, r (row i) = ∑ j, r (grid i j))
    (hc : ∀ j, r (col j) = ∑ i, r (grid i j)) :
    ∃ B : RealizedBand none (List.ofFn (some ∘ row)) (List.ofFn (some ∘ col)),
      (∀ v, (B.decoration v).Conservative (freshRank N r)) ∧
      (∀ v, ∃ d : (B.kind v).SecondaryNames F,
        B.decoration v = (B.kind v).freshDecoration d) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.freshRank

  28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.parentTemplate line 322

    Source documentation

    The very same band, with all branch ports and all colours. The fresh-name proof supplies exhaustion, rather than replacing the band by an unrelated cyclic template with identical endpoints.

    noncomputable def VertexTable.RealizedBand.parentTemplate (B : RealizedBand none a b)
    (h : ∀ v, ∃ d : (B.kind v).SecondaryNames F,
      B.decoration v = (B.kind v).freshDecoration d) : ParentTemplate F where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate

  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.parentTemplate_decoration line 356

    Source documentation

    Literal equality of decorations after conversion, not just equality of ranks or matching named endpoints.

    lemma VertexTable.RealizedBand.parentTemplate_decoration (B : RealizedBand none a b)
    (h : ∀ v, ∃ d : (B.kind v).SecondaryNames F,
      B.decoration v = (B.kind v).freshDecoration d) :
    (B.parentTemplate h).decoration = B.decoration := rfl
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand

  30. inductive OAI.IntegralCharacterVarieties.DirectedSort.Program line 368

    Source documentation

    A directed adjacent sorting gallery. Labels here are occurrences, not facet names. Every crossing removes an inversion in the target order.

    inductive Program : List α → List α → Type
  | refl (a : List α) : Program a a
  | step (left : List α) (a b : α) (right : List α) (h : b < a)
      {out : List α} (next : Program (left ++ b :: a :: right) out) :
      Program (left ++ a :: b :: right) out

namespace Program
variable {a b c : List α}
  31. def OAI.IntegralCharacterVarieties.DirectedSort.Program.events line 376
  32. def OAI.IntegralCharacterVarieties.DirectedSort.Program.trans line 380
  33. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.events_trans line 384
  34. def OAI.IntegralCharacterVarieties.DirectedSort.Program.reindex line 390
  35. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.events_reindex line 393
  36. def OAI.IntegralCharacterVarieties.DirectedSort.Program.prepend line 399
  37. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.events_prepend line 406
  38. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.perm line 413
  39. theorem OAI.IntegralCharacterVarieties.DirectedSort.Program.insert line 420

    Source documentation

    Insertion moves the one new label right, crossing each encountered label at most once. The recursive tail sorting never involves this new occurrence.

    theorem insert (x : α) (l : List α) (hl : l.Nodup) :
    ∃ p : Program (x :: l) (l.orderedInsert (· ≤ ·) x),
      p.events.Nodup ∧ ∀ e ∈ p.events, e.2 = x ∧ e.1 ∈ l ∧ e.1 < x := by
…

    Mentions: OAI.IntegralCharacterVarieties.DirectedSort.Program

  40. theorem OAI.IntegralCharacterVarieties.DirectedSort.Program.sort line 448

    Source documentation

    Constructive no-recrossing sort. Its event list names the actual pair of occurrences exchanged at each adjacent vertex, and contains no repetition.

    theorem sort (l : List α) (hl : l.Nodup) :
    ∃ p : Program l (l.insertionSort (· ≤ ·)), p.events.Nodup ∧
      ∀ e ∈ p.events, e.1 ∈ l ∧ e.2 ∈ l ∧ e.1 < e.2 := by
…

    Mentions: OAI.IntegralCharacterVarieties.DirectedSort.Program

  41. theorem OAI.IntegralCharacterVarieties.DirectedSort.Program.sort_equiv line 482

    Source documentation

    Sorting an arbitrary finite enumeration ends at the literal target order; no abstract change of labels is applied afterwards.

    theorem sort_equiv {m n : ℕ} (e : Fin m ≃ Fin n) :
    ∃ p : Program (List.ofFn e) (List.finRange n), p.events.Nodup := by
…

    Mentions: OAI.IntegralCharacterVarieties.DirectedSort.Program

  42. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.adjacentIndex line 502
  43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.adjacent_ofFn line 506
  44. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.adjacent line 536

    Source documentation

    Literal child lists for one adjacent event; the decoration is exactly the allowed passage table, with its full two-block identified quotient.

    def OrderedStep.adjacent (parent : F) (l : List F) (x y : F) (r : List F) :
    OrderedStep parent (l ++ x :: y :: r) (l ++ y :: x :: r) where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep

  45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.reindex line 546
  46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.adjacent_conservative line 555
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.adjacent_fresh line 561
  48. def OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked line 582

    Source documentation

    A direct realization of the displayed program, one literal passage for each recorded adjacent crossing. It does not choose an arbitrary permutation word after forgetting the no-recrossing property.

    noncomputable def ranked (f : α → F) (p : Program a b)
    (hp : N = listRank r (a.map f)) :
    RankedChain (freshRank N r) none ((a.map f).map some) ((b.map f).map some) := by
…

    Mentions: OAI.IntegralCharacterVarieties.DirectedSort.Program

  49. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked_fresh line 601
  50. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked_length line 610
  51. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.crossings line 626

    Source documentation

    Actual crossing pairs read from the literal vertex decoration, with the right (moving left) label first. Splits, merges and continuations do not add crossings. This retains occurrence labels when the colours label occurrences.

    def Decoration.crossings : {k : Kind} → Decoration k F → List (F × F)
  | .passage _ (.interchange i),d =>
    [(d.color ⟨false,some ⟨i.val+1,by omega⟩⟩,
      d.color ⟨false,some ⟨i.val,by omega⟩⟩)]
  | .passage _ .continuation,_ => []
  | .splitting _ _ _ _,_ => []

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage

  52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.adjacent_crossings line 633
  53. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.crossings line 640
  54. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.crossings_trans line 644
  55. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked_crossings line 657
  56. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked_no_recrossing line 667
  57. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.reindex line 684
  58. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.reindex_fresh line 686
  59. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.reindex_crossings line 688
  60. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery line 693

    Source documentation

    A refinement/coarsening containing no crossings, with actual fresh names.

    def CleanGallery (N : ℕ) (r : F → ℕ) (a b : List F) : Prop :=
…
  61. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery.refl line 698
  62. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery.trans line 699
  63. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery.split line 705
  64. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery.merge line 726
  65. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.CleanGallery.refine_rows line 747
  66. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery line 777

    Source documentation

    A genuinely fresh ranked gallery whose literal passage trace never repeats an ordered pair of occurrence labels.

    def ReducedGallery (N : ℕ) (r : F → ℕ) (a b : List F) : Prop :=
…
  67. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery.clean_left line 782
  68. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery.clean_right line 787
  69. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery.rectangular line 795

    Source documentation

    The finite program is built in the target column order. Each block is labelled by its occurrence, even when ranks and underlying modules coincide.

    lemma rectangular {m n : ℕ} (f : Fin m → Fin n → F)
    (hinj : Function.Injective (fun p : Fin m × Fin n => f p.1 p.2))
    (hf : N = listRank r ((List.ofFn fun i => List.ofFn (f i)).flatten)) :
    ReducedGallery N r ((List.ofFn fun i => List.ofFn (f i)).flatten)
      ((List.ofFn fun j => List.ofFn fun i => f i j).flatten) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery

  70. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ReducedGallery.two_flag_gallery line 835