OrderedRepairDistance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Unconditional repair lower bound for the ordered canonical host

The sampler order certificate follows from the independent increasing row and column enumerations, giving the arbitrary-repair lower bound.

theorem OAI.Problem348.OrderedHost.hammingDistance_ge line 20
Source documentation
Every fixedH-free repair of the actual ordered host changes at least m² cells. In particular no pinning premise or preservation condition is assumed.
```
theorem hammingDistance_ge {h : ℕ} (hh : 1 ≤ h)
    (B : BinaryMatrix (size h)) (hfree : HFree fixedH B) :
    (2 ^ h) ^ 2 ≤
      hammingDistance (SelectedAnchor.matrix (rowIndex h) (columnIndex h)) B :=
…
```
Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.OrderedHost.size, OAI.Problem348.HFree, OAI.Problem348.fixedH, OAI.Problem348.hammingDistance, OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex

theorem OAI.Problem348.OrderedHost.sampledSelection_guard_frequency line 28

Source documentation

The concrete three-seed sampler has the exact uniform guard bound.

theorem sampledSelection_guard_frequency {h : ℕ} (hh : 1 ≤ h)
    (rc : Fin (size h) × Fin (size h)) :
    (Finset.univ.filter fun s : TreeSampling.Seeds (2 ^ h) =>
      rc ∈ (sampledSelection hh s.1 s.2.1 s.2.2).guards h).card * (2 ^ h) ^ 2 ≤
        Fintype.card (TreeSampling.Seeds (2 ^ h)) :=
…

Mentions: OAI.Problem348.OrderedHost.size, OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.OrderedHost.sampledSelection