OAI/Algebra/GroupRing/StageRealization.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.StageRealization.allowed_turn_table line 14

   Source documentation

   Generic table application avoids reducing the concrete projective-plane alphabet while composing the elementary cardinality bounds.

   theorem allowed_turn_table {PV PD TV T : Type*} [Fintype PD] [Fintype TV]
       (Γ : 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)
       (hab : plabel a ≠ plabel b) (f : T → T → ℝ)
       (htable : ∀ t u, t ≠ u →
         (Fintype.card {x : TV // t ∈ outgoing x ∧ u ∈ outgoing x} : ℝ) ≤ f t u) :
       ((allowed Γ plabel outgoing pin v).card : ℝ) ≤ f (plabel a) (plabel b) :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.allowed

2. def OAI.TorsionFreeZeroDivisors.ChainRealization.edgePair line 35

   Source documentation

   A choice of orientation for each actual edge; only this choice, not an independent matching event for its reverse, is counted.

   def edgePair (e : Edge len) : Sym2 (Dart len) := s((e,false),(e,true))
   …

3. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.edgePair_injective line 38
4. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.edges_eq line 47
5. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.edges_card line 61
6. def OAI.TorsionFreeZeroDivisors.ChainRealization.label line 64
7. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.label_reverse line 69
8. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.label_back line 75
9. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.label_front line 78
10. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.internal_weight line 84

    Source documentation

    Literal internal turn weight, not an independent-letter approximation.

    theorem internal_weight (w : C → ℤ → WordEstimate.Letter)
        (himm : Function.Injective (fun d => ((graph len first last).origin d,label len w d)))
        (v : Interior len) :
        TypeWeights.jointWeight (label len w (back len v)) (label len w (front len v)) =
          WordEstimate.weight (w v.1 v.2.val) (w v.1 ((v.2.val : ℤ)+1)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.WordEstimate.weight

11. def OAI.TorsionFreeZeroDivisors.ChainRealization.turnProduct line 103
12. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.internal_product line 108

    Source documentation

    Exact product of the type-table factors at all unmarked vertices.

    theorem internal_product (w : C → ℤ → WordEstimate.Letter)
        (himm : Function.Injective (fun d => ((graph len first last).origin d,label len w d))) :
        (∏ v : Interior len,
          TypeWeights.jointWeight (label len w (back len v)) (label len w (front len v))) =
          turnProduct len w := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.ChainRealization.turnProduct

13. def OAI.TorsionFreeZeroDivisors.ChainRealization.pin line 119

    Source documentation

    Marked vertices carry the optional prescribed root. Internal vertices never gain spurious pins.

    def pin {TV : Type*} (p : V → Option TV) : Vertex len (V := V) → Option TV
    …

14. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.pin_internal line 124
15. def OAI.TorsionFreeZeroDivisors.ChainRealization.cost line 128

    Source documentation

    Source vertex-assignment cost, separating the finitely many marked vertices.

    def cost {TV : Type*} (pp : V → Option TV) (n p : ℝ)
        (w : C → ℤ → WordEstimate.Letter) : Vertex len (V := V) → ℝ
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter

16. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.cost_product line 133
17. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.allowed_cost line 145
18. theorem OAI.TorsionFreeZeroDivisors.ChainRealization.fixed_label_bound line 179

    Source documentation

    Exact finite first moment for an actually subdivided chain pattern. The fixed root costs one instead of n; all unmarked vertices use the type table.

    theorem fixed_label_bound {TV : Type*} [Fintype TV]
        (outgoing : TV → Finset Types.Letter) (pp : V → Option TV)
        (n p : ℝ) (w : C → ℤ → WordEstimate.Letter)
        (himm : Function.Injective (fun d => ((graph len first last).origin d,label len w d)))
        (hn : (Fintype.card TV : ℝ) ≤ n)
        (htable : ∀ t u, t ≠ u →
          (Fintype.card {x : TV // t ∈ outgoing x ∧ u ∈ outgoing x} : ℝ) ≤
            n*p*TypeWeights.jointWeight t u)
        (N d R : ℕ) (h2 : 2 ≤ d) (hR : 0 < R)
        (hd : ∀ v, Nat.card {e : PatternEmbeddings.Dart outgoing //
          PatternEmbeddings.origin outgoing e = v} ≤ d)
        (hsize : ∀ x : PatternEmbeddings.Dart outgoing,
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.origin

19. abbrev OAI.TorsionFreeZeroDivisors.ChainWeights.BlockTurn line 220
20. def OAI.TorsionFreeZeroDivisors.ChainWeights.firstCoordinate line 222
21. def OAI.TorsionFreeZeroDivisors.ChainWeights.nextCoordinate line 224
22. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.firstCoordinate_val line 228
23. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.nextCoordinate_val line 235
24. def OAI.TorsionFreeZeroDivisors.ChainWeights.turnPoint line 242
25. def OAI.TorsionFreeZeroDivisors.ChainWeights.turns line 245
26. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.turnPoint_mem line 247
27. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.turnPoint_block line 255
28. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.turnPoint_injective line 261

    Source documentation

    Different block turns are different turns of the actual chain subdivision.

    theorem turnPoint_injective : Function.Injective (turnPoint s hs len) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainWeights.turnPoint

29. def OAI.TorsionFreeZeroDivisors.ChainWeights.atTurn line 278
30. def OAI.TorsionFreeZeroDivisors.ChainWeights.chainProduct line 280
31. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.wordWeight_pred line 283
32. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.turn_product line 289
33. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.chain_le_blocks line 309

    Source documentation

    Discarding only nonnegative factors at most one can increase a chain's turn product. This accounts for cross-block turns and all end fragments.

    theorem chain_le_blocks (w : C → ℤ → Letter) :
        chainProduct len w ≤ ∏ i : Underlying s len, wordWeight (height s len i) (word s len w i) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainWeights.chainProduct

34. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.bin_weight_upper line 325

    Source documentation

    A literal bin contributes its upper endpoint to the fixed-label exponent.

    theorem bin_weight_upper {h : ℕ} {d : ℤ} {W : Fin h → Letter}
        (hW : W ∈ binWords h d) : wordWeight h W ≤ Real.exp (-(d : ℝ)) := by
    …

35. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.chain_bin_bound line 337

    Source documentation

    Fixed-label loss from all active full blocks. The stage instance is obtained by taking C to be the active-chain subtype itself.

    theorem chain_bin_bound (w : C → ℤ → Letter) (d : Underlying s len → ℤ)
        (hbin : ∀ i, word s len w i ∈ binWords (height s len i) (d i)) :
        chainProduct len w ≤ Real.exp (-∑ i, (d i : ℝ)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainWeights.chainProduct

36. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.mem_positions_nat line 347
37. def OAI.TorsionFreeZeroDivisors.ChainWeights.turnEquiv line 358

    Source documentation

    Literal indexing equivalence from internal subdivision vertices to the half-integer-grid turn positions.

    def turnEquiv : ((c : C) × Fin (len c-1)) ≃ (turns len) where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainWeights.turns

38. theorem OAI.TorsionFreeZeroDivisors.ChainWeights.chainProduct_eq line 386

    Source documentation

    The full-chain product is exactly the product over the actual internal vertices used in the matching first moment.

    theorem chainProduct_eq (w : C → ℤ → Letter) :
        chainProduct len w = ∏ v : ((c : C) × Fin (len c-1)),
          weight (w v.1 v.2.val) (w v.1 ((v.2.val : ℤ)+1)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainWeights.chainProduct