OAI/Algebra/GroupRing/TwoSideFullStage.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.TwoSideFullStage.CA line 16
  2. abbrev OAI.TorsionFreeZeroDivisors.TwoSideFullStage.CB line 17
  3. abbrev OAI.TorsionFreeZeroDivisors.TwoSideFullStage.lenA line 18
  4. abbrev OAI.TorsionFreeZeroDivisors.TwoSideFullStage.lenB line 19
  5. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.restrictA line 21
  6. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.restrictB line 23
  7. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.indexA line 26
  8. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.indexB line 27
  9. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.binsA line 30
  10. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.binsB line 48
  11. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.joinBlock line 65
  12. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.joinBlock_bijective line 71
  13. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.blockEquiv line 102
  14. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.bin_sum line 104
  15. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.sideA line 119
  16. def OAI.TorsionFreeZeroDivisors.TwoSideFullStage.sideB line 125
  17. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.exponential_fusion line 134
  18. theorem OAI.TorsionFreeZeroDivisors.TwoSideFullStage.mean_bound line 144

    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))
…
  19. theorem OAI.TorsionFreeZeroDivisors.MatchingGraphs.exists_typed_large_girth line 183

    Source documentation

    Nonemptiness of the exact typed matching family conditioned on girth. The numerical hypothesis is an explicit finite-size bound, not a new standing hypothesis for the main existential theorem.

    theorem exists_typed_large_girth (origin : D → V) (label : D → T) (bar : T → T)
    (Γ₀ : PortGraph V D) (ho : Γ₀.origin = origin)
    (hlabel : ∀ f, label (Γ₀.reverse f) = bar (label f))
    (d N : ℕ) (h2 : 2 ≤ d)
    (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
    (hbig : ∀ x, 4*d^(2*N+1) < Nat.card {e : D // label e = label x}) :
    ∃ Γ : PortGraph V D, Γ.origin = origin ∧
      (∀ f, label (Γ.reverse f) = bar (label f)) ∧
      (N : ℕ∞) ≤ Γ.subdivision.egirth := by
…
  20. abbrev OAI.TorsionFreeZeroDivisors.TypedGraphs.Dart line 231

    Source documentation

    The source's outgoing half-edges, preserving their basepoints and letters.

    abbrev Dart := {e : V × Letter // e.2 ∈ outgoing e.1}
  21. def OAI.TorsionFreeZeroDivisors.TypedGraphs.origin line 232
  22. def OAI.TorsionFreeZeroDivisors.TypedGraphs.label line 233
  23. def OAI.TorsionFreeZeroDivisors.TypedGraphs.reverse line 235
  24. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.reverse_involutive line 239
  25. def OAI.TorsionFreeZeroDivisors.TypedGraphs.matching line 246
  26. def OAI.TorsionFreeZeroDivisors.TypedGraphs.originFiber line 253

    Source documentation

    An origin fibre is exactly the prescribed outgoing type.

    def originFiber (v : V) : {e : Dart outgoing // origin outgoing e = v} ≃
    {t : Letter // t ∈ outgoing v} where
…

    Mentions: OAI.TorsionFreeZeroDivisors.TypedGraphs.Dart, OAI.TorsionFreeZeroDivisors.TypedGraphs.origin

  27. def OAI.TorsionFreeZeroDivisors.TypedGraphs.labelFiber line 266

    Source documentation

    A letter fibre is exactly its empirical carrier set on this side.

    def labelFiber (t : Letter) : {e : Dart outgoing // label outgoing e = t} ≃
    {v : V // t ∈ outgoing v} where
…

    Mentions: OAI.TorsionFreeZeroDivisors.TypedGraphs.Dart, OAI.TorsionFreeZeroDivisors.TypedGraphs.label

  28. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.origin_card line 278
  29. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.label_card line 283
  30. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.origin_label_injective line 290

    Source documentation

    No label can leave its basepoint twice: this is literally the immersion into the rose, not a simplicity assumption on the graph.

    theorem origin_label_injective : Function.Injective
    (fun e : Dart outgoing => (origin outgoing e,label outgoing e)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.TypedGraphs.Dart, OAI.TorsionFreeZeroDivisors.TypedGraphs.origin, OAI.TorsionFreeZeroDivisors.TypedGraphs.label

  31. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.exists_conditioned line 295
  32. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.conditionedA_nonempty line 320

    Source documentation

    The actual prescribed A-side graph space has nonzero cardinality.

    theorem conditionedA_nonempty (rep N : ℕ) (hsize : 4*132^(2*N+1) < 4260354*rep) :
    (Matching.conditioned (label := label (@outgoingA rep)) (bar := inverse)
…

    Mentions: OAI.TorsionFreeZeroDivisors.TypedGraphs.label

  33. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.conditionedB_nonempty line 328
  34. def OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L line 343

    Source documentation

    The source logarithmic girth, including its specified constant c=1/100.

    def L (n : ℕ) : ℕ := ⌊Real.log n / 100⌋₊
  35. def OAI.TorsionFreeZeroDivisors.GirthAsymptotics.exclusion line 345

    Source documentation

    Exclusion cost for the faithful threefold port subdivision.

    def exclusion (n : ℕ) : ℕ := 4 * 132 ^ (6 * L n + 1)

    Mentions: OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L

  36. theorem OAI.TorsionFreeZeroDivisors.GirthAsymptotics.log132_lt line 347
  37. theorem OAI.TorsionFreeZeroDivisors.GirthAsymptotics.exclusion_bound line 357
  38. theorem OAI.TorsionFreeZeroDivisors.GirthAsymptotics.exclusion_ratio line 382
  39. theorem OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L_tendsto line 397
  40. theorem OAI.TorsionFreeZeroDivisors.GirthAsymptotics.eventual_small line 404