HostVerticalLocalization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Vertical-mode localization for the concrete host

The only additional input to the exclusion theorems is the node inequality provided by the tree order. All entry values and role memberships follow from the host definitions.

def OAI.Problem348.Construction.positionNode line 17
Source documentation
Extend the variable node index to all positions.
```
def positionNode {h : ℕ} : Position h → ℕ
  | Sum.inr (Sum.inl v) => node v
  | _ => 0
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.node
theorem OAI.Problem348.Construction.positionNode_variable line 21
theorem OAI.Problem348.Construction.variableEntry_same_level line 24
theorem OAI.Problem348.Construction.variableEntry_child_parent line 37
theorem OAI.Problem348.Construction.rowRole_vertical_variable line 48
theorem OAI.Problem348.Construction.colRole_vertical_first_dummy line 57
theorem OAI.Problem348.Construction.colRole_vertical_second_variable line 65
theorem OAI.Problem348.Construction.host_vertical_plus_not_body line 74
Source documentation
An actual vertical plus mode of the host cannot contain the body.
```
theorem host_vertical_plus_not_body {h : ℕ} {t : Mode h}
    (hk : kind t = 0) {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₁)
    (horder : positionNode r₀ / 2 ≤ positionNode r₁) :
    ¬ ModeLocalization.IsP (host r₀ c₀) (host r₀ c₁)
      (host r₁ c₀) (host r₁ c₁) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.kind, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.positionNode, OAI.Problem348.ModeLocalization.IsP, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_vertical_minus_not_body line 100
Source documentation
An actual vertical minus mode of the host cannot contain the body.
```
theorem host_vertical_minus_not_body {h : ℕ} {t : Mode h}
    (hk : kind t = 1) {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₁)
    (horder : positionNode r₀ ≤ positionNode r₁ / 2) :
    ¬ ModeLocalization.IsP (host r₀ c₀) (host r₀ c₁)
      (host r₁ c₀) (host r₁ c₁) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.kind, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.positionNode, OAI.Problem348.ModeLocalization.IsP, OAI.Problem348.Construction.host