OAI/Combinatorics/MatrixRemoval/SelectedAnchorSparsity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Sparsity for arbitrary selected raw host positions. Only the selected core is assumed to consist of anchors; outside it the selection may include variable and dummy positions.

  1. def OAI.Problem348.Construction.SelectedAnchors.label line 16

    Source documentation

    Anchor mode and group, forgetting the irrelevant within-group offset.

    def label {h : ℕ} : Position h → Option (Mode h × Fin 64)
  | .inl a => some (a.1, a.2.1)
  | .inr _ => none

/-- The mode classifier used by the abstract rigidity theorem. -/

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.SelectedAnchors.mode

  2. def OAI.Problem348.Construction.SelectedAnchors.mode line 21

    Source documentation

    The mode classifier used by the abstract rigidity theorem.

    def mode {h : ℕ} : Position h → Option (Mode h)
  | .inl a => some a.1
  | .inr _ => none

/-- Group uniqueness only concerns anchors, so it permits many nonanchors. -/

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode

  3. def OAI.Problem348.Construction.SelectedAnchors.GroupInjective line 26

    Source documentation

    Group uniqueness only concerns anchors, so it permits many nonanchors.

    def GroupInjective {I : Type uI} {h : ℕ} (f : I → Position h) : Prop :=
…

    Mentions: OAI.Problem348.Construction.Position

  4. theorem OAI.Problem348.Construction.SelectedAnchors.variable_row_core_card_le_four line 31

    Source documentation

    Restrict the actual sparse-row theorem to an arbitrary selected anchor core.

    theorem variable_row_core_card_le_four {I : Type uI} [DecidableEq I] {h : ℕ}
    (f : I → Position h) (S : Finset I) (v : VariablePosition h)
    (hanchor : ∀ i ∈ S, ∃ a, f i = .inl a)
    (hgroups : Set.InjOn (fun i => label (f i)) (S : Set I)) :
    (S.filter (fun i => host (.inr (.inl v)) (f i) = true)).card ≤ 4 := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.SelectedAnchors.label, OAI.Problem348.Construction.host

  5. theorem OAI.Problem348.Construction.SelectedAnchors.variable_col_core_card_le_four line 53

    Source documentation

    The transpose restriction to a selected anchor core.

    theorem variable_col_core_card_le_four {I : Type uI} [DecidableEq I] {h : ℕ}
    (f : I → Position h) (S : Finset I) (v : VariablePosition h)
    (hanchor : ∀ i ∈ S, ∃ a, f i = .inl a)
    (hgroups : Set.InjOn (fun i => label (f i)) (S : Set I)) :
    (S.filter (fun i => host (f i) (.inr (.inl v)) = true)).card ≤ 4 := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.SelectedAnchors.label, OAI.Problem348.Construction.host

  6. theorem OAI.Problem348.Construction.SelectedAnchors.GroupInjective.injOn line 75

    Source documentation

    The structural group-uniqueness property gives label injectivity on a core.

    theorem GroupInjective.injOn {I : Type uI} {h : ℕ} {f : I → Position h}
    (hf : GroupInjective f) (S : Set I)
    (hanchor : ∀ i ∈ S, ∃ a, f i = .inl a) :
    Set.InjOn (fun i => label (f i)) S := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.SelectedAnchors.label

  7. theorem OAI.Problem348.Construction.SelectedAnchors.nonanchor_row_unit line 88

    Source documentation

    Exact nonanchor-row unit hypothesis of the abstract rigidity theorem.

    theorem nonanchor_row_unit {I : Type uI} {h : ℕ}
    (f : I → Position h) (hf : GroupInjective f)
    (r : VariablePosition h ⊕ Fin (2 ^ h)) (i j : I) (t : Mode h)
    (hi : mode (f i) = some t) (hj : mode (f j) = some t)
    (hri : host (.inr r) (f i) = true)
    (hrj : host (.inr r) (f j) = true) : i = j := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.host

  8. theorem OAI.Problem348.Construction.SelectedAnchors.nonanchor_col_unit line 106

    Source documentation

    Exact nonanchor-column unit hypothesis of the abstract rigidity theorem.

    theorem nonanchor_col_unit {I : Type uI} {h : ℕ}
    (f : I → Position h) (hf : GroupInjective f)
    (c : VariablePosition h ⊕ Fin (2 ^ h)) (i j : I) (t : Mode h)
    (hi : mode (f i) = some t) (hj : mode (f j) = some t)
    (hci : host (f i) (.inr c) = true)
    (hcj : host (f j) (.inr c) = true) : i = j := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.host

  9. def OAI.Problem348.Construction.SelectedAnchors.IsDummy line 124

    Source documentation

    The raw dummy-position predicate.

    def IsDummy {h : ℕ} (p : Position h) : Prop :=
