Amplification.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.lossBound line 10
Source documentation
The exponential lower bound for 2 ≤ h.
```
def lossBound (h : ℕ) : ℕ := 2 ^ ((h - 2) / 127)
```
theorem OAI.TwoWayComplementation.map_identity_corner line 13
Source documentation
The image of a monoid lies in the diagram corner of its image identity.
```
theorem map_identity_corner {A : Type*} [Monoid A] {m : ℕ}
    (ι : A →ₙ* Diagram m) (a : A) : ι a ∈ (ι 1).corner := by
…
```
Mentions: OAI.TwoWayComplementation.Diagram

theorem OAI.TwoWayComplementation.missing_context_card line 22

Source documentation

The cardinality consequence of the uniform transport theorem.

theorem missing_context_card {m : ℕ} (e d u v z : Diagram m)
    (he : Diagram.comp e e = e) (hd : Diagram.comp d d = d)
    (hcontext : Diagram.comp (Diagram.comp u e) v = d) (hz : z ∈ e.corner)
    (hnew : Diagram.comp (Diagram.comp u z) v ∈ d.corner) :
    (d.missing (Diagram.comp (Diagram.comp u z) v)).ncard ≤ 2 * (e.missing z).ncard := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

theorem OAI.TwoWayComplementation.conjugate_missing_bound line 32

Source documentation

Conjugating by a unit costs at most twice as many missing classes.

theorem conjugate_missing_bound {A : Type*} [Monoid A] {m : ℕ}
    (ι : A →ₙ* Diagram m) (p : Aˣ) (a : A) :
    ((ι 1).missing (ι (p * a * (↑p⁻¹ : A)))).ncard ≤
      2 * ((ι 1).missing (ι a)).ncard := by
…

Mentions: OAI.TwoWayComplementation.Diagram

theorem OAI.TwoWayComplementation.common_pair_budget line 51

Source documentation

All pair products share one missing-set bound after sandwiching by an idempotent.

theorem common_pair_budget {A : Type*} [Monoid A] {m t c : ℕ}
    (ι : A →ₙ* Diagram m) (f : Bool × Fin t → A) (b0 : A) (hb0 : IsIdempotentElem b0)
    (hcost : ∀ p, ((ι 1).missing (ι (f p))).ncard ≤ 2 * c) :
    ∃ J0 ⊆ (ι b0).classes, J0.ncard ≤ 8 * t * c ∧
      ∀ i j, (ι b0).missing (ι (b0 * f (false, i) * f (true, j) * b0)) ⊆ J0 := by
…

Mentions: OAI.TwoWayComplementation.Diagram

theorem OAI.TwoWayComplementation.bipartite_relation_comp line 94

Source documentation

Disjoint source and target sets prevent two added edges from being concatenated.

theorem bipartite_relation_comp {H : Type*} (F U V : Set H)
    (hU : U ⊆ F) (hV : V ⊆ F) (hUV : Disjoint U V)
    (E E' : SetRel H H) (hE : E ⊆ U ×ˢ V) (hE' : E' ⊆ U ×ˢ V) :
    (restrictedIdentity F ∪ E) ○ (restrictedIdentity F ∪ E') =
      restrictedIdentity F ∪ (E ∪ E') := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.hub_pair_relation line 112

Source documentation

Removing the hub leaves exactly the desired pair between its two neighbours.

theorem hub_pair_relation {H : Type*} (u v z : H) (huz : u ≠ z) (hvz : v ≠ z) :
    restrictedIdentity {x | x ≠ z} ○ (SetRel.id ∪ {(u, z)}) ○
      (SetRel.id ∪ {(z, v)}) ○ restrictedIdentity {x | x ≠ z} =
        restrictedIdentity {x | x ≠ z} ∪ {(u, v)} := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

def OAI.TwoWayComplementation.permutationUnit line 122
Source documentation
A permutation and its inverse form a unit in the full relation monoid.
```
def permutationUnit {H : Type*} (σ : Equiv.Perm H) : (RelationMonoid H)ˣ where
…
```
Mentions: OAI.TwoWayComplementation.RelationMonoid

theorem OAI.TwoWayComplementation.permutation_conjugate_relation line 137

Source documentation

Permutation conjugation relabels both endpoints of every relation edge.

theorem permutation_conjugate_relation {H : Type*} (σ : Equiv.Perm H) (R : SetRel H H) :
    Function.graph σ ○ R ○ Function.graph σ.symm = {xy | (σ xy.1, σ xy.2) ∈ R} := by
…

theorem OAI.TwoWayComplementation.pair_conjugate line 150

Source documentation

Unit lifts move the initial added pair to any other ordered pair of distinct points.

theorem pair_conjugate {A H : Type*} [Monoid A] {m : ℕ}
    (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H)
    (hlift : ∀ σ : Equiv.Perm H, ∃ p : Aˣ, φ p = (permutationUnit σ).val)
    (a : A) (ha : IsIdempotentElem a) (x y : H) (hxy : x ≠ y)
    (himage : (φ a).toRel = SetRel.id ∪ {(x, y)}) (u v : H) (huv : u ≠ v) :
    ∃ s : A, IsIdempotentElem s ∧ (φ s).toRel = SetRel.id ∪ {(u, v)} ∧
      ((ι 1).missing (ι s)).ncard ≤ 2 * ((ι 1).missing (ι a)).ncard := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.RelationMonoid, OAI.TwoWayComplementation.permutationUnit

theorem OAI.TwoWayComplementation.smaller_relation_instance line 179

Source documentation

Restricting an idempotent sandwich preserves the new pair and supplies all unit lifts.

theorem smaller_relation_instance {A H : Type*} [Monoid A] [Finite A] {m : ℕ}
    (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H) (hφ : Function.Surjective φ)
    (b b' : A) (hb : IsIdempotentElem b) (hbb' : b * b' = b') (hb'b : b' * b = b')
    (F : Set H)
    (hiPi : restrictedIdentity F ○ (φ b).toRel ○ restrictedIdentity F = restrictedIdentity F)
    (x y : F)
    (hpair : restrictedIdentity F ○ (φ b').toRel ○ restrictedIdentity F =
      restrictedIdentity F ∪ {(x.val, y.val)}) :
    ∃ d : hb.Corner, ∃ hd : IsIdempotentElem d, ∃ ψ : hd.Corner →* RelationMonoid F,
      Function.Surjective ψ ∧
      (∀ σ : Equiv.Perm F, ∃ p : hd.Cornerˣ, ψ p = (permutationUnit σ).val) ∧
      (∀ w, (ψ w).toRel = {xy : F × F | (xy.1.val, xy.2.val) ∈ (φ w.val.val).toRel}) ∧
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.RelationMonoid, OAI.TwoWayComplementation.restrictedIdentity, OAI.TwoWayComplementation.permutationUnit