OAI/Algebra/GroupRing/RealizationTransport.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.RealizationTransport.restrict line 20

    Source documentation

    Restriction needs only injectivity, not a bijection onto the whole image. In particular, inactive marked vertices are never carried into a stage.

    def restrict (Q : PortGraph QV QD) (fv : QV ↪ PV) (fd : QD ↪ PD)
    (ho : ∀ d,fv (Q.origin d)=Γ.origin (fd d))
    (hr : ∀ d,fd (Q.reverse d)=Γ.reverse (fd d)) (pin' : QV → Option TV)
    (hp : ∀ v y,pin' v=some y → pin (fv v)=some y) :
    Embedding Q (plabel ∘ fd) outgoing pin' bar r where
…

    Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding

  2. def OAI.TorsionFreeZeroDivisors.RealizationTransport.congrLabel line 33

    Source documentation

    Change the displayed port labeling by a literal pointwise equality.

    def congrLabel (label' : PD → T) (hl : ∀ d,label' d=plabel d) :
    Embedding Γ label' outgoing pin bar r where
…

    Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding

  3. def OAI.TorsionFreeZeroDivisors.ActualStageRealization.word line 58

    Source documentation

    The actual signed labels, at every position of every active chain.

    def word (label : D → Types.Letter) : ComparedBlocks.Position len → WordEstimate.Letter :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position, OAI.TorsionFreeZeroDivisors.WordEstimate.Letter

  4. lemma OAI.TorsionFreeZeroDivisors.ActualStageRealization.index_mem line 61
  5. lemma OAI.TorsionFreeZeroDivisors.ActualStageRealization.label_eq line 69
  6. def OAI.TorsionFreeZeroDivisors.ActualStageRealization.embedding line 86

    Source documentation

    An actual sampled graph embedding yields the exact stage realization counted by the conditional-matching first moment.

    def embedding (label : D → Types.Letter)
    (hl : ∀ d,label (Γ.reverse d)=Types.inverse (label d))
    (e : RealizationTransport.Embedding Γ label outgoing pin Types.inverse r)
    (pin' : StageSubgraphs.ActiveV (S) (ListStageExponents.mult (S) paths) j → Option TV)
    (hp : ∀ v y,pin' v=some y → pin v.val=some y) :
    RealizationTransport.Embedding (Q)
      (ChainRealization.label len (StageExpectation.readWord len (word Γ mark h2 paths j label)))
      outgoing (ChainRealization.pin len pin') Types.inverse r := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.Types.inverse, OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveV, OAI.TorsionFreeZeroDivisors.ListStageExponents.mult, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.StageExpectation.readWord, OAI.TorsionFreeZeroDivisors.ActualStageRealization.word, OAI.TorsionFreeZeroDivisors.ChainRealization.pin

  7. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.signed_inverse line 116
  8. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.signed_choice line 120
  9. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.weight_pos line 125
  10. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.block_weight_pos line 133
  11. def OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.bins line 146
  12. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.mem_bin line 150
  13. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.fullWords_of_comparing line 155
  14. def OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.globalWord line 172
  15. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.immersed line 175
  16. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.comparing line 196
  17. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.feasible line 213
  18. lemma OAI.TorsionFreeZeroDivisors.ActualStageFeasibility.fullWords_mem line 226
  19. abbrev OAI.TorsionFreeZeroDivisors.StagePartition.CA line 250
  20. abbrev OAI.TorsionFreeZeroDivisors.StagePartition.CB line 251
  21. abbrev OAI.TorsionFreeZeroDivisors.StagePartition.lenA line 252
  22. abbrev OAI.TorsionFreeZeroDivisors.StagePartition.lenB line 253
  23. def OAI.TorsionFreeZeroDivisors.StagePartition.restrictA line 255
  24. def OAI.TorsionFreeZeroDivisors.StagePartition.restrictB line 257
  25. def OAI.TorsionFreeZeroDivisors.StagePartition.indexA line 260
  26. def OAI.TorsionFreeZeroDivisors.StagePartition.indexB line 261
  27. theorem OAI.TorsionFreeZeroDivisors.StagePartition.binsA line 264
  28. theorem OAI.TorsionFreeZeroDivisors.StagePartition.binsB line 282
  29. def OAI.TorsionFreeZeroDivisors.StagePartition.joinBlock line 299
  30. theorem OAI.TorsionFreeZeroDivisors.StagePartition.joinBlock_bijective line 305
  31. def OAI.TorsionFreeZeroDivisors.StagePartition.blockEquiv line 344
  32. theorem OAI.TorsionFreeZeroDivisors.StagePartition.bin_sum line 346
  33. def OAI.TorsionFreeZeroDivisors.StagePartition.sideA line 361
  34. def OAI.TorsionFreeZeroDivisors.StagePartition.sideB line 367
  35. theorem OAI.TorsionFreeZeroDivisors.StagePartition.exponential_fusion line 376
  36. theorem OAI.TorsionFreeZeroDivisors.StagePartition.mean_bound line 386

    Source documentation

    The joint matching expectation applied to the actual fullWords projection, including cross-side comparisons. All entropy and bin costs are computed on that one global pattern.

    theorem mean_bound (cmp : Comparisons (E := E) (traversalLength len m))
…