Retained.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.exists_hub_families line 10

Source documentation

Select the two 64-point families and a distinct hub.

theorem exists_hub_families {H : Type*} [Finite H] (hh : 129 ≤ Nat.card H) :
    ∃ u v : Fin 64 ↪ H, ∃ z : H,
      (∀ i j, u i ≠ v j) ∧ (∀ i, u i ≠ z) ∧ (∀ j, v j ≠ z) := by
…

theorem OAI.TwoWayComplementation.retained_pair_set line 40

Source documentation

Retaining a new pair and all external points removes exactly 127 points.

theorem retained_pair_set {H : Type*} [Finite H] (U V : Set H)
    (hU : U.ncard = 64) (hV : V.ncard = 64) (hUV : Disjoint U V)
    (z x y : H) (hzU : z ∉ U) (hzV : z ∉ V) (hx : x ∈ U) (hy : y ∈ V) :
    ∃ F : Set H, Nat.card F = Nat.card H - 127 ∧ x ∈ F ∧ y ∈ F ∧ z ∉ F ∧
      (∀ a ∈ U, a ∈ F → a = x) ∧ (∀ b ∈ V, b ∈ F → b = y) := by
…

theorem OAI.TwoWayComplementation.mem_restricted_sandwich line 79

Source documentation

Identity sandwiches restrict exactly the two endpoints.

theorem mem_restricted_sandwich {H : Type*} (F : Set H) (R : SetRel H H) (a b : H) :
    (a, b) ∈ restrictedIdentity F ○ R ○ restrictedIdentity F ↔
      a ∈ F ∧ b ∈ F ∧ (a, b) ∈ R := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.retained_relation_identity line 86

Source documentation

Before its turn, the selected pair is absent from the retained restriction.

theorem retained_relation_identity {H : Type*} (U V F : Set H) (z x y : H)
    (hz : z ∉ F) (hx : ∀ a ∈ U, a ∈ F → a = x) (hy : ∀ b ∈ V, b ∈ F → b = y)
    (E : SetRel H H) (hE : E ⊆ U ×ˢ V) (hnew : (x, y) ∉ E) :
    restrictedIdentity F ○ (restrictedIdentity {a | a ≠ z} ∪ E) ○ restrictedIdentity F =
      restrictedIdentity F := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.retained_relation_pair line 101

Source documentation

At its turn, restriction adds precisely the selected pair to the retained identity.

theorem retained_relation_pair {H : Type*} (P : SetRel H H) (F : Set H)
    (hP : restrictedIdentity F ○ P ○ restrictedIdentity F = restrictedIdentity F)
    (x y : H) (hx : x ∈ F) (hy : y ∈ F) :
    restrictedIdentity F ○ (P ∪ {(x, y)}) ○ restrictedIdentity F =
      restrictedIdentity F ∪ {(x, y)} := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.lossBound_step line 114
Source documentation
The target doubles whenever the induction removes 127 points.
```
theorem lossBound_step {h : ℕ} (hh : 129 ≤ h) : lossBound h = 2 * lossBound (h - 127) := by
…
```
Mentions: OAI.TwoWayComplementation.lossBound

theorem OAI.TwoWayComplementation.amplification_arithmetic line 119

Source documentation

The numerical conclusion of summing the 4096 inductive lower bounds.

theorem amplification_arithmetic {h c : ℕ} (hh : 129 ≤ h) (δ : Fin 4096 → ℕ)
    (htotal : ∑ j, δ j ≤ 1024 * c)
    (hstep : ∀ j, lossBound (h - 127) ≤ 2 * δ j) : lossBound h ≤ c := by
…

Mentions: OAI.TwoWayComplementation.lossBound

theorem OAI.TwoWayComplementation.single_edge_base line 130

Source documentation

The base case detects the off-diagonal pair using rectangle coverage and order reversal.

theorem single_edge_base {A H : Type*} [Monoid A] {m : ℕ}
    (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H)
    (hreverse : ∀ a b, (ι a, ι b) ∈ Diagram.inclusion m → (φ b).toRel ⊆ (φ a).toRel)
    (a : A) (x y : H) (hxy : x ≠ y)
    (himage : (φ a).toRel = SetRel.id ∪ {(x, y)}) (hh : Nat.card H ≤ 128) :
    lossBound (Nat.card H) ≤ ((ι 1).missing (ι a)).ncard := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.RelationMonoid, OAI.TwoWayComplementation.Diagram.inclusion, OAI.TwoWayComplementation.lossBound

theorem OAI.TwoWayComplementation.sandwich_power_absorption line 150

Source documentation

Every positive power of a sandwich is absorbed by its idempotent outer factor.

theorem sandwich_power_absorption {A : Type*} [Monoid A] (b a : A)
    (hb : IsIdempotentElem b) (k : ℕ) :
    b * (b * a * b) ^ (k + 1) = (b * a * b) ^ (k + 1) ∧
      (b * a * b) ^ (k + 1) * b = (b * a * b) ^ (k + 1) := by
…