HostSampledSelection.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The concrete common-leaf selection in the canonical host

The row/column enumerations are independent. AxisConditions records only the order properties required of those enumerations; entries, role memberships, root values, shared leaves, and the resulting guarded-path validity are proved from the actual canonical host and the concrete sampled positions.

structure OAI.Problem348.Construction.SampledSelection.AxisConditions line 26
Source documentation
The ten order facts used by the sampled-path construction. These are separate from matrix entries and can be supplied by any correct enumeration of the two recursively ordered axes.
```
structure AxisConditions {h n : ℕ} (er ec : Position h ≃ Fin n) : Prop where
…
```
Mentions: OAI.Problem348.Construction.Position
def OAI.Problem348.Construction.SampledSelection.path line 53
Source documentation
A total path; indices beyond the tree depth repeat the common leaf.
```
def path (h i : ℕ) (s : Bool) (z u : Fin (2 ^ h)) : Position h :=
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.SampledSelection.path_of_le line 56
def OAI.Problem348.Construction.SampledSelection.edge line 61
Source documentation
A harmless total extension of the edge index; it equals i for i<h.
```
def edge {h : ℕ} (hh : 1 ≤ h) (i : ℕ) : Fin h :=
…
```
theorem OAI.Problem348.Construction.SampledSelection.edge_of_lt line 64
def OAI.Problem348.Construction.SampledSelection.horizontalMode line 70
Source documentation
The anchor mode for one of the horizontal propagation steps.
```
def horizontalMode {h : ℕ} (hh : 1 ≤ h) (z : Fin (2 ^ h))
    (i : ℕ) (s : Bool) : Mode h :=
…
```
Mentions: OAI.Problem348.Construction.Mode
def OAI.Problem348.Construction.SampledSelection.frame line 77
Source documentation
The selected anchor representatives use the same row/column seed in every anchor group. This correlation does not affect the cellwise sampling proof.
```
def frame {h n : ℕ} (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (t : Mode h) (u v : Fin (2 ^ h)) :
    GuardedPath.AnchorFrame n :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.Mode, OAI.Problem348.GuardedPath.AnchorFrame
def OAI.Problem348.Construction.SampledSelection.selection line 84
Source documentation
The actual selected path and four anchor frames at each edge.
```
def selection {h n : ℕ} (hh : 1 ≤ h) (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (z u v : Fin (2 ^ h)) : GuardedPath.Selection n where
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.GuardedPath.Selection
theorem OAI.Problem348.Construction.SampledSelection.frame_valid line 99
Source documentation
For named body roles, all anchor/signature data follow from the host; only the two body order inequalities need to be supplied.
```
theorem frame_valid {h n : ℕ} (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (t : Mode h) (u v : Fin (2 ^ h))
    (r₀ r₁ c₀ c₁ : Position h)
    (hr₀ : rowRole t 0 r₀) (hr₁ : rowRole t 1 r₁)
    (hc₀ : colRole t 0 c₀) (hc₁ : colRole t 1 c₁)
    (hrs : er r₀ < er r₁) (hcs : ec c₀ < ec c₁) :
    (frame er ec ha t u v).Valid (SelectedAnchor.matrix er ec)
      (er r₀) (er r₁) (ec c₀) (ec c₁) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.SampledSelection.frame, OAI.Problem348.Construction.SelectedAnchor.matrix
theorem OAI.Problem348.Construction.SampledSelection.vertical_plus_valid line 120
theorem OAI.Problem348.Construction.SampledSelection.vertical_minus_valid line 134
theorem OAI.Problem348.Construction.SampledSelection.horizontal_plus_valid line 148
theorem OAI.Problem348.Construction.SampledSelection.horizontal_minus_valid line 164
theorem OAI.Problem348.Construction.SampledSelection.selection_valid line 183
Source documentation
Every concrete three-seed selection satisfies all guarded-path hypotheses. Only the axis order laws were assumed; the entire original-matrix certificate is derived from the exact host entries and the sampled common-leaf path.
```
theorem selection_valid {h n : ℕ} (hh : 1 ≤ h) (er ec : Position h ≃ Fin n)
    (ha : AxisConditions er ec) (z u v : Fin (2 ^ h)) :
    (selection hh er ec ha z u v).Valid (SelectedAnchor.matrix er ec) h := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SampledSelection.AxisConditions, OAI.Problem348.Construction.SampledSelection.selection, OAI.Problem348.Construction.SelectedAnchor.matrix