OrderedHostCopy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ordered-copy localization and counting

The six-mode body theorem places the distinguished cell at a shared leaf. The count needs only anchor pinning, not a further order certificate.

theorem OAI.Problem348.OrderedHost.orderedBodyLocalizes line 18
Source documentation
The six-mode theorem supplies the exact body-localization counting input.
```
theorem orderedBodyLocalizes (h : ℕ) :
    OrderedBodyLocalizes (rowIndex h) (columnIndex h) := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex

theorem OAI.Problem348.OrderedHost.matching_copy_leaf_of_pinning line 24

Source documentation

Every matching ordered copy has its top-left body cell at a shared leaf.

theorem matching_copy_leaf_of_pinning (h : ℕ)
    (hpin : Anchor64Pinned (rowIndex h) (columnIndex h))
    (r c : Fin 66 → Position h)
    (hr : StrictMono (fun i => rowIndex h (r i)))
    (hc : StrictMono (fun j => columnIndex h (c j)))
    (hmatch : ∀ i j, host (r i) (c j) = fixedH i j) :
    ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z :=
…

Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.fixedH

theorem OAI.Problem348.OrderedHost.copyCount_le_of_pinning line 35
Source documentation
Integer copy bound for the actual two-axis enumeration.
```
theorem copyCount_le_of_pinning (h : ℕ)
    (hpin : Anchor64Pinned (rowIndex h) (columnIndex h)) :
    copyCount fixedH (hostMatrix (rowIndex h) (columnIndex h)) ≤
      2 ^ h * (size h) ^ 130 :=
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.copyCount, OAI.Problem348.fixedH, OAI.Problem348.OrderedHost.size
theorem OAI.Problem348.OrderedHost.copyDensity_le_of_pinning line 43
Source documentation
The normalized copy bound, conditional only on anchor pinning.
```
theorem copyDensity_le_of_pinning (h : ℕ)
    (hpin : Anchor64Pinned (rowIndex h) (columnIndex h)) :
    (copyCount fixedH (hostMatrix (rowIndex h) (columnIndex h)) : ℝ) /
        ((size h : ℝ) ^ 132) ≤
      (1 / (((386 * h + 2 : ℕ) : ℝ) ^ 2)) * (1 / ((2 : ℝ) ^ h)) :=
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.copyCount, OAI.Problem348.fixedH, OAI.Problem348.OrderedHost.size