OAI/Combinatorics/Automata/RankLoss.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OneWayLiveness.rankLoss line 7
2. def OAI.OneWayLiveness.RankLossAt line 10

   Source documentation

   A simultaneous rank-loss bound for relation quotients with unit lifts.

   def RankLossAt (h : ℕ) : Prop :=
   …

3. lemma OAI.OneWayLiveness.rank_drop_step line 20

   Source documentation

   One new relation pair forces the inductive rank loss, after two genuine corner reductions. The support budget loses only the factor two.

   lemma rank_drop_step {H A M : Type} [Fintype H] [Fintype A] [Monoid M] [Finite M]
       (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ρ)
       (φ : M →* BRel H) (hφ : Function.Surjective φ)
       (e : M) (he : e * e = e) (b : Corner e he) (hb : b * b = b)
       (P N : BRel H) (heP : φ e = P) (hbN : φ b.val = N)
       (F : Set H) [Fintype F]
       (hF : BRel.restrictedId F * P * BRel.restrictedId F = BRel.restrictedId F)
       (hPN : P * N = N) (hNP : N * P = N)
       (x y : F) (hxy : x ≠ y)
       (hN : ∀ i j : F, N.holds i.val j.val ↔ (BRel.addEdge x y).holds i j)
       (hIH : RankLossAt (Fintype.card F)) :
       rankLoss (Fintype.card F) ≤ 2 * (Pairing.rank (ρ e) - Pairing.rank (ρ b.val)) := by
   …

   Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.BRel, OAI.OneWayLiveness.Corner, OAI.OneWayLiveness.BRel.restrictedId, OAI.OneWayLiveness.BRel.addEdge, OAI.OneWayLiveness.RankLossAt, OAI.OneWayLiveness.rankLoss, OAI.OneWayLiveness.Pairing.rank

4. def OAI.OneWayLiveness.RectangleFrame.deleted line 91
5. def OAI.OneWayLiveness.RectangleFrame.retained line 94
6. lemma OAI.OneWayLiveness.RectangleFrame.deleted_card line 96
7. lemma OAI.OneWayLiveness.RectangleFrame.retained_card line 114
8. lemma OAI.OneWayLiveness.RectangleFrame.retained_ne_hub line 120
9. lemma OAI.OneWayLiveness.RectangleFrame.left_mem_retained line 125
10. lemma OAI.OneWayLiveness.RectangleFrame.right_mem_retained line 138
11. lemma OAI.OneWayLiveness.RectangleFrame.old_avoids_retained line 151
12. lemma OAI.OneWayLiveness.RectangleFrame.exists_frame line 159
13. lemma OAI.OneWayLiveness.rectangle_chain line 180
14. lemma OAI.OneWayLiveness.rankLoss_recurrence line 269
15. theorem OAI.OneWayLiveness.rankLoss_all line 276

    Source documentation

    Exponential rank loss by 256-addition amplification, simultaneously in the relation alphabet and the ambient diagram degree.

    theorem rankLoss_all (h : ℕ) : RankLossAt h := by
    …

    Mentions: OAI.OneWayLiveness.RankLossAt

16. def OAI.OneWayLiveness.Corner.oneEquiv line 356
17. theorem OAI.OneWayLiveness.relation_divisor_degree line 365

    Source documentation

    No permutation-lift hypothesis remains in the divisor degree bound.

    theorem relation_divisor_degree {H A M : Type} [Fintype H] [Fintype A]
        [Monoid M] [Finite M] (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ρ)
        (φ : M →* BRel H) (hφ : Function.Surjective φ) (x y : H) (hxy : x ≠ y) :
        rankLoss (Fintype.card H) ≤ Fintype.card A := by
    …

    Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.BRel, OAI.OneWayLiveness.rankLoss