HostModeIncidence.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The mode-incidence count bounds sparse anchor traces for the actual finite host.

def OAI.Problem348.Construction.incidenceKind line 15
def OAI.Problem348.Construction.incidenceMode line 20
Source documentation
Decode the canonical six-mode enumeration into the incidence labels.
```
def incidenceMode {h : ℕ} (t : Mode h) : ModeIncidence.Mode :=
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.ModeIncidence.Mode
def OAI.Problem348.Construction.nodeParity line 24
Source documentation
Boolean parity, in the convention used by ModeIncidence.
```
def nodeParity {h : ℕ} (v : VariablePosition h) : Bool :=
…
```
Mentions: OAI.Problem348.Construction.VariablePosition
theorem OAI.Problem348.Construction.incidenceKind_injective line 27
theorem OAI.Problem348.Construction.incidenceMode_injective line 31
theorem OAI.Problem348.Construction.rowRole_incident line 42
theorem OAI.Problem348.Construction.colRole_incident line 53
theorem OAI.Problem348.Construction.card_rowRole_modes_le_four line 65
Source documentation
The actual canonical variable row meets at most four modes.
```
theorem card_rowRole_modes_le_four {h : ℕ} (v : VariablePosition h)
    (s : Finset (Mode h))
    (hs : ∀ t ∈ s, ∃ j, rowRole t j (.inr (.inl v))) : s.card ≤ 4 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.rowRole
theorem OAI.Problem348.Construction.card_colRole_modes_le_four line 76
Source documentation
The actual canonical variable column meets at most four modes.
```
theorem card_colRole_modes_le_four {h : ℕ} (v : VariablePosition h)
    (s : Finset (Mode h))
    (hs : ∀ t ∈ s, ∃ j, colRole t j (.inr (.inl v))) : s.card ≤ 4 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.colRole
theorem OAI.Problem348.Construction.row_anchor_ones_unique_group line 87
Source documentation
A nonanchor row has at most one one-bearing anchor group in each mode.
```
theorem row_anchor_ones_unique_group {h : ℕ}
    (x : VariablePosition h ⊕ Fin (2 ^ h))
    (a b : AnchorPosition h)
    (ha : host (.inr x) (.inl a) = true)
    (hb : host (.inr x) (.inl b) = true)
    (hm : a.1 = b.1) : a.2.1 = b.2.1 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AnchorPosition, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.col_anchor_ones_unique_group line 106
Source documentation
The corresponding unit-signature fact for a nonanchor column.
```
theorem col_anchor_ones_unique_group {h : ℕ}
    (x : VariablePosition h ⊕ Fin (2 ^ h))
    (a b : AnchorPosition h)
    (ha : host (.inl a) (.inr x) = true)
    (hb : host (.inl b) (.inr x) = true)
    (hm : a.1 = b.1) : a.2.1 = b.2.1 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AnchorPosition, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.card_variable_row_anchor_ones_le_four line 126
Source documentation
The concrete sparse-anchor-trace conclusion for arbitrary indexed anchor representatives: no group is represented twice among the selected indices.
```
theorem card_variable_row_anchor_ones_le_four {h : ℕ} {α : Type uAlpha}
    [DecidableEq α] (v : VariablePosition h) (s : Finset α)
    (a : α → AnchorPosition h)
    (hgroups : Set.InjOn (fun x => ((a x).1, (a x).2.1)) (s : Set α)) :
    (s.filter (fun x => host (.inr (.inl v)) (.inl (a x)) = true)).card ≤ 4 := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AnchorPosition, OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.card_variable_col_anchor_ones_le_four line 150

Source documentation

The concrete sparse-anchor-trace conclusion for a variable column.

theorem card_variable_col_anchor_ones_le_four {h : ℕ} {α : Type uAlpha}
    [DecidableEq α] (v : VariablePosition h) (s : Finset α)
    (a : α → AnchorPosition h)
    (hgroups : Set.InjOn (fun x => ((a x).1, (a x).2.1)) (s : Set α)) :
    (s.filter (fun x => host (.inl (a x)) (.inr (.inl v)) = true)).card ≤ 4 := by
…

Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AnchorPosition, OAI.Problem348.Construction.host