ModeIncidence.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Mode-incidence bounds. Active modes have levels 1 through h, while variable positions have levels 0 through h. At level h the plus and minus blocks coincide.

inductive OAI.Problem348.ModeIncidence.Kind line 15
abbrev OAI.Problem348.ModeIncidence.Mode line 20
def OAI.Problem348.ModeIncidence.hasSign line 23
Source documentation
Leaf positions have both sign names; other positions have their own sign.
```
def hasSign (h depth : ℕ) (own requested : Bool) : Prop :=
…
```
def OAI.Problem348.ModeIncidence.rowIncident line 27
Source documentation
Incidence with either row role of a mode.
```
def rowIncident (h depth : ℕ) (sign parity : Bool) (t : Mode) : Prop :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.ModeIncidence.colIncident line 34
Source documentation
Incidence with either column role of a mode.
```
def colIncident (h depth : ℕ) (sign parity : Bool) (t : Mode) : Prop :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.ModeIncidence.internalRowModes line 43
Source documentation
Three possible modes for an internal variable row. Boundary levels may remove some of these modes.
```
def internalRowModes (depth : ℕ) (sign parity : Bool) : Finset Mode :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.ModeIncidence.leafRowModes line 48
Source documentation
The four possible modes for a shared leaf row.
```
def leafRowModes (h : ℕ) (parity : Bool) : Finset Mode :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.ModeIncidence.internalColModes line 53
Source documentation
Four possible modes for an internal variable column.
```
def internalColModes (depth : ℕ) (sign parity : Bool) : Finset Mode :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.ModeIncidence.leafColModes line 58
Source documentation
The two possible modes for a shared leaf column.
```
def leafColModes (h : ℕ) (parity : Bool) : Finset Mode :=
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode
theorem OAI.Problem348.ModeIncidence.rowIncident_internal line 61
theorem OAI.Problem348.ModeIncidence.rowIncident_leaf line 77
theorem OAI.Problem348.ModeIncidence.colIncident_internal line 90
theorem OAI.Problem348.ModeIncidence.colIncident_leaf line 110
theorem OAI.Problem348.ModeIncidence.card_internalRowModes_le line 124
Source documentation
An internal row participates in at most three modes.
```
theorem card_internalRowModes_le (depth : ℕ) (sign parity : Bool) :
    (internalRowModes depth sign parity).card ≤ 3 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.internalRowModes
theorem OAI.Problem348.ModeIncidence.card_leafRowModes_le line 131
Source documentation
A leaf row participates in at most four modes.
```
theorem card_leafRowModes_le (h : ℕ) (parity : Bool) :
    (leafRowModes h parity).card ≤ 4 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.leafRowModes
theorem OAI.Problem348.ModeIncidence.card_internalColModes_le line 136
Source documentation
A variable column below the leaf level participates in at most four modes.
```
theorem card_internalColModes_le (depth : ℕ) (sign parity : Bool) :
    (internalColModes depth sign parity).card ≤ 4 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.internalColModes
theorem OAI.Problem348.ModeIncidence.card_leafColModes_le line 144
Source documentation
A leaf column participates in at most two modes.
```
theorem card_leafColModes_le (h : ℕ) (parity : Bool) :
    (leafColModes h parity).card ≤ 2 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.leafColModes
theorem OAI.Problem348.ModeIncidence.card_row_incident_le_four line 149
Source documentation
Formulation independent of the particular finite enumeration of valid modes.
```
theorem card_row_incident_le_four {h depth : ℕ} {sign parity : Bool}
    (hd : depth ≤ h) (modes : Finset Mode)
    (hmodes : ∀ t ∈ modes, rowIncident h depth sign parity t) :
    modes.card ≤ 4 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode, OAI.Problem348.ModeIncidence.rowIncident
theorem OAI.Problem348.ModeIncidence.card_col_incident_le_four line 165
Source documentation
Formulation independent of the particular finite enumeration of valid modes.
```
theorem card_col_incident_le_four {h depth : ℕ} {sign parity : Bool}
    (hd : depth ≤ h) (modes : Finset Mode)
    (hmodes : ∀ t ∈ modes, colIncident h depth sign parity t) :
    modes.card ≤ 4 := by
…
```
Mentions: OAI.Problem348.ModeIncidence.Mode, OAI.Problem348.ModeIncidence.colIncident

theorem OAI.Problem348.ModeIncidence.card_ones_le_of_mode_bound line 181

Source documentation

A generic sparse-trace transfer: at most one chosen one-entry per mode.

theorem card_ones_le_of_mode_bound {α : Type uAlpha} [DecidableEq α]
    (positions : Finset α) (mode : α → Mode) (entry : α → Bool)
    (incident : Mode → Prop) (bound : ℕ)
    (hbound : ∀ modes : Finset Mode,
      (∀ t ∈ modes, incident t) → modes.card ≤ bound)
    (hincident : ∀ x ∈ positions, entry x = true → incident (mode x))
    (hunique : ∀ x ∈ positions, ∀ y ∈ positions,
      entry x = true → entry y = true → mode x = mode y → x = y) :
    (positions.filter (fun x => entry x = true)).card ≤ bound := by
…

Mentions: OAI.Problem348.ModeIncidence.Mode

theorem OAI.Problem348.ModeIncidence.card_row_ones_le_four line 205

Source documentation

Against anchor representatives, a variable row has at most four ones, provided one-entries in the same mode use the same representative.

theorem card_row_ones_le_four {α : Type uAlpha} [DecidableEq α]
    {h depth : ℕ} {sign parity : Bool} (hd : depth ≤ h)
    (positions : Finset α) (mode : α → Mode) (entry : α → Bool)
    (hincident : ∀ x ∈ positions, entry x = true →
      rowIncident h depth sign parity (mode x))
    (hunique : ∀ x ∈ positions, ∀ y ∈ positions,
      entry x = true → entry y = true → mode x = mode y → x = y) :
    (positions.filter (fun x => entry x = true)).card ≤ 4 :=
…

Mentions: OAI.Problem348.ModeIncidence.Mode, OAI.Problem348.ModeIncidence.rowIncident

theorem OAI.Problem348.ModeIncidence.card_col_ones_le_four line 218

Source documentation

The symmetric sparse-trace statement for variable columns.

theorem card_col_ones_le_four {α : Type uAlpha} [DecidableEq α]
    {h depth : ℕ} {sign parity : Bool} (hd : depth ≤ h)
    (positions : Finset α) (mode : α → Mode) (entry : α → Bool)
    (hincident : ∀ x ∈ positions, entry x = true →
      colIncident h depth sign parity (mode x))
    (hunique : ∀ x ∈ positions, ∀ y ∈ positions,
      entry x = true → entry y = true → mode x = mode y → x = y) :
    (positions.filter (fun x => entry x = true)).card ≤ 4 :=
…

Mentions: OAI.Problem348.ModeIncidence.Mode, OAI.Problem348.ModeIncidence.colIncident