AnchorProperties.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem348.anchor64_eq_decide_ne line 8
Source documentation
The anchor is off-diagonal one outside its modified bit rectangle.
```
theorem anchor64_eq_decide_ne (u v : Fin 64)
    (h : u.val < 32 ∨ v.val < 59) :
    anchor64 u v = decide (u.val ≠ v.val) := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.anchor64_first32_zero_iff line 17
Source documentation
In the dense prefix, every column has at most one zero.
```
theorem anchor64_first32_zero_iff (u v : Fin 64) (hu : u.val < 32) :
    anchor64 u v = false ↔ u = v := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.anchor64_first32_column_zero_iff line 23
Source documentation
In the dense prefix, every row has at most one zero.
```
theorem anchor64_first32_column_zero_iff (u v : Fin 64) (hv : v.val < 32) :
    anchor64 u v = false ↔ u = v := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.anchor64_row_ones line 29
Source documentation
Every anchor row contains at least 58 ones.
```
theorem anchor64_row_ones : ∀ u : Fin 64,
    58 ≤ (Finset.univ.filter (fun v => anchor64 u v = true)).card := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.anchor64_column_ones line 34
Source documentation
Every anchor column contains at least 48 ones.
```
theorem anchor64_column_ones : ∀ v : Fin 64,
    48 ≤ (Finset.univ.filter (fun u => anchor64 u v = true)).card := by
…
```
Mentions: OAI.Problem348.anchor64
def OAI.Problem348.anchorLastCol line 39
Source documentation
The five bit-coordinate columns of the anchor.
```
def anchorLastCol (b : Fin 5) : Fin 64 := ⟨b.val + 59, by omega⟩
```
theorem OAI.Problem348.anchor64_rows_injective line 42
Source documentation
Distinct rows have distinct complete anchor words.
```
theorem anchor64_rows_injective : Function.Injective anchor64 := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.anchor64_columns_injective line 63
Source documentation
Distinct columns have distinct complete anchor words.
```
theorem anchor64_columns_injective :
    Function.Injective (fun v : Fin 64 => fun u : Fin 64 => anchor64 u v) := by
…
```
Mentions: OAI.Problem348.anchor64
def OAI.Problem348.anchorWord line 68
Source documentation
All five-bit words, in the order used by the replacement rectangle.
```
def anchorWord (a : Fin 32) (b : Fin 5) : Bool :=
…
```
theorem OAI.Problem348.anchorWord_bijective line 72
Source documentation
The 32 lower anchor rows realize all binary words on the last five columns.
```
theorem anchorWord_bijective : Function.Bijective anchorWord := by
…
```
Mentions: OAI.Problem348.anchorWord
def OAI.Problem348.anchorFirst32 line 76
Source documentation
Inclusion of the dense 32-position prefix.
```
def anchorFirst32 (i : Fin 32) : Fin 64 := ⟨i.val, by omega⟩
```
theorem OAI.Problem348.anchor64_first32_column_ones line 79
Source documentation
First-prefix column density, used to exclude variable columns.
```
theorem anchor64_first32_column_ones : ∀ v : Fin 64,
    31 ≤ (Finset.univ.filter (fun u : Fin 32 =>
      anchor64 (anchorFirst32 u) v = true)).card := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.anchorFirst32
theorem OAI.Problem348.anchor64_first32_row_ones line 85
Source documentation
First-prefix row density, used to exclude variable rows.
```
theorem anchor64_first32_row_ones : ∀ u : Fin 64,
    31 ≤ (Finset.univ.filter (fun v : Fin 32 =>
      anchor64 u (anchorFirst32 v) = true)).card := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.anchorFirst32
theorem OAI.Problem348.anchor64_columns_common_one line 91
Source documentation
Any two columns share a one in the first 32 rows.
```
theorem anchor64_columns_common_one : ∀ v w : Fin 64,
    ∃ u : Fin 32, anchor64 (anchorFirst32 u) v = true ∧
      anchor64 (anchorFirst32 u) w = true := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.anchorFirst32
theorem OAI.Problem348.anchor64_rows_common_one line 103
Source documentation
Any two rows share a one in the first 32 columns.
```
theorem anchor64_rows_common_one : ∀ u w : Fin 64,
    ∃ v : Fin 32, anchor64 u (anchorFirst32 v) = true ∧
      anchor64 w (anchorFirst32 v) = true := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.anchorFirst32