GuardContainment.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Containment of guarded-path cells in the protected sampling set. The geometric validity of a selection and the cellwise counting bound are separate requirements.

def OAI.Problem348.Construction.HostSampling.RowChosen line 19
Source documentation
A selected row after the independent row reindexing.
```
def RowChosen (row : Position h ≃ Fin n) (s : Seeds (2 ^ h)) (r : Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
def OAI.Problem348.Construction.HostSampling.ColChosen line 23
Source documentation
A selected column after the independent column reindexing.
```
def ColChosen (col : Position h ≃ Fin n) (s : Seeds (2 ^ h)) (c : Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
def OAI.Problem348.Construction.HostSampling.GoodCell line 27
Source documentation
The exact cell predicate needed by transported_guard_frequency.
```
def GoodCell (row col : Position h ≃ Fin n) (s : Seeds (2 ^ h))
    (rc : Fin n × Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.HostSampling.goodCell_of_chosen line 32
structure OAI.Problem348.Construction.HostSampling.FrameChosen line 39
Source documentation
A selected anchor frame, considered only as a family of protected positions.
```
structure FrameChosen (row col : Position h ≃ Fin n) (s : Seeds (2 ^ h))
    (F : AnchorFrame n) : Prop where
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.HostSampling.FrameChosen.cell_good line 47
Source documentation
All anchor and signature cells of a chosen frame are protected and selected.
```
theorem FrameChosen.cell_good {row col : Position h ≃ Fin n} {s : Seeds (2 ^ h)}
    {F : AnchorFrame n} (hF : FrameChosen row col s F)
    {r₀ r₁ c₀ c₁ : Fin n}
    (hr₀ : RowChosen row s r₀) (hr₁ : RowChosen row s r₁)
    (hc₀ : ColChosen col s c₀) (hc₁ : ColChosen col s c₁)
    {rc : Fin n × Fin n} (hcell : F.Cell r₀ r₁ c₀ c₁ rc) :
    GoodCell row col s rc := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.FrameChosen, OAI.Problem348.Construction.HostSampling.RowChosen, OAI.Problem348.Construction.HostSampling.ColChosen, OAI.Problem348.Construction.HostSampling.GoodCell
structure OAI.Problem348.Construction.HostSampling.PathChosen line 67
Source documentation
Purely geometric sampling facts, separate from the host's matrix values.
```
structure PathChosen (row col : Position h ≃ Fin n) (s : Seeds (2 ^ h))
    (P : Selection n) : Prop where
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.HostSampling.PathChosen.core_good line 84
theorem OAI.Problem348.Construction.HostSampling.PathChosen.edge_good line 101
theorem OAI.Problem348.Construction.HostSampling.PathChosen.guard_good line 121
Source documentation
Every actual guarded-path cell is in the protected selected-cell event.
```
theorem PathChosen.guard_good {row col : Position h ≃ Fin n} {s : Seeds (2 ^ h)}
    {P : Selection n} (hP : PathChosen row col s P)
    {rc : Fin n × Fin n} (hc : rc ∈ P.guards h) : GoodCell row col s rc := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.PathChosen, OAI.Problem348.Construction.HostSampling.GoodCell

theorem OAI.Problem348.Construction.HostSampling.path_guard_frequency line 130

Source documentation

The frequency bound for any concretely chosen family of paths.

theorem path_guard_frequency (row col : Position h ≃ Fin n)
    (P : Seeds (2 ^ h) → Selection n)
    (hP : ∀ s, PathChosen row col s (P s)) (rc : Fin n × Fin n) :
    (Finset.univ.filter fun s => rc ∈ (P s).guards h).card * (2 ^ h) ^ 2 ≤
      Fintype.card (Seeds (2 ^ h)) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.PathChosen