OAI/AlgebraicGeometry/CharacterVarieties/Foundation/RoutedFamilies.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.variable_connected line 30

   Source documentation

   Boundary connectedness for mixed replacement patches with different numbers of events. The only closure equation is exterior lane sewing.

   theorem variable_connected (t : Fin (m+1)) (j : Fin (n t+1)) :
       (((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext.SameCycle
         (((family P).complete e he).sideOf (familyEnd k 0 ((C 0).node 0)))
         (((family P).complete e he).sideOf (familyEnd k t ((C t).node j))) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd

2. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.variable_boundary_count line 50

   Source documentation

   Exhaustive local parent-germ coverage closes the whole named facet, not merely an embedded selected path. Coverage is a finite table proposition; it is deliberately not asserted for arbitrary unverified templates.

   theorem variable_boundary_count (u : F)
       (hstart : facet (((family P).complete e he).sideOf (familyEnd k 0 ((C 0).node 0)))=u)
       (cover : ∀ z, facet z=u → ∃ t j,
         ((family P).complete e he).sideOf (familyEnd k t ((C t).node j))=z) :
       IntegralCharacterVarieties.FiniteCycles.componentCount
         (((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext facet u=1 := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd, OAI.IntegralCharacterVarieties.FiniteCycles.componentCount

3. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.variable_boundary_count_germs line 65

   Source documentation

   The check needed on local templates is just exhaustion by parent corners. Both side-germ occurrences are allowed, and the corner permutation carries the input to its mate. Repeated facet names are not erased.

   theorem variable_boundary_count_germs (u : F)
       (hstart : facet (((family P).complete e he).sideOf (familyEnd k 0 ((C 0).node 0)))=u)
       (cover : ∀ t (x : LocalEnd (V t) (k t)),
         facet (((family P).complete e he).sideOf (familyEnd k t x))=u →
         ∃ j, x=(C t).node j ∨ x=localMate ((C t).node j)) :
       IntegralCharacterVarieties.FiniteCycles.componentCount
         (((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext facet u=1 := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate, OAI.IntegralCharacterVarieties.FiniteCycles.componentCount

4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.SecondaryNames line 102

   Source documentation

   All nonprincipal facet names remain explicit and may repeat. The new disk parent is a separate name, not a replacement or quotient of old facet names.

   def Kind.SecondaryNames (F : Type) : Kind → Type
     | .passage m _ => Fin m → F
     | .splitting a b c _ => F × (Fin a → F) × (Fin b → F) × (Fin c → F)

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

5. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.freshDecoration line 106
6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.fresh_color_none line 113

   Source documentation

   No lower facet, even a repeated one, can be mistaken for the fresh parent in any permitted passage, split, or merge table.

   lemma Kind.fresh_color_none (k : Kind) (d : k.SecondaryNames F)
       (z : (p : k.table.Port) × Option (k.table.Child p)) :
       (k.freshDecoration d).color z=none ↔ z=⟨k.input,none⟩ ∨ z=⟨k.output,none⟩ := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

7. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.patches line 142
8. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.In line 143
9. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.Out line 144
10. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.wiring line 150
11. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.colors line 152
12. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.assembly line 154
13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.color_mate line 156
14. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.parent_boundary_count line 168

    Source documentation

    Unequal-length galleries of ANY permitted event kinds, with all explicit old child names and split branches retained, close to one fresh parent boundary. No local exhaustion hypothesis is left: it follows from the tables.

    theorem parent_boundary_count : IntegralCharacterVarieties.FiniteCycles.componentCount
        (assembly n k ha e he labels hd).vertexAssembly.corners.boundaryNext
        ((wiring n k ha e he).coloredFacet (colors n k labels)) none=1 := by
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.assembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.Cyclic.colors

15. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate line 197

    Source documentation

    Verified local data, with port tables and parent corner exhaustion.

    structure ParentTemplate (F : Type) where
    …

16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.gallery line 218

    Source documentation

    Full gallery; no side branches have been dropped.

    noncomputable def gallery {l : ℕ} (k : Fin (l+1) → Kind)
        (ha : ∀ j : Fin l, (k j.castSucc).arity (k j.castSucc).output=
          (k j.succ).arity (k j.succ).input)
        (d : ∀ v, (k v).SecondaryNames F) : ParentTemplate F where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate

17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.complementColor line 245
18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.complementColor_none line 248
19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.complementary line 252
20. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Recipe line 272
21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Recipe.template line 279
22. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.templates line 290
23. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.kinds line 291
24. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.patches line 292
25. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.colors line 293
26. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.wiring line 300
27. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.assembly line 302
28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.color_mate line 304
29. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.parent_boundary_count line 314

    Source documentation

    Every finite cyclic mixture of the ordinary/split/merge gallery and nonregular complementary templates has one full fresh-parent boundary. All other entire ports are still sewn by the original arbitrary exterior e; no side-germ or old facet label has been discarded by this theorem.

    theorem parent_boundary_count : IntegralCharacterVarieties.FiniteCycles.componentCount
        (assembly R e he hd).vertexAssembly.corners.boundaryNext
        ((wiring R e he).coloredFacet (colors R)) none=1 := by
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.assembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.colors

30. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.distinguished line 335
31. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn line 338
32. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut line 339
33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew line 342

    Source documentation

    Sewing consumes exactly each designated parent interface once.

    noncomputable def sew (rest : OtherIn a ≃ OtherOut b) :
        ((t : Fin (m+1)) × A t) ≃ ((t : Fin (m+1)) × B t) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut

34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew_parent line 347
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew_other line 356
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.rotate_mod line 365
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew_route line 377
38. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.input line 390
39. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.output line 391
40. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.exterior line 393
41. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.parent_boundary_count line 402

    Source documentation

    The exterior sewing is constructed, not hypothesized; cyclic closure of all mixed parent routes and exhaustion of this facet follow. rest retains every exposed old/branch port, as CyclicInterface.sew_other proves.

    theorem parent_boundary_count : IntegralCharacterVarieties.FiniteCycles.componentCount
        (Cyclic.assembly R (exterior R rest) he hd).vertexAssembly.corners.boundaryNext
        ((Cyclic.wiring R (exterior R rest) he).coloredFacet (Cyclic.colors R)) none=1 :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.assembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.exterior, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Cyclic.colors

42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.forward line 419
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.parent_range_iff line 426
44. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.recover line 438

    Source documentation

    Restriction to all residual occurrences is an invertible matching, not a choice of matching with the right cardinality.

    noncomputable def recover : OtherIn a ≃ OtherOut b where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut

45. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew_recover line 447

    Source documentation

    Exhaustiveness of the concrete cyclic sewing: every original matching with the given parent route is returned literally, also off that route.

    theorem sew_recover : sew a b (recover a b e route)=e := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.recover

46. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.recover_sew line 457

    Source documentation

    No arbitrary complement choice survives in the data: the original old matching on every branch is recovered from its sewing.

    theorem recover_sew (rest : OtherIn a ≃ OtherOut b) :
        recover a b (sew a b rest) (sew_parent a b rest)=rest := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.recover, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew_parent

47. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.Routed line 469

    Source documentation

    All old exterior matchings with the matching parent cycle, including every separate branch occurrence. This is a subtype of finite interface data.

    def Routed := {e : ((t : Fin (m+1)) × A t) ≃ ((t : Fin (m+1)) × B t) //
    …

48. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.parametrization line 473

    Source documentation

    The concrete producer is exhaustive and has an explicit inverse. Neither surviving external side germs nor their previous matchings are quotient out.

    noncomputable def parametrization : (OtherIn a ≃ OtherOut b) ≃ Routed a b where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.Routed

49. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.compatible_iff line 485

    Source documentation

    Literally all seam equations split into their cyclic parent interface and their unchanged old branch equations. The relation may encode arities, ordered graded names or equality of coefficient-ring transport matrices.

    theorem compatible_iff (rest : OtherIn a ≃ OtherOut b)
        (R : ((t : Fin (m+1)) × A t) → ((t : Fin (m+1)) × B t) → Prop) :
        (∀ p, R p (sew a b rest p)) ↔
          (∀ t, R (distinguished a t) (distinguished b ((finRotate (m+1)).symm t))) ∧
          (∀ p : OtherIn a, R p.val (rest p).val) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherIn, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.OtherOut, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.sew, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.distinguished

50. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Recipe.finiteInput line 512
51. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Recipe.finiteOutput line 514
52. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.In line 521
53. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Out line 522
54. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Residual line 523
55. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Index line 527

    Source documentation

    Finite rank-array choices and finite old-branch matchings together, with NO identification of occurrences sharing their facet name.

    abbrev Index := (j : J) × Residual m R j

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Residual

56. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.finiteIn line 528
57. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.finiteOut line 531
58. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.finiteResidual line 534
59. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.finiteIndex line 542
60. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.produce line 544
61. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.exhaustive line 549

    Source documentation

    Every original routed matching appears LITERALLY in the finite family.

    theorem exhaustive (j : J) (e : In m R j ≃ Out m R j)
        (route : ∀ t, e.symm (CyclicInterface.distinguished (ParentTemplate.Sewn.output (R j)) t)=
          CyclicInterface.distinguished (ParentTemplate.Sewn.input (R j))
            (finRotate (m j+1) t)) :
        ∃ i : Index m R, produce m R i=⟨j,e⟩ := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.In, OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Out, OAI.IntegralCharacterVarieties.OccurrenceIncidence.CyclicInterface.distinguished, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.output, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ParentTemplate.Sewn.input, OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Index, OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.produce