AnchorPatternFixed.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Structural anchor bridges for the fixed pattern

The generic bridges are specialized to the explicit anchor64 definition.

theorem OAI.Problem348.AnchorBridge.anchor64_word_block_complete line 17
Source documentation
The exact anchor realizes every five-bit word on the specified suffix.
```
theorem anchor64_word_block_complete (w : Fin 5 → Bool) :
    ∃ a : Fin 32, ∀ b : Fin 5,
      anchor64 (wordRow a) (wordCol b) = w b := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.AnchorBridge.wordRow, OAI.Problem348.AnchorBridge.wordCol

theorem OAI.Problem348.AnchorBridge.anchor64_anchor_majority line 28

Source documentation

An exact anchor copy has at least 33 anchors on one of its two axes, provided anchors form prefixes and non-anchor rows do not shatter five non-anchor columns.

theorem anchor64_anchor_majority {R : Type uR} {C : Type uC}
    (A : R → C → Bool) (row : Fin 64 → R) (col : Fin 64 → C)
    (anchorR : R → Prop) (anchorC : C → Prop)
    [DecidablePred anchorR] [DecidablePred anchorC]
    (hcopy : ∀ i j, A (row i) (col j) = anchor64 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))
    (hnoshatter : ∀ cs : Fin 5 → C, Function.Injective cs →
      (∀ b, ¬ anchorC (cs b)) → ∃ w : Fin 5 → Bool,
        ∀ r, ¬ anchorR r → ∃ b, A r (cs b) ≠ w b) :
    33 ≤ (Finset.univ.filter (fun i => anchorR (row i))).card ∨
…

Mentions: OAI.Problem348.anchor64

theorem OAI.Problem348.AnchorBridge.anchor64_row_class_single_use line 47

Source documentation

A row class of equal host rows occurs at most once in an anchor copy.

theorem anchor64_row_class_single_use {R : Type uR} {C : Type uC}
    (A : R → C → Bool) (row : Fin 64 → R) (col : Fin 64 → C)
    (P : R → Prop) [DecidablePred P]
    (hcopy : ∀ i j, A (row i) (col j) = anchor64 i j)
    (hclass : ∀ r s, P r → P s → A r = A s) :
    (Finset.univ.filter (fun i => P (row i))).card ≤ 1 :=
…

Mentions: OAI.Problem348.anchor64

theorem OAI.Problem348.AnchorBridge.anchor64_col_class_single_use line 57

Source documentation

A column class of equal host columns occurs at most once in an anchor copy.

theorem anchor64_col_class_single_use {R : Type uR} {C : Type uC}
    (A : R → C → Bool) (row : Fin 64 → R) (col : Fin 64 → C)
    (P : C → Prop) [DecidablePred P]
    (hcopy : ∀ i j, A (row i) (col j) = anchor64 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 :=
…

Mentions: OAI.Problem348.anchor64