RejectingMates.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.WLIdentification.ComparisonSchemas.SpecialImages line 12
Source documentation
Exactly the individual scalar-image hypotheses of special-twist sufficiency. No simultaneous choice satisfying the wires is required.
```
structure SpecialImages (b : E → Bit) where
…
```
Mentions: OAI.WLIdentification.Bit
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.chooseAt line 22
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.scalar_mem line 33
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.scalar_preimage line 43

theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.wrapping_shift_extension line 66

Source documentation

The one constrained old wrapping component lifts even if it lies entirely inside a wire and the new cut re-expresses it at the opposite real endpoint.

theorem wrapping_shift_extension {n : ℕ} (hr : 3 ≤ r) {U : Finset (S.layout n).Block}
    (hu : U.card ≤ r) (hw : (S.layout n).Wrapping (by omega) U)
    {cut cut' : E → Fin n} (hc : S.Avoids n U cut) (hc' : S.Avoids n U cut')
    {A A' : Fin r → Bool}
    (hA : (S.layout n).IsWrappingAddress U (S.align n cut) A)
    (hA' : (S.layout n).IsWrappingAddress U (S.align n cut') A')
    (q : S.RealShift) (hq : ∀ p, q p ∈ I.values p A) :
    ∃ q' : S.RealShift, (∀ p, q' p ∈ I.values p A') ∧
      ∀ h : (S.layout n).HName, Sum.inl h ∈ (S.layout n).names U →
        S.starShift n cut' b q' h.1 = S.starShift n cut b q h.1 := by
…

theorem OAI.WLIdentification.RingLayout.translation_eq_of_shifts line 130
def OAI.WLIdentification.ComparisonSchemas.SpecialImages.Admissible line 150
Source documentation
A stronger sufficient family using globally completed cut stars. Its address restriction is imposed only by wrapping subcollections of size r.
```
def Admissible (n : ℕ) (hr : 2 ≤ r) (U : Finset (S.layout n).Block)
    (x : (S.layout n).Coordinate → Bit) : Prop :=
…
```
Mentions: OAI.WLIdentification.Bit
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.admissible_nonempty line 158
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.admissible_restrict line 169
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.admissible_legal line 178
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.admissible_extend line 191
def OAI.WLIdentification.ComparisonSchemas.SpecialImages.offsetFamily line 231
Source documentation
A proved producer of the exact-projection interface, not a hypothesis asserting that local translations happen to extend.
```
noncomputable def offsetFamily {n : ℕ} (hr : 3 ≤ r) (hn : r + 1 < n) :
    ((S.layout n).affine (by omega)).OffsetFamily (S.specialTwist n b) (r + 1) where
…
```
theorem OAI.WLIdentification.ComparisonSchemas.SpecialImages.equivalent_special line 242
Source documentation
Equivalence of the special twist on the uncolored leaf-coded graph; the private interior may be arbitrarily longer than K.
```
theorem equivalent_special {n : ℕ} (hr : 32 ≤ r) (hn : r + 1 < n) :
    Equivalent r (((S.layout n).affine (by omega)).graph 0)
      (((S.layout n).affine (by omega)).graph (S.specialTwist n b)) := by
…
```
Mentions: OAI.WLIdentification.Equivalent