HostRepairDistance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary-repair lower bound for the actual canonical host

The concrete common-leaf selection satisfies both independent certificates: its guarded path is valid, and its chosen coordinates bound each guard cell's sampling multiplicity. Together these prove the integer repair lower bound. No assumption about preservation of arbitrary variable-variable cells is made.

theorem OAI.Problem348.Construction.SampledSelection.frame_chosen line 22
Source documentation
The actual constant-offset anchor frame is chosen by its row/column seeds.
```
theorem frame_chosen {h n : ℕ} (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (s : Seeds (2 ^ h)) (t : Mode h) :
    FrameChosen er ec s (frame er ec ha t s.2.1 s.2.2) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.SampledSelection.frame
theorem OAI.Problem348.Construction.SampledSelection.selection_chosen line 37
Source documentation
Every actual path point and anchor frame obeys the uniform sampler's coordinate equations. This is separate from all matrix-entry claims.
```
theorem selection_chosen {h n : ℕ} (hh : 1 ≤ h) (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (s : Seeds (2 ^ h)) :
    PathChosen er ec s (selection hh er ec ha s.1 s.2.1 s.2.2) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.SampledSelection.selection
theorem OAI.Problem348.Construction.SampledSelection.selection_guard_frequency line 68
Source documentation
Each fixed guarded cell occupies at most the prescribed 1/m² fraction of the three-seed sample space, for the actual selected paths.
```
theorem selection_guard_frequency {h n : ℕ} (hh : 1 ≤ h)
    (er ec : Position h ≃ Fin n) (ha : AxisConditions er ec)
    (rc : Fin n × Fin n) :
    (Finset.univ.filter fun s : Seeds (2 ^ h) =>
      rc ∈ (selection hh er ec ha s.1 s.2.1 s.2.2).guards h).card * (2 ^ h) ^ 2 ≤
        Fintype.card (Seeds (2 ^ h)) :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.SampledSelection.selection
theorem OAI.Problem348.Construction.SampledSelection.hammingDistance_ge line 83
Source documentation
The arbitrary-repair lower bound for the literal canonical host. The independent axis enumerations satisfy AxisConditions: increasing anchor groups precede all nonanchors, variable rows precede dummy rows, dummy columns precede variable columns, and sampled parent/child pairs obey the four signed tree-order inequalities. No entry-preservation condition is imposed on repairs.
```
theorem hammingDistance_ge {h n : ℕ} (hh : 1 ≤ h)
    (er ec : Position h ≃ Fin n) (ha : AxisConditions er ec)
    (B : BinaryMatrix n) (hfree : HFree fixedH B) :
    (2 ^ h) ^ 2 ≤ hammingDistance (SelectedAnchor.matrix er ec) B := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH, OAI.Problem348.hammingDistance, OAI.Problem348.Construction.SelectedAnchor.matrix