AnchorPatternBridge.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Structural bridges for anchor pinning

Group uniqueness and no-shattering give pinning criteria independent of the host construction.

theorem OAI.Problem348.AnchorBridge.row_labels_injective line 18

Source documentation

Distinct pattern rows prevent a copy from repeating any host row class whose members have identical entries.

theorem row_labels_injective {I : Type uI} {J : Type uJ} {R : Type uR} {C : Type uC} {G : Type uG}
    (H : I → J → Bool) (A : R → C → Bool)
    (row : I → R) (col : J → C) (label : R → G)
    (hcopy : ∀ i j, A (row i) (col j) = H i j)
    (hrows : Function.Injective H)
    (hlabel : ∀ r s, label r = label s → A r = A s) :
    Function.Injective (fun i => label (row i)) := by
…

theorem OAI.Problem348.AnchorBridge.col_labels_injective line 32

Source documentation

The column version of row_labels_injective.

theorem col_labels_injective {I : Type uI} {J : Type uJ} {R : Type uR} {C : Type uC} {G : Type uG}
    (H : I → J → Bool) (A : R → C → Bool)
    (row : I → R) (col : J → C) (label : C → G)
    (hcopy : ∀ i j, A (row i) (col j) = H i j)
    (hcols : Function.Injective (fun j => fun i => H i j))
    (hlabel : ∀ c d, label c = label d → ∀ r, A r c = A r d) :
    Function.Injective (fun j => label (col j)) := by
…

def OAI.Problem348.AnchorBridge.wordRow line 47
Source documentation
The 32 rows carrying all binary words in the fixed anchor.
```
def wordRow (a : Fin 32) : Fin 64 := ⟨32 + a.val, by omega⟩
```
def OAI.Problem348.AnchorBridge.wordCol line 50
Source documentation
The five columns carrying the word coordinates in the fixed anchor.
```
def wordCol (b : Fin 5) : Fin 64 := ⟨59 + b.val, by omega⟩
```
theorem OAI.Problem348.AnchorBridge.wordCol_injective line 52

theorem OAI.Problem348.AnchorBridge.anchor_at_32_or_anchor_at_32 line 62

Source documentation

If both axes had at most 32 initial anchor positions, the complete-word submatrix would shatter five non-anchor columns. Thus the position at index 32 is an anchor on at least one axis.

theorem anchor_at_32_or_anchor_at_32 {R : Type uR} {C : Type uC}
    (H : Fin 64 → Fin 64 → Bool) (A : R → C → Bool)
    (row : Fin 64 → R) (col : Fin 64 → C)
    (anchorR : R → Prop) (anchorC : C → Prop)
    (hcopy : ∀ i j, A (row i) (col j) = H i j)
    (hcol : Function.Injective col)
    (hprefixR : ∀ i j, i ≤ j → anchorR (row j) → anchorR (row i))
    (hprefixC : ∀ i j, i ≤ j → anchorC (col j) → anchorC (col i))
    (hwords : ∀ w : Fin 5 → Bool, ∃ a : Fin 32,
      ∀ b : Fin 5, H (wordRow a) (wordCol b) = w b)
    (hnoshatter : ∀ cs : Fin 5 → C, Function.Injective cs →
      (∀ b, ¬ anchorC (cs b)) → ∃ w : Fin 5 → Bool,
…

Mentions: OAI.Problem348.AnchorBridge.wordRow, OAI.Problem348.AnchorBridge.wordCol

theorem OAI.Problem348.AnchorBridge.prefix_card_lower_bound line 95

Source documentation

A downward-closed predicate holding at index m holds at at least m+1 indices.

theorem prefix_card_lower_bound {n : ℕ} (P : Fin n → Prop) [DecidablePred P]
    (m : Fin n) (hprefix : ∀ i j, i ≤ j → P j → P i) (hm : P m) :
    m.val + 1 ≤ (Finset.univ.filter P).card := by
…

theorem OAI.Problem348.AnchorBridge.increasing_labels_eq_id line 109
Source documentation
An increasing self-map of a finite ordered interval uses every label in the prescribed order.
```
theorem increasing_labels_eq_id {n : ℕ} (f : Fin n → Fin n)
    (hf : StrictMono f) : f = id := by
…
```

theorem OAI.Problem348.AnchorBridge.card_selected_row_class_le_one line 117

Source documentation

Any class of host rows with identical entries is used at most once in a copy with distinct pattern rows. In particular this applies to the dummy row class.

theorem card_selected_row_class_le_one {I : Type uI} {J : Type uJ} {R : Type uR} {C : Type uC}
    [Fintype I] (H : I → J → Bool) (A : R → C → Bool)
    (row : I → R) (col : J → C) (P : R → Prop) [DecidablePred P]
    (hcopy : ∀ i j, A (row i) (col j) = H i j)
    (hrows : Function.Injective H)
    (hclass : ∀ r s, P r → P s → A r = A s) :
    (Finset.univ.filter (fun i => P (row i))).card ≤ 1 := by
…

theorem OAI.Problem348.AnchorBridge.card_selected_col_class_le_one line 134

Source documentation

Column version of the single-use class bound.

theorem card_selected_col_class_le_one {I : Type uI} {J : Type uJ} {R : Type uR} {C : Type uC}
    [Fintype J] (H : I → J → Bool) (A : R → C → Bool)
    (row : I → R) (col : J → C) (P : C → Prop) [DecidablePred P]
    (hcopy : ∀ i j, A (row i) (col j) = H i j)
    (hcols : Function.Injective (fun j => fun i => H i j))
    (hclass : ∀ c d, P c → P d → ∀ r, A r c = A r d) :
    (Finset.univ.filter (fun j => P (col j))).card ≤ 1 := by
…