…

    Mentions: OAI.Problem348.Construction.Position

  10. theorem OAI.Problem348.Construction.SelectedAnchors.variable_of_mode_none_not_dummy line 128

    Source documentation

    A mode-free non-dummy position is a variable position.

    theorem variable_of_mode_none_not_dummy {h : ℕ} (p : Position h)
    (hm : mode p = none) (hd : ¬ IsDummy p) :
    ∃ v, p = .inr (.inl v) := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.SelectedAnchors.IsDummy

  11. theorem OAI.Problem348.Construction.SelectedAnchors.sparse_column_of_mode_none line 137

    Source documentation

    The exact variable-column sparsity input of one-sided anchor rigidity.

    theorem sparse_column_of_mode_none {I : Type uI} [DecidableEq I] {h : ℕ}
    (f : I → Position h) (S : Finset I) (p : Position h)
    (hanchor : ∀ i ∈ S, ∃ a, f i = .inl a)
    (hgroups : GroupInjective f)
    (hm : mode p = none) (hd : ¬ IsDummy p) :
    (S.filter (fun i => host (f i) p = true)).card ≤ 4 := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.SelectedAnchors.IsDummy, OAI.Problem348.Construction.host

  12. theorem OAI.Problem348.Construction.SelectedAnchors.sparse_row_of_mode_none line 148

    Source documentation

    The axis-transposed sparsity input.

    theorem sparse_row_of_mode_none {I : Type uI} [DecidableEq I] {h : ℕ}
    (f : I → Position h) (S : Finset I) (p : Position h)
    (hanchor : ∀ i ∈ S, ∃ a, f i = .inl a)
    (hgroups : GroupInjective f)
    (hm : mode p = none) (hd : ¬ IsDummy p) :
    (S.filter (fun i => host p (f i) = true)).card ≤ 4 := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.SelectedAnchors.IsDummy, OAI.Problem348.Construction.host

  13. theorem OAI.Problem348.Construction.SelectedAnchors.cross_mode line 159

    Source documentation

    An anchor-anchor one forces equality of the two mode labels.

    theorem cross_mode {h : ℕ} (r c : Position h) (t u : Mode h)
    (hr : mode r = some t) (hc : mode c = some u)
    (hentry : host r c = true) : t = u := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.host

  14. theorem OAI.Problem348.Construction.SelectedAnchors.nonanchor_row_unit_of_mode_none line 173

    Source documentation

    Raw-position form matching the abstract nonanchor-row unit hypothesis.

    theorem nonanchor_row_unit_of_mode_none {I : Type uI} {h : ℕ}
    (f : I → Position h) (hf : GroupInjective f) (r : Position h)
    (hr : mode r = none) (i j : I) (t : Mode h)
    (hi : mode (f i) = some t) (hj : mode (f j) = some t)
    (hri : host r (f i) = true) (hrj : host r (f j) = true) : i = j := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host

  15. theorem OAI.Problem348.Construction.SelectedAnchors.nonanchor_col_unit_of_mode_none line 183

    Source documentation

    Raw-position form matching the abstract nonanchor-column unit hypothesis.

    theorem nonanchor_col_unit_of_mode_none {I : Type uI} {h : ℕ}
    (f : I → Position h) (hf : GroupInjective f) (c : Position h)
    (hc : mode c = none) (i j : I) (t : Mode h)
    (hi : mode (f i) = some t) (hj : mode (f j) = some t)
    (hci : host (f i) c = true) (hcj : host (f j) c = true) : i = j := by
…

    Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.SelectedAnchors.GroupInjective, OAI.Problem348.Construction.SelectedAnchors.mode, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host