OAI/Algebra/GroupRing/TypeWeights.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight line 14

   Source documentation

   The conditional joint-incidence table in the manuscript, before excluding cancellation. Arguments here are the two outgoing letters at the vertex.

   def jointWeight : Letter → Letter → ℝ
     | .inl _, .inl _ => 1/129
     | .inl _, .inr _ => 129/16513
     | .inr _, .inl _ => 129/16513
     | .inr _, .inr _ => 1

2. def OAI.TorsionFreeZeroDivisors.TypeWeights.turnWeight line 20
3. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight_signed line 24

   Source documentation

   The finite geometric incidence table equals the analytic table, without changing the given inverse pairing or field.

   theorem jointWeight_signed (t u : Signed) :
       jointWeight (inverse (signedLetter t)) (signedLetter u) = WordEstimate.baseWeight t u := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.WordEstimate.baseWeight

4. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.turnWeight_signed line 33
5. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight_comm line 42
6. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.joint_countB line 46

   Source documentation

   At an internal chain vertex of side B this is an exact count.

   theorem joint_countB (rep : ℕ) (a b : Letter) (hab : a ≠ b) :
       (Fintype.card {v : VertexB rep // a ∈ outgoingB v ∧ b ∈ outgoingB v} : ℝ) =
         (Fintype.card (VertexB rep) : ℝ) * (129/16513) * jointWeight a b := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight

7. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.joint_countA_le line 74

   Source documentation

   The A-side conditional table is dominated by the B-side table, with the source's factor 1/2 for distinct extras.

   theorem joint_countA_le (rep : ℕ) (a b : Letter) (hab : a ≠ b) :
       (Fintype.card {v : VertexA rep // a ∈ outgoingA v ∧ b ∈ outgoingA v} : ℝ) ≤
         (Fintype.card (VertexA rep) : ℝ) * (129/16513) * jointWeight a b := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight

8. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.internal_countB line 105
9. theorem OAI.TorsionFreeZeroDivisors.TypeWeights.internal_countA line 110
10. def OAI.TorsionFreeZeroDivisors.StageRealization.allowed line 124

    Source documentation

    Actual vertex carriers: all outgoing template ports must be available; pin imposes exactly the prescribed images, not extra random conditions.

    def allowed (Γ : PortGraph PV PD) (plabel : PD → T) (outgoing : TV → Finset T)
        (pin : PV → Option TV) (v : PV) : Finset TV :=
    …

11. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_ports line 130
12. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_card_le line 138
13. theorem OAI.TorsionFreeZeroDivisors.StageRealization.pinned_card_le line 144
14. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_turn_le line 155

    Source documentation

    A turn at an internal chain vertex restricts its image to the joint carrier. This does not assume independence of consecutive turns.

    theorem allowed_turn_le (Γ : PortGraph PV PD) (plabel : PD → T)
        (outgoing : TV → Finset T) (pin : PV → Option TV) (v : PV) (a b : PD)
        (ha : Γ.origin a = v) (hb : Γ.origin b = v) :
        (allowed Γ plabel outgoing pin v).card ≤
          Fintype.card {x : TV // plabel a ∈ outgoing x ∧ plabel b ∈ outgoing x} := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.allowed

15. def OAI.TorsionFreeZeroDivisors.StageRealization.realizations line 168

    Source documentation

    Concrete realization count for one fixed immersed labeling.

    def realizations (Γ : PortGraph PV PD) (plabel : PD → T)
        (outgoing : TV → Finset T) (pin : PV → Option TV) (bar : T → T)
        (r : Matching (label outgoing) bar) : ℕ :=
    …

16. theorem OAI.TorsionFreeZeroDivisors.StageRealization.fixed_label_bound line 177

    Source documentation

    Finite, exact form of the source fixed-label first moment. cost v is a literal upper bound for carrier size; the matching estimate is proved above.

    theorem fixed_label_bound (Γ : PortGraph PV PD) (plabel : PD → T)
        (outgoing : TV → Finset T) (pin : PV → Option TV) (bar : T → T)
        (hbar : ∀ t, bar t ≠ t) (himm : Function.Injective (fun d => (Γ.origin d,plabel d)))
        (N d R : ℕ) (h2 : 2 ≤ d) (hR : 0 < R)
        (hd : ∀ v, Nat.card {e : Dart outgoing // origin outgoing e = v} ≤ d)
        (hsize : ∀ x : Dart outgoing,
          R + (edges Γ).card + 4*d^(2*N+1) ≤
            Nat.card {e : Dart outgoing // label outgoing e = label outgoing x})
        (hΩ : (Matching.conditioned (label := label outgoing) (bar := bar)
    …

17. def OAI.TorsionFreeZeroDivisors.StageRealization.vertexCost line 200

    Source documentation

    Source internal-turn product, retaining a finite, explicit matching error denominator instead of hiding it in o(L).

    def vertexCost (n p : ℝ) (J : Finset PV) (w : T → T → ℝ)
        (a b : PV → T) (pin : PV → Option TV) (v : PV) : ℝ :=
    …

18. theorem OAI.TorsionFreeZeroDivisors.StageRealization.product_vertexCost line 205
19. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_cost line 224

    Source documentation

    Every eligible local carrier is bounded by its actual type-table cost.

    theorem allowed_cost (Γ : PortGraph PV PD) (plabel : PD → T)
        (outgoing : TV → Finset T) (pin : PV → Option TV)
        (J : Finset PV) (a b : PV → PD)
        (ha : ∀ v ∈ J, Γ.origin (a v) = v) (hb : ∀ v ∈ J, Γ.origin (b v) = v)
        (hab : ∀ v ∈ J, a v ≠ b v)
        (himm : Function.Injective (fun d => (Γ.origin d,plabel d)))
        (n p : ℝ) (w : T → T → ℝ)
        (hn : (Fintype.card TV : ℝ) ≤ n)
        (htable : ∀ t u, t ≠ u →
          (Fintype.card {x : TV // t ∈ outgoing x ∧ u ∈ outgoing x} : ℝ) ≤ n*p*w t u) :
        ∀ v, ((allowed Γ plabel outgoing pin v).card : ℝ) ≤
          vertexCost n p J w (plabel ∘ a) (plabel ∘ b) pin v := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.allowed, OAI.TorsionFreeZeroDivisors.StageRealization.vertexCost

20. theorem OAI.TorsionFreeZeroDivisors.StageRealization.turn_product_bound line 255

    Source documentation

    Literal fixed-label bound with actual internal turns and fixed vertices, before taking logarithms or asymptotics.

    theorem turn_product_bound (Γ : PortGraph PV PD) (plabel : PD → T)
        (outgoing : TV → Finset T) (pin : PV → Option TV) (bar : T → T)
        (hbar : ∀ t, bar t ≠ t) (himm : Function.Injective (fun d => (Γ.origin d,plabel d)))
        (N d R : ℕ) (h2 : 2 ≤ d) (hR : 0 < R)
        (hd : ∀ v, Nat.card {e : Dart outgoing // origin outgoing e = v} ≤ d)
        (hsize : ∀ x : Dart outgoing,
          R + (edges Γ).card + 4*d^(2*N+1) ≤
            Nat.card {e : Dart outgoing // label outgoing e = label outgoing x})
        (hΩ : (Matching.conditioned (label := label outgoing) (bar := bar)
    …

21. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_costA line 293

    Source documentation

    The exact source A-side empirical counts instantiate the local estimate.

    theorem allowed_costA (pin : PV → Option (VertexA rep)) :
        ∀ v, ((allowed Γ plabel (@outgoingA rep) pin v).card : ℝ) ≤
          vertexCost (Fintype.card (VertexA rep)) (129/16513) J TypeWeights.jointWeight
            (plabel ∘ a) (plabel ∘ b) pin v :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.allowed, OAI.TorsionFreeZeroDivisors.StageRealization.vertexCost, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight

22. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_costB line 303

    Source documentation

    The B-side count uses its own types, not independent coordinates.

    theorem allowed_costB (pin : PV → Option (VertexB rep)) :
        ∀ v, ((allowed Γ plabel (@outgoingB rep) pin v).card : ℝ) ≤
          vertexCost (Fintype.card (VertexB rep)) (129/16513) J TypeWeights.jointWeight
            (plabel ∘ a) (plabel ∘ b) pin v :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.allowed, OAI.TorsionFreeZeroDivisors.StageRealization.vertexCost, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight

23. theorem OAI.TorsionFreeZeroDivisors.StageRealization.mean_product line 315

    Source documentation

    Exact expectation factorization for the two independently chosen side matchings. No independence of edges within either matching is used.

    theorem mean_product {A B : Type*} (S : Finset A) (U : Finset B)
        (f : A → ℝ) (g : B → ℝ) :
        (∑ x ∈ S, ∑ y ∈ U, f x*g y) / ((S.card : ℝ)*U.card) =
          ((∑ x ∈ S, f x)/S.card) * ((∑ y ∈ U, g y)/U.card) := by
    …

24. theorem OAI.TorsionFreeZeroDivisors.StageRealization.mean_product_le line 322

    Source documentation

    Combining the side bounds correctly counts a mixed-side stage.

    theorem mean_product_le {A B : Type*} (S : Finset A) (U : Finset B)
        (f : A → ℝ) (g : B → ℝ) (hf : ∀ x ∈ S, 0 ≤ f x) (hg : ∀ y ∈ U, 0 ≤ g y)
        (a b : ℝ) (ha : (∑ x ∈ S, f x)/S.card ≤ a)
        (hb : (∑ y ∈ U, g y)/U.card ≤ b) :
        (∑ x ∈ S, ∑ y ∈ U, f x*g y) / ((S.card : ℝ)*U.card) ≤ a*b := by
    …

25. abbrev OAI.TorsionFreeZeroDivisors.ChainSubdivision.Interior line 336
26. abbrev OAI.TorsionFreeZeroDivisors.ChainSubdivision.Vertex line 337
27. abbrev OAI.TorsionFreeZeroDivisors.ChainSubdivision.Edge line 338
28. abbrev OAI.TorsionFreeZeroDivisors.ChainSubdivision.Dart line 339
29. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.point line 341
30. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.graph line 345
31. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.reverse line 355
32. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.origin_forward line 356
33. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.origin_backward line 358
34. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.at_zero line 361
35. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.at_last line 364
36. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.at_interior line 368
37. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.back line 375

    Source documentation

    Outgoing darts at an internal vertex: the preceding edge backwards and following edge forwards, with no arbitrary choices.

    def back (v : Interior len) : Dart len := (⟨v.1,⟨v.2.val,by omega⟩⟩,true)

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.Interior, OAI.TorsionFreeZeroDivisors.ChainSubdivision.Dart

38. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.front line 376
39. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.back_origin line 378
40. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.front_origin line 381
41. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.back_ne_front line 385
42. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.at_eq_interior line 390
43. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.internal_ports line 402

    Source documentation

    Each internal vertex has precisely the two prescribed outgoing darts.

    theorem internal_ports (v : Interior len) (d : Dart len) :
        (graph len first last).origin d = .inr v ↔ d = back len v ∨ d = front len v := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.Interior, OAI.TorsionFreeZeroDivisors.ChainSubdivision.Dart, OAI.TorsionFreeZeroDivisors.ChainSubdivision.graph, OAI.TorsionFreeZeroDivisors.ChainSubdivision.back, OAI.TorsionFreeZeroDivisors.ChainSubdivision.front

44. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.card_edges line 432
45. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.card_darts line 435
46. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.card_interiors line 438
47. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.card_vertices line 442

    Source documentation

    Interior and endpoint counts are kept separate, including loop chains.

    theorem card_vertices (hpos : ∀ c, 0 < len c) :
        Fintype.card (Vertex len (V := V)) + Fintype.card C = Fintype.card V + ∑ c, len c := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.Vertex

48. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.internal line 455

    Source documentation

    The complete set of unmarked internal vertices.

    def internal : Finset (Vertex len (V := V)) := Finset.univ.image Sum.inr
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.Vertex

49. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.mem_internal line 458
50. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.card_internal line 463
51. def OAI.TorsionFreeZeroDivisors.ChainSubdivision.multiplicity line 467

    Source documentation

    Constant traversal multiplicity on each original marked chain.

    def multiplicity (m : C → ℕ) (d : Dart len) := m d.1.1
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.Dart

52. theorem OAI.TorsionFreeZeroDivisors.ChainSubdivision.multiplicity_reverse line 469