SamplingDistance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From sampled protected cells to arbitrary-repair distance

The guard sets comprise only cells that the path proof requires to stay unchanged. The hypotheses do not require preservation of every variable-variable entry or of an original copy of the pattern.

theorem OAI.Problem348.Sampling.hammingDistance_ge_of_guard_sampling line 22

Source documentation

A sparse family of guards with a deterministic obstruction forces a lower bound on every repair to an H-free matrix. The pattern may be arbitrary.

theorem hammingDistance_ge_of_guard_sampling
    {k n : ℕ} {Ω : Type uOmega} [Fintype Ω]
    (H : BinaryMatrix k) (A B : BinaryMatrix n)
    (guard : Ω → Finset (Fin n × Fin n)) (m : ℕ)
    (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ e,
      (Finset.univ.filter (fun ω => e ∈ guard ω)).card * m ^ 2 ≤ Fintype.card Ω)
    (hforce : ∀ ω,
      (∀ e ∈ guard ω, A e.1 e.2 = B e.1 e.2) → ¬ HFree H B)
    (hfree : HFree H B) : m ^ 2 ≤ hammingDistance A B := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.hammingDistance

theorem OAI.Problem348.Sampling.hammingDistance_ge_of_three_seed_guards line 48

Source documentation

The three-seed specialization: a guard uses each cell in at most m of the m³ samples. Therefore no H-free repair changes fewer than m² entries.

theorem hammingDistance_ge_of_three_seed_guards
    {k n : ℕ} (m : ℕ) (hm : 0 < m)
    (H : BinaryMatrix k) (A B : BinaryMatrix n)
    (guard : (Fin m × Fin m × Fin m) → Finset (Fin n × Fin n))
    (hbound : ∀ e, (Finset.univ.filter (fun ω => e ∈ guard ω)).card ≤ m)
    (hforce : ∀ ω,
      (∀ e ∈ guard ω, A e.1 e.2 = B e.1 e.2) → ¬ HFree H B)
    (hfree : HFree H B) : m ^ 2 ≤ hammingDistance A B := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.hammingDistance

theorem OAI.Problem348.Sampling.guard_frequency_le line 69

Source documentation

A guard-frequency estimate can be obtained from a larger set of protected selected cells. This is useful when the deterministic path proof uses just a subset of all selected anchor, dummy, and root incidences.

theorem guard_frequency_le {Ω : Type uOmega} {Cell : Type uCell} [Fintype Ω] [DecidableEq Cell]
    (guard : Ω → Finset Cell) (selected : Ω → Cell → Prop)
    [DecidableRel selected]
    (hsub : ∀ ω e, e ∈ guard ω → selected ω e) (e : Cell) :
    (Finset.univ.filter (fun ω => e ∈ guard ω)).card ≤
      (Finset.univ.filter (fun ω => selected ω e)).card := by
…