CopyBoundFixed.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem348.copyCount_le_of_cell_mem line 9

Source documentation

Ordered-copy specialization of the generic constrained-cell bound.

theorem copyCount_le_of_cell_mem {k n : ℕ}
    (H : BinaryMatrix (k + 1)) (A : BinaryMatrix n)
    (i j : Fin (k + 1)) (L : Finset (Fin n × Fin n))
    (hL : ∀ rc ∈ orderedCopies H A, (rc.1.val i, rc.2.val j) ∈ L) :
    copyCount H A ≤ L.card * n ^ (2 * k) :=
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.orderedCopies, OAI.Problem348.copyCount

theorem OAI.Problem348.fixedCopyCount_le_of_body_cell_mem line 17
Source documentation
Locate the top-left body entry (zero-based index 64) to count fixed-H copies.
```
theorem fixedCopyCount_le_of_body_cell_mem {n : ℕ}
    (A : BinaryMatrix n) (L : Finset (Fin n × Fin n))
    (hL : ∀ rc ∈ orderedCopies fixedH A, (rc.1.val 64, rc.2.val 64) ∈ L) :
    copyCount fixedH A ≤ L.card * n ^ 130 :=
…
```
Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.orderedCopies, OAI.Problem348.fixedH, OAI.Problem348.copyCount

theorem OAI.Problem348.fixedCopyDensity_le_of_body_cell_mem line 24

Source documentation

The copy bound reduced to concrete leaf localization.

theorem fixedCopyDensity_le_of_body_cell_mem {d m : ℕ}
    (hd : 0 < d) (hm : 0 < m) (A : BinaryMatrix (d * m))
    (L : Finset (Fin (d * m) × Fin (d * m))) (hcard : L.card ≤ m)
    (hL : ∀ rc ∈ orderedCopies fixedH A, (rc.1.val 64, rc.2.val 64) ∈ L) :
    (copyCount fixedH A : ℝ) / (((d * m : ℕ) : ℝ) ^ 132) ≤
      (1 / ((d : ℝ) ^ 2)) * (1 / (m : ℝ)) := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.orderedCopies, OAI.Problem348.fixedH, OAI.Problem348.copyCount

theorem OAI.Problem348.sequenceCopyDensity_le_of_body_cell_mem line 35

Source documentation

The exact numerical upper bound appearing in counterexample_sequence.

theorem sequenceCopyDensity_le_of_body_cell_mem (h : ℕ)
    (A : BinaryMatrix ((386 * h + 2) * 2 ^ h))
    (L : Finset
      (Fin ((386 * h + 2) * 2 ^ h) × Fin ((386 * h + 2) * 2 ^ h)))
    (hcard : L.card ≤ 2 ^ h)
    (hL : ∀ rc ∈ orderedCopies fixedH A, (rc.1.val 64, rc.2.val 64) ∈ L) :
    (copyCount fixedH A : ℝ) / ((((386 * h + 2) * 2 ^ h : ℕ) : ℝ) ^ 132) ≤
      (1 / (((386 * h + 2 : ℕ) : ℝ) ^ 2)) * (1 / ((2 : ℝ) ^ h)) := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.orderedCopies, OAI.Problem348.fixedH, OAI.Problem348.copyCount

theorem OAI.Problem348.sequenceCopyDensity_le_of_leaf_witness line 49

Source documentation

A localization witness is enough; no separate leaf-cell set or injectivity proof is required for the upper bound. Images can only decrease cardinality.

theorem sequenceCopyDensity_le_of_leaf_witness (h : ℕ)
    (A : BinaryMatrix ((386 * h + 2) * 2 ^ h))
    (rowLeaf colLeaf : Fin (2 ^ h) → Fin ((386 * h + 2) * 2 ^ h))
    (hloc : ∀ r c : IncreasingMap 66 ((386 * h + 2) * 2 ^ h),
      (∀ i j, A (r.val i) (c.val j) = fixedH i j) →
      ∃ z, r.val 64 = rowLeaf z ∧ c.val 64 = colLeaf z) :
    (copyCount fixedH A : ℝ) / ((((386 * h + 2) * 2 ^ h : ℕ) : ℝ) ^ 132) ≤
      (1 / (((386 * h + 2 : ℕ) : ℝ) ^ 2)) * (1 / ((2 : ℝ) ^ h)) := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.IncreasingMap, OAI.Problem348.fixedH, OAI.Problem348.copyCount