OAI/Algebra/GroupRing/StageBlocks.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.StageBlocks.Component line 15
2. def OAI.TorsionFreeZeroDivisors.StageBlocks.translationWords line 17
3. theorem OAI.TorsionFreeZeroDivisors.StageBlocks.translation_card line 20
4. def OAI.TorsionFreeZeroDivisors.StageBlocks.rootWords line 33
5. def OAI.TorsionFreeZeroDivisors.StageBlocks.basicCost line 38
6. def OAI.TorsionFreeZeroDivisors.StageBlocks.Feasible line 43
7. theorem OAI.TorsionFreeZeroDivisors.StageBlocks.feasible_root line 48
8. theorem OAI.TorsionFreeZeroDivisors.StageBlocks.root_bound line 56
9. theorem OAI.TorsionFreeZeroDivisors.StageBlocks.stage_count line 87

   Source documentation

   Count the actual active projections with bin or self-translation roots. The error exponent is explicit: twice the missing substring size per block.

   theorem stage_count (A : Finset I) (s : ℝ) (e : ℕ)
       (hlarge : ∀ i, 3002 ≤ h i) (hscale : ∀ i, s+1200 ≤ 2*(h i : ℝ))
       (hlinks : ∀ i j, L.graph.Adj i j → h i - (L.known i j).card ≤ e)
       (hself : ∀ c tr, D c = some tr → h (r c).val-tr.domain.card ≤ e) :
       ((StageLabels.stageWords h A (Feasible L r D d)).card : ℝ) ≤
         Real.exp ((∑ c : StageLabels.activeComponents L.graph.connectedComponentMk A,
           basicCost L r D d s c.val) + 2*(e : ℝ)*Fintype.card I*Real.log (Fintype.card Letter)) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.stageWords, OAI.TorsionFreeZeroDivisors.StageBlocks.Feasible, OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents, OAI.TorsionFreeZeroDivisors.StageBlocks.basicCost

10. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.projection_empty line 118

    Source documentation

    An infeasible complete word has no active projection.

    theorem projection_empty {I T : Type*} [Fintype I] [Fintype T]
        (h : I → ℕ) (A : Finset I) (P : ((i : I) → Fin (h i) → T) → Prop)
        (hn : ¬∃ W, P W) : StageLabels.stageWords h A P = ∅ := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualStageLabels.P, OAI.TorsionFreeZeroDivisors.StageLabels.stageWords

11. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.projection_bound line 128

    Source documentation

    Uniform root errors and propagation errors together cost at most twice one missing substring per underlying block.

    theorem projection_bound {I T : Type*} [Fintype I] [Fintype T] [Nonempty T]
        {h : I → ℕ} (L : StageLabels.Links (T := T) h) (A : Finset I)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualStageLabels.L, OAI.TorsionFreeZeroDivisors.StageLabels.Links

12. def OAI.TorsionFreeZeroDivisors.ActualStageLabels.symbol line 161
13. abbrev OAI.TorsionFreeZeroDivisors.ActualStageLabels.L line 164
14. abbrev OAI.TorsionFreeZeroDivisors.ActualStageLabels.P line 165
15. abbrev OAI.TorsionFreeZeroDivisors.ActualStageLabels.Component line 166
16. def OAI.TorsionFreeZeroDivisors.ActualStageLabels.Comparing line 168
17. def OAI.TorsionFreeZeroDivisors.ActualStageLabels.Immersed line 174
18. def OAI.TorsionFreeZeroDivisors.ActualStageLabels.Feasible line 180
19. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.feasible_consistent line 185
20. def OAI.TorsionFreeZeroDivisors.ActualStageLabels.cost line 203

    Source documentation

    The source component cost with the actual occurrence matching and its actual self-links, not a supplied abstract component partition.

    def cost (c : Component s hs len m cmp err) : ℝ :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualStageLabels.Component

21. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.root_count line 207
22. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.stage_count line 253

    Source documentation

    Counting the actual stage projection. Self-link roots are selected from one feasible realization; if none exists, the projection is empty.

    theorem stage_count (A : Finset (Underlying s len))
        (hlarge : ∀ i, 3002 ≤ height s len i)
        (hscale : ∀ i, s+1200 ≤ 2*(height s len i : ℝ))
        (hreduced : ∀ x e, cmp.side x = some e →
          (x.1.1,x.2.val) ≠ ((cmp.pairing.partner x).1.1,(cmp.pairing.partner x).2.val)) :
        ((StageLabels.stageWords (height s len) A (Feasible s len m cmp d)).card : ℝ) ≤
          Real.exp ((∑ c : StageLabels.activeComponents (L s hs len m cmp err).graph.connectedComponentMk A,
            cost s hs len m cmp err d c.val) +
            2*(err : ℝ)*Fintype.card (Underlying s len)*Real.log (Fintype.card Letter)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.stageWords, OAI.TorsionFreeZeroDivisors.ActualStageLabels.Feasible, OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents, OAI.TorsionFreeZeroDivisors.ActualStageLabels.L, OAI.TorsionFreeZeroDivisors.ActualStageLabels.cost

23. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.active_iff line 276

    Source documentation

    Stage components are precisely those whose maximum multiplicity exceeds the zero-based stage number.

    theorem active_iff (j : ℕ) (c : Component s hs len m cmp err) :
        c ∈ StageLabels.activeComponents (L s hs len m cmp err).graph.connectedComponentMk
          (Finset.univ.filter (fun i => j < multiplicity s len m i)) ↔
          j < LinkComponents.maximum (multiplicity s len m) (P s hs len m cmp err) c := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualStageLabels.Component, OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents, OAI.TorsionFreeZeroDivisors.ActualStageLabels.L, OAI.TorsionFreeZeroDivisors.LinkComponents.maximum, OAI.TorsionFreeZeroDivisors.ActualStageLabels.P

24. theorem OAI.TorsionFreeZeroDivisors.ActualStageLabels.cost_sum line 289

    Source documentation

    Literal source component sum, now in the form used by stage-cost summation.

    theorem cost_sum (j : ℕ) :
        (∑ c : StageLabels.activeComponents (L s hs len m cmp err).graph.connectedComponentMk
          (Finset.univ.filter (fun i => j < multiplicity s len m i)), cost s hs len m cmp err d c.val) =
        ∑ c : Component s hs len m cmp err,
          if j < LinkComponents.maximum (multiplicity s len m) (P s hs len m cmp err) c then
            cost s hs len m cmp err d c else 0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents, OAI.TorsionFreeZeroDivisors.ActualStageLabels.L, OAI.TorsionFreeZeroDivisors.ActualStageLabels.cost, OAI.TorsionFreeZeroDivisors.ActualStageLabels.Component, OAI.TorsionFreeZeroDivisors.LinkComponents.maximum, OAI.TorsionFreeZeroDivisors.ActualStageLabels.P

25. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.stageWords_mem line 315

    Source documentation

    Direct membership in a finite active projection, with the generic index instances retained rather than recomputed after specializing the sigma type.

    theorem stageWords_mem {I T : Type*} [Fintype I] [Fintype T] (h : I → ℕ)
        (A : Finset I) (P : ((i : I) → Fin (h i) → T) → Prop)
        (W : (i : I) → Fin (h i) → T) (hW : P W) :
        (fun i : A => W i.val) ∈ StageLabels.stageWords h A P := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.stageWords

26. abbrev OAI.TorsionFreeZeroDivisors.ChainStageLabels.ActiveChain line 328
27. abbrev OAI.TorsionFreeZeroDivisors.ChainStageLabels.StagePosition line 329
28. abbrev OAI.TorsionFreeZeroDivisors.ChainStageLabels.StageTail line 330
29. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.activeBlocks line 331
30. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.tail_subset line 335
31. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.blockPoint line 341
32. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.tailPoint line 347
33. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.blockRestrict line 350
34. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.tailRestrict line 353
35. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.encode line 356
36. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.encode_injective line 361

    Source documentation

    Full blocks and the literal end fragments determine every active chain letter, without choosing values on inactive chains.

    theorem encode_injective : Function.Injective (encode s hs len m j) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageLabels.encode

37. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.extension_count line 376

    Source documentation

    The exact finite extension factor contributed by arbitrary tail letters.

    theorem extension_count (X : Finset (StagePosition len m j → Letter))
        (Y : Finset ((i : activeBlocks s len m j) → Fin (height s len i.val) → Letter))
        (hX : ∀ F ∈ X, blockRestrict s hs len m j F ∈ Y) :
        X.card ≤ Y.card * (Fintype.card Letter)^Fintype.card (StageTail s len m j) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageLabels.StagePosition, OAI.TorsionFreeZeroDivisors.ChainStageLabels.activeBlocks, OAI.TorsionFreeZeroDivisors.ChainStageLabels.blockRestrict, OAI.TorsionFreeZeroDivisors.ChainStageLabels.StageTail

38. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.tail_count line 392

    Source documentation

    The fragment loss is O(s) per marked chain, with a literal uniform bound.

    theorem tail_count : (Fintype.card (StageTail s len m j) : ℝ) ≤
        (s+1)*Fintype.card C := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageLabels.StageTail

39. def OAI.TorsionFreeZeroDivisors.ChainStageLabels.fullWords line 405
40. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.blockRestrict_word line 411
41. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.restrict_mem line 423

    Source documentation

    Every literal feasible full-chain assignment projects to feasible blocks.

    theorem restrict_mem (F : StagePosition len m j → Letter)
        (hF : F ∈ fullWords s len m j cmp d) :
        blockRestrict s hs len m j F ∈ StageLabels.stageWords (height s len)
          (activeBlocks s len m j) (ActualStageLabels.Feasible s len m cmp d) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageLabels.StagePosition, OAI.TorsionFreeZeroDivisors.ChainStageLabels.fullWords, OAI.TorsionFreeZeroDivisors.ChainStageLabels.blockRestrict, OAI.TorsionFreeZeroDivisors.StageLabels.stageWords, OAI.TorsionFreeZeroDivisors.ChainStageLabels.activeBlocks, OAI.TorsionFreeZeroDivisors.ActualStageLabels.Feasible

42. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.count_extension_exp line 438

    Source documentation

    Numerical extension bound factored independently of the graph types.

    theorem count_extension_exp (x y k z : ℕ) (cost error bound : ℝ)
        (hxy : x ≤ y*k^z) (hy : (y : ℝ) ≤ Real.exp (cost+error*Real.log k))
        (hz : (z : ℝ) ≤ bound) (hk : 0 < k) :
        (x : ℝ) ≤ Real.exp (cost+(error+bound)*Real.log k) := by
    …

43. theorem OAI.TorsionFreeZeroDivisors.ChainStageLabels.full_stage_count line 454

    Source documentation

    Source stage-label estimate including every tail, not just full blocks.

    theorem full_stage_count (err : ℕ)
        (hlarge : ∀ i, 3002 ≤ height s len i)
        (hscale : ∀ i, s+1200 ≤ 2*(height s len i : ℝ))
        (hreduced : ∀ x e, cmp.side x = some e →
          (x.1.1,x.2.val) ≠ ((cmp.pairing.partner x).1.1,(cmp.pairing.partner x).2.val)) :
        ((fullWords s len m j cmp d).card : ℝ) ≤
          Real.exp ((∑ c : StageLabels.activeComponents
            (ActualStageLabels.L s hs len m cmp err).graph.connectedComponentMk (activeBlocks s len m j),
            ActualStageLabels.cost s hs len m cmp err d c.val) +
            (2*(err : ℝ)*Fintype.card (Underlying s len)+(s+1)*Fintype.card C)*
              Real.log (Fintype.card Letter)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageLabels.fullWords, OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents, OAI.TorsionFreeZeroDivisors.ActualStageLabels.L, OAI.TorsionFreeZeroDivisors.ChainStageLabels.activeBlocks, OAI.TorsionFreeZeroDivisors.ActualStageLabels.cost