Sparse commutation defects

If h commutes with f, changing f to g can break commutation only at changed inputs or their preimages under h. For injective h on a finite type this gives at most twice as many defects as edited inputs. These facts support sparse-counter circuit bounds. For the related block characterization of almost-commuting permutations, see Moreno and Rivera, as credited in the source formalization.

Main definitions

• Cslib.FunctionalGraph.disagreement: the finite set on which two endomaps differ.

Main results

• Cslib.FunctionalGraph.commutation_defect_subset: localization of commutation failures.
• Cslib.FunctionalGraph.commutation_defect_card: the factor-two bound for injective maps.
• Cslib.FunctionalGraph.disagreement_image_eq: edited permutations have the same edited outputs.
• Cslib.FunctionalGraph.disagreement_conjugate_card: relabeling preserves the number of edits.

References

• Adapted from lean/Proofs/CommutationDefect.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

theorem Cslib.FunctionalGraph.commutation_defect_subset {α : Type u} (f g h : α → α) (hc : Function.Commute h f) : {x : α | h (g x) ≠ g (h x)} ⊆ {x : α | f x ≠ g x} ∪ h ⁻¹' {x : α | f x ≠ g x}

Commuting with a sparse modification creates defects only at modified inputs or at their preimages under the commuting map.

noncomputable def Cslib.FunctionalGraph.disagreement {α : Type u} [Fintype α] (f g : α → α) : Finset α

The inputs on which two endomaps disagree.

@[simp]

theorem Cslib.FunctionalGraph.mem_disagreement {α : Type u} [Fintype α] (f g : α → α) (x : α) : x ∈ disagreement f g ↔ f x ≠ g x

A state lies in the disagreement set exactly when f and g differ there.

theorem Cslib.FunctionalGraph.commutation_defect_card {α : Type u} [Fintype α] (f g h : α → α) (hc : Function.Commute h f) (hi : Function.Injective h) : (disagreement (h ∘ g) (g ∘ h)).card ≤ 2 * (disagreement f g).card

Injectivity suffices for the uniform factor-two defect bound.

theorem Cslib.FunctionalGraph.disagreement_image_eq {α : Type u} [Fintype α] [DecidableEq α] (f g : Equiv.Perm α) : Finset.image (⇑f) (disagreement ⇑f ⇑g) = Finset.image (⇑g) (disagreement ⇑f ⇑g)

Permutations agreeing away from the edited inputs use the same remaining outputs.

theorem Cslib.FunctionalGraph.disagreement_conjugate_card {α : Type u} {β : Type u_1} [Fintype α] [Fintype β] (f g : α → α) (e : α ≃ β) : (disagreement (⇑e ∘ f ∘ ⇑e.symm) (⇑e ∘ g ∘ ⇑e.symm)).card = (disagreement f g).card

Relabeling a finite universe preserves the number of edited successors.