SequenceAssembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the counterexample sequence from two integer bounds. The existence of a host satisfying both bounds is an explicit hypothesis.

def OAI.Problem348.SequenceAssembly.HostBounds line 15
Source documentation
Integer certificates for one candidate host. This does not assert existence.
```
def HostBounds {n : ℕ} (A : BinaryMatrix n) (m : ℕ) : Prop :=
…
```
Mentions: OAI.Problem348.BinaryMatrix
theorem OAI.Problem348.SequenceAssembly.fixedMinEdits_ge_of_repairs line 20
Source documentation
The sentinel value in fixedMinEdits respects every lower bound at most n².
```
theorem fixedMinEdits_ge_of_repairs {n q : ℕ} (A : BinaryMatrix n)
    (hq : q ≤ n * n)
    (hrep : ∀ B : BinaryMatrix n, HFree fixedH B → q ≤ hammingDistance A B) :
    q ≤ fixedMinEdits A := by
…
```
Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH, OAI.Problem348.hammingDistance, OAI.Problem348.fixedMinEdits
theorem OAI.Problem348.SequenceAssembly.fixedDistance_ge_of_integer_bound line 34
Source documentation
Normalize an arbitrary-repair certificate at order n=d*m.
```
theorem fixedDistance_ge_of_integer_bound {d m : ℕ}
    (hd : 0 < d) (hm : 0 < m) (A : BinaryMatrix (d * m))
    (hrep : ∀ B : BinaryMatrix (d * m), HFree fixedH B →
      m ^ 2 ≤ hammingDistance A B) :
    1 / ((d : ℝ) ^ 2) ≤ fixedDistance A := by
…
```
Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH, OAI.Problem348.hammingDistance, OAI.Problem348.fixedDistance

theorem OAI.Problem348.SequenceAssembly.copyDensity_le_of_integer_bound line 54

Source documentation

Normalize the localized-copy integer estimate at order n=d*m.

theorem copyDensity_le_of_integer_bound {d m : ℕ}
    (hd : 0 < d) (hm : 0 < m) (A : BinaryMatrix (d * m))
    (hcount : copyCount fixedH A ≤ m * (d * m) ^ 130) :
    (copyCount fixedH A : ℝ) / (((d * m : ℕ) : ℝ) ^ 132) ≤
      (1 / ((d : ℝ) ^ 2)) * (1 / (m : ℝ)) := by
…

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

theorem OAI.Problem348.SequenceAssembly.counterexample_sequence_of_integer_bounds line 71
Source documentation
The counterexample sequence follows from the integer bounds.
```
theorem counterexample_sequence_of_integer_bounds
    (hcert : ∀ h : ℕ, 1 ≤ h →
      let d : ℕ := 386 * h + 2
…
```