Hydrophobic-polar protein folding model: main theoretical development

A treatment of the hydrophobic-polar protein folding model in a generality that covers rectangular, triangular and hexagonal lattices: P_rect, P_tri, P_hex.

We formalize the non-monotonicity of the objective function, refuting an unpublished conjecture of Stecher.

We prove objective function bounds: P_tri ≤ P_rect ≤ P_hex (using a theory of embeddings) and for any model, P ≤ b * l and P ≤ l * (l-1)/2 [see pts_earned_bound_loc']

(The latter is worth keeping when l ≤ 2b+1.)

where b is the number of moves and l is the word length. We also prove P ≤ b * l / 2 using "handshake lemma" type reasoning that was pointed out in Agarwala, Batzoglou et al. (RECOMB 97, Lemma 2.1) and a symmetry assumption on the folding model that holds for rect and hex but not for tri. The latter result required improving our definitions.

We prove the correctness of our backtracking algorithm for protein folding.

To prove some results about rotations (we can always assume our fold starts by going to the right) we use the type Fin n → α instead of Vector α n

def morphSep {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (l : List (Fin b₀)) : List (Fin b₁)

Extend a map on moves to lists. Trying a new def. Sep 13, 2024.

Equations

• morphSep f go₀ [] = []
• morphSep f go₀ (head :: tail) = f head (path go₀ tail).head :: morphSep f go₀ tail

theorem morphSep_len {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (l : List (Fin b₀)) : (morphSep f go₀ l).length = l.length

morph is length-preserving. New proof Sep 13, 2024 using rw [← itself].

def morphSepᵥ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (v : List.Vector (Fin b₀) l) : List.Vector (Fin b₁) l

.

Equations

• morphSepᵥ f go₀ v = ⟨morphSep f go₀ ↑v, ⋯⟩

theorem morphSep_nil {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) : morphSep f go₀ [] = []

.

def morph {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (l : List (Fin b₀)) : List (Fin b₁)

Extend a map on moves to lists.

Equations

• morph f go₀ l = List.rec [] (fun (head : Fin b₀) (tail : List (Fin b₀)) (tail_ih : List (Fin b₁)) => f head (path go₀ tail).head :: tail_ih) l

theorem morph_len {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (l : List (Fin b₀)) : (morph f go₀ l).length = l.length

morph is length-preserving

def morphᵥ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (v : List.Vector (Fin b₀) l) : List.Vector (Fin b₁) l

.

Equations

• morphᵥ f go₀ v = ⟨morph f go₀ ↑v, ⋯⟩

def morf {l b₀ b₁ : ℕ} (f : Fin b₀ → Fin b₁) (v : List.Vector (Fin b₀) l) : List.Vector (Fin b₁) l

.

Equations

• morf f v = List.Vector.map f v

def morfF {l b₀ b₁ : ℕ} (f : Fin b₀ → Fin b₁) (v : Fin l → Fin b₀) : Fin l → Fin b₁

Here, "f" means: f doesn't depend on space. "F" means: use Fin not Vector 3/10/24. Hopefully simple enough to prove a lot about it.

Equations

• morfF f v i = f (v i)

def morf_list {b₀ b₁ : ℕ} (f : Fin b₀ → Fin b₁) (v : List (Fin b₀)) : List (Fin b₁)

.

Equations

• morf_list f v = List.map f v

theorem morf_len {b₀ b₁ : ℕ} (f : Fin b₀ → Fin b₁) (l : List (Fin b₀)) : (morf_list f l).length = l.length

finished March 8, 2024

@[reducible, inline]

abbrev σ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (v : List.Vector (Fin b₀) l) : List.Vector (Fin b₁) l

.

Equations

• σ f go₀ v = morphᵥ f go₀ v

theorem nearby_of_embeds {α : Type} [DecidableEq α] {b₀ b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : embeds_in go₀ go₁) {x y : α} (hn : nearby go₀ x y = true) : nearby go₁ x y = true

.

theorem pt_loc_of_embeds {α : Type} [DecidableEq α] {b₀ b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : embeds_in go₀ go₁) {l : ℕ} (fold : List.Vector α l) (a b : Fin l) (phobic : List.Vector Bool l) (htri : pt_loc go₀ fold a b phobic = true) : pt_loc go₁ fold a b phobic = true

.

theorem pts_at_of_embeds' {α : Type} [DecidableEq α] {b₀ b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : embeds_in go₀ go₁) {l : ℕ} (k : Fin l) (ph : List.Vector Bool l) (fold : List.Vector α l) : pts_at' go₀ k ph fold ≤ pts_at' go₁ k ph fold

.

def pts_tot' {α β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (ph : List.Vector Bool l) (fold : List.Vector α l) : ℕ

.

Equations

• pts_tot' go ph fold = ∑ i : Fin l, pts_at' go i ph fold

def points_tot {α β : Type} [DecidableEq α] [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l) (fold : List.Vector α l) : ℕ

This is needed to get the Handshake Lemma bound from Agarwal et al.'s paper, but it is also just a nicer definition. March 13, 2024. think "ik = (i,k)"

Equations

• points_tot go ph fold = {ik : Fin l × Fin l | pt_loc go fold ik.1 ik.2 ph = true}.card

def ProteinGraph₀ {α β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (ph : List.Vector Bool l.succ) (fold : List.Vector α l.succ) : SimpleGraph (Fin l.succ)

.

Equations

• ProteinGraph₀ go ph fold = { Adj := fun (i j : Fin l.succ) => pt_loc go fold i j ph = true ∨ pt_loc go fold j i ph = true, symm := ⋯, loopless := ⋯ }

def slicer {l : ℕ} (P : Fin l → Fin l → Bool) : Fin l → Finset (Fin l × Fin l)

.

Equations

• slicer P k = {ik : Fin l × Fin l | ik.2 = k ∧ P ik.1 k = true}

theorem slicer_disjointness {l : ℕ} (P : Fin l → Fin l → Bool) (k₁ k₂ : Fin l) : k₁ ≠ k₂ → Disjoint (slicer P k₁) (slicer P k₂)

.

theorem slicer_card {l : ℕ} (P : Fin l → Fin l → Bool) (x : Fin l) : {ik : Fin l × Fin l | ik.2 = x ∧ P ik.1 x = true}.card = {i_1 : Fin l | P i_1 x = true}.card

.

theorem pts_tot'_eq_points_tot {α β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (ph : List.Vector Bool l) (fold : List.Vector α l) : points_tot go ph fold = pts_tot' go ph fold

Write points_tot as a disjoint union over ik.2 to prove. March 14, 2024

theorem pts_bound_of_embeds' {α : Type} [DecidableEq α] {b₀ b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : embeds_in go₀ go₁) {l : ℕ} (ph : List.Vector Bool l) (fold : List.Vector α l) : pts_tot' go₀ ph fold ≤ pts_tot' go₁ ph fold

.

def pts_at_improved {α β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (k : Fin l) (ph : List.Vector Bool l) (fold : List.Vector α l) : ℕ

.

Equations

• pts_at_improved go k ph fold = {i : Fin (↑k).pred | pt_loc go fold (Fin_trans_pred i) k ph = true}.card

theorem pts_at_eq_pts_at'_improved {α β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (k : Fin l) (ph : List.Vector Bool l) (fold : List.Vector α l) : pts_at_improved go k ph fold = pts_at' go k ph fold

.

theorem pts_at_bound'_improved {α : Type} [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l) (fold : List.Vector α l) (i : Fin l) : pts_at' go i ph fold ≤ (↑i).pred

can make this i.pred I think

theorem Fin_sum_range (i : ℕ) : ∑ j : Fin (i + 1), ↑j = i.succ * i / 2

.

theorem Fin_sum_range_pred (i : ℕ) : ∑ j : Fin (i + 1), (↑j).pred = i * (i - 1) / 2

April 2, 2024

theorem pts_earned_bound_loc'_improved {α : Type} [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) (fold : List.Vector α l.succ) : pts_tot' go ph fold ≤ l * l.pred / 2

.

theorem when_zero {α : Type} [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) (fold : List.Vector α l.succ) : ph.length ≤ 2 → pts_tot' go ph fold = 0

The result pts_earned_bound_loc'_improved is sharp in that for l=2, we have words of length 3 and the points bound is 1, which does in fact happen for hex fold. April 2, 2024

theorem path_len {α : Type} [Zero α] {β : Type} (go : β → α → α) {l : ℕ} (moves : List.Vector β l) : (↑(path go ↑moves)).length = l.succ

.

theorem path_at_len {α : Type} (base : α) {β : Type} (go : β → α → α) {l : ℕ} (moves : List.Vector β l) : (↑(path_at base go ↑moves)).length = l.succ

.

def pathᵥ {l : ℕ} {α : Type} [Zero α] {β : Type} (go : β → α → α) (moves : List.Vector β l) : List.Vector α l.succ

.

Equations

• pathᵥ go moves = ⟨↑(path go ↑moves), ⋯⟩

@[reducible, inline]

abbrev π {l : ℕ} {α : Type} [Zero α] {β : Type} (go : β → α → α) (moves : List.Vector β l) : List.Vector α l.succ

.

Equations

• π go moves = pathᵥ go moves

theorem pathᵥ_len {α : Type} [Zero α] {β : Type} (go : β → α → α) {l : ℕ} (moves : List.Vector β l) : (pathᵥ go moves).length = l.succ

.

def pathᵥ_at {l : ℕ} {α : Type} (base : α) {β : Type} (go : β → α → α) (moves : List.Vector β l) : List.Vector α l.succ

.

Equations

• pathᵥ_at base go moves = ⟨↑(path_at base go ↑moves), ⋯⟩

def pt_dir {α : Type} [Zero α] {β : Type} (go : β → α → α) {l : ℕ} (j : Fin l.succ) (moves : List.Vector β l) (ph : List.Vector Bool l.succ) : β → Fin l.succ → Prop

.

Equations

• pt_dir go j moves ph a i = (ph.get i = true ∧ ph.get j = true ∧ (↑i).succ < ↑j ∧ (pathᵥ go moves).get j = go a ((pathᵥ go moves).get i))

theorem unique_loc {α : Type} [Zero α] {β : Type} {go : β → α → α} {l : ℕ} {j : Fin l.succ} {moves : List.Vector β l} {ph : List.Vector Bool l.succ} (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ go moves).get k) (right_inj : right_injective go) (a : β) (i₀ i₁ : Fin l.succ) (hai₀ : pt_dir go j moves ph a i₀) (hai₁ : pt_dir go j moves ph a i₁) : i₀ = i₁

.

theorem unique_dir {α : Type} [Zero α] {β : Type} {go : β → α → α} {l : ℕ} (j : Fin l.succ) (moves : List.Vector β l) (ph : List.Vector Bool l.succ) (left_inj : left_injective go) (i : Fin l.succ) (a₀ a₁ : β) (hai₀ : pt_dir go j moves ph a₀ i) (hai₁ : pt_dir go j moves ph a₁ i) : a₀ = a₁

.

theorem unique_loc_dir {α : Type} [Zero α] {β : Type} {go : β → α → α} {l : ℕ} {j : Fin l.succ} {moves : List.Vector β l} {ph : List.Vector Bool l.succ} (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ go moves).get k) (right_inj : right_injective go) (left_inj : left_injective go) : (∀ (a : β) (i₀ i₁ : Fin l.succ), pt_dir go j moves ph a i₀ → pt_dir go j moves ph a i₁ → i₀ = i₁) ∧ ∀ (i : Fin l.succ) (a₀ a₁ : β), pt_dir go j moves ph a₀ i → pt_dir go j moves ph a₁ i → a₀ = a₁

.

theorem left_injective_of_embeds_in_strongly {α : Type} {b : ℕ} {go₀ go₁ : Fin b → α → α} (f : Fin b → α → Fin b) (is_emb : is_embedding go₀ go₁ f) (left_inj_emb : left_injective f) (left_inj_go : left_injective go₁) : left_injective go₀

left_injective f which we can prove for tri_rect_embedding although it's harder than left_injective_tri!

theorem unique_loc_dir_rect {l : ℕ} (j : Fin l.succ) (moves : List.Vector (Fin 4) l) (ph : List.Vector Bool l.succ) (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ rect moves).get k) : (∀ (a : Fin 4) (i₀ i₁ : Fin l.succ), pt_dir rect j moves ph a i₀ → pt_dir rect j moves ph a i₁ → i₀ = i₁) ∧ ∀ (i : Fin l.succ) (a₀ a₁ : Fin 4), pt_dir rect j moves ph a₀ i → pt_dir rect j moves ph a₁ i → a₀ = a₁

location, direction

theorem unique_loc_dir_hex {l : ℕ} (j : Fin l.succ) (moves : List.Vector (Fin 6) l) (ph : List.Vector Bool l.succ) (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ hex moves).get k) : (∀ (a : Fin 6) (i₀ i₁ : Fin l.succ), pt_dir hex j moves ph a i₀ → pt_dir hex j moves ph a i₁ → i₀ = i₁) ∧ ∀ (i : Fin l.succ) (a₀ a₁ : Fin 6), pt_dir hex j moves ph a₀ i → pt_dir hex j moves ph a₁ i → a₀ = a₁

.

@[implicit_reducible]

instance instDecidablePt_dirFinOfDecidableEq {α : Type} [Zero α] [DecidableEq α] {b : ℕ} {go : Fin b → α → α} {l : ℕ} (j : Fin l.succ) (ph : List.Vector Bool l.succ) (moves : List.Vector (Fin b) l) (a : Fin b) (i : Fin l.succ) : Decidable (pt_dir go j moves ph a i)

This trivial instance is nonetheless needed.

Equations

• instDecidablePt_dirFinOfDecidableEq j ph moves a i = decidable_of_iff (ph.get i = true ∧ ph.get j = true ∧ (↑i).succ < ↑j ∧ (pathᵥ go moves).get j = go a ((pathᵥ go moves).get i)) ⋯

theorem pts_at'_dir {α : Type} [Zero α] [DecidableEq α] {b : ℕ} {go : Fin b → α → α} {l : ℕ} (j : Fin l.succ) (ph : List.Vector Bool l.succ) (moves : List.Vector (Fin b) l) (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ go moves).get k) (right_inj : right_injective go) (left_inj : left_injective go) : pts_at' go j ph (pathᵥ go moves) ≤ b

.

theorem pts_earned_bound_dir' {α : Type} [Zero α] [DecidableEq α] {b : ℕ} {go : Fin b → α → α} {l : ℕ} (ph : List.Vector Bool l.succ) (moves : List.Vector (Fin b) l) (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ go moves).get k) (right_inj : right_injective go) (left_inj : left_injective go) : pts_tot' go ph (pathᵥ go moves) ≤ l.succ * b

Almost obsolete, except for rect₃ fold which is not symmetric so that Handshake Lemma reasoning does not apply.

theorem independence_in_symmetric_pts_earned_bound_dir'₁ : ∃ (α : Type) (β : Type) (x : Fintype β) (x_1 : DecidableEq α) (go : β → α → α), right_injective go ∧ left_injective go ∧ ¬Symmetric fun (x_2 y : α) => nearby go x_2 y = true

.

def f_dni : Fin 2 × Fin 2 → Fin 2

"does not imply"

Equations

• f_dni (0, 0) = 0
• f_dni (0, 1) = 0
• f_dni (1, 0) = 1
• f_dni (1, 1) = 0

def g : Fin 2 → Fin 2 → Fin 2

.

Equations

• g x y = f_dni (x, y)

@[implicit_reducible]

instance instDecidableSymmetricFinOfNatNatEqBoolNearbyGTrue : Decidable (Symmetric fun (x y : Fin 2) => nearby g x y = true)

.

Equations

• instDecidableSymmetricFinOfNatNatEqBoolNearbyGTrue = id (id inferInstance)

@[implicit_reducible]

instance instDecidableLeft_injectiveFinOfNatNatG : Decidable (left_injective g)

.

Equations

• instDecidableLeft_injectiveFinOfNatNatG = id inferInstance

@[implicit_reducible]

instance instDecidableRight_injectiveFinOfNatNatG : Decidable (right_injective g)

.

Equations

• instDecidableRight_injectiveFinOfNatNatG = id inferInstance

def ctrex : (Fin 2 → Fin 2) → Fin 2 → Fin 2

This is the first example I thought of that has a Symmetric nearby function, but is neither left nor right injective.

Equations

• ctrex f x = f x

theorem independence_in_symmetric_pts_earned_bound_dir'₂ : ∃ (α : Type) (β : Type) (x : Fintype β) (x_1 : DecidableEq α) (go : β → α → α), ¬right_injective go ∧ ¬left_injective go ∧ Symmetric fun (x_2 y : α) => nearby go x_2 y = true

.

theorem pts_earned_bound' {α : Type} [Zero α] [DecidableEq α] {b : ℕ} {go : Fin b → α → α} {l : ℕ} (ph : List.Vector Bool l.succ) (moves : List.Vector (Fin b) l) (path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ go moves).get k) (right_inj : right_injective go) (left_inj : left_injective go) : pts_tot' go ph (pathᵥ go moves) ≤ min (l.succ * b) (l * l.pred / 2)

this is anyway obsolete since Handshake lemma gives another /2 factor

theorem two_heads {α : Type} {k : ℕ} (v : List.Vector α k.succ) (w : List α) (hw : w ≠ []) (h : ↑v = w) : v.head = w.head hw

.

theorem path_cons {α : Type} [Zero α] {b₀ : ℕ} (go₀ : Fin b₀ → α → α) (head : Fin b₀) (tail : List (Fin b₀)) : ↑(path go₀ (head :: tail)) = go₀ head (path go₀ tail).head :: ↑(path go₀ tail)

.

theorem path_cons_vec {α : Type} [Zero α] {b₀ : ℕ} (go₀ : Fin b₀ → α → α) (head : Fin b₀) (tail : List (Fin b₀)) : path go₀ (head :: tail) = go₀ head (path go₀ tail).head ::ᵥ path go₀ tail

.

theorem path_at_cons {α : Type} (base : α) {b₀ : ℕ} (go₀ : Fin b₀ → α → α) (hd : Fin b₀) (tl : List (Fin b₀)) : ↑(path_at base go₀ (hd :: tl)) = go₀ hd (path_at base go₀ tl).head :: ↑(path_at base go₀ tl)

.

theorem path_at_cons_vec {α : Type} (base : α) {b₀ : ℕ} (go₀ : Fin b₀ → α → α) (hd : Fin b₀) (tl : List (Fin b₀)) : path_at base go₀ (hd :: tl) = go₀ hd (path_at base go₀ tl).head ::ᵥ path_at base go₀ tl

.

theorem plane_assoc (x y z : ℤ × ℤ) : x + (y + z) = x + y + z

.

theorem orderly_injective_helper {β : Type} (x : ℕ → β) (a b : β) (hab : a ≠ b) (h₀ : x 0 = a) (j : ℕ) (hj : ∃ i < j, x i.succ = b) (h₂ : ∀ i < j, x i = a ∨ x i = b) [DecidablePred fun (n : ℕ) => n < j ∧ x n.succ = b] : ∃ i < j, x i = a ∧ x i.succ = b

.

theorem fin_fin {k i : ℕ} {j : Fin k.succ} (h : i < ↑j) : i < k

.

theorem fin_fi {k i : ℕ} {j : Fin k.succ} (h : i < ↑j) : i < k.succ

.

theorem orderly_injective_helper₁ {β : Type} {k : ℕ} {x : Fin k.succ → β} {a b : β} (hab : a ≠ b) (h₀ : x 0 = a) {j : Fin k.succ} (hj : ∃ (i : Fin k), ↑i < ↑j ∧ x i.succ = b) (h₂ : ∀ (i : Fin k.succ), ↑i < ↑j → x i = a ∨ x i = b) [DecidablePred fun (n : ℕ) => ∃ (h : n < ↑j), x ⟨n, ⋯⟩.succ = b] : ∃ (i : Fin k), ↑i < ↑j ∧ x i.castSucc = a ∧ x i.succ = b

.

theorem orderly_injective_helper₂ (k : ℕ) (x : Fin k.succ → Fin 4) (h₀ : x 0 = 0) (j : Fin k.succ) (hj : ∃ (i : Fin k), ↑i < ↑j ∧ x i.succ = 1) (h₂ : ∀ (i : Fin k.succ), ↑i < ↑j → x i = 0 ∨ x i = 1) : ∃ (i : Fin k), ↑i < ↑j ∧ x i.castSucc = 0 ∧ x i.succ = 1

.

theorem path_len' {α : Type} [Zero α] {β : Type} (go : β → α → α) (l : ℕ) (moves : List β) (hm : moves.length = l) : (↑(path go moves)).length = l.succ

.

theorem path_nil {α : Type} [Zero α] {β : Type} (go : β → α → α) : ↑(path go []) = [0]

.

theorem path_at_nil {α : Type} (base : α) {β : Type} (go : β → α → α) : ↑(path_at base go []) = [base]

.

theorem path_at_nil_vec {α : Type} (base : α) {β : Type} (go : β → α → α) : path_at base go [] = ⟨[base], ⋯⟩

.

theorem ne_nil_of_succ_length {α : Type} {k : ℕ} (tail_ih : List.Vector α k.succ) : ↑tail_ih ≠ []

.

theorem path_eq_path_morph {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (g : is_embedding go₀ go₁ f) (moves : List (Fin b₀)) : ↑(path go₀ moves) = ↑(path go₁ (morph f go₀ moves))

.

theorem path_eq_path_morphᵥ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (g : is_embedding go₀ go₁ f) (moves : List.Vector (Fin b₀) l) : ↑(path go₀ ↑moves) = ↑(path go₁ ↑(morphᵥ f go₀ moves))

.

theorem pathᵥ_eq_path_morphᵥ1 {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (g : is_embedding go₀ go₁ f) (moves : List.Vector (Fin b₀) l) : ↑(pathᵥ go₀ moves) = ↑(pathᵥ go₁ (morphᵥ f go₀ moves))

.

theorem pathᵥ_eq_path_morphᵥ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (g : is_embedding go₀ go₁ f) (moves : List.Vector (Fin b₀) l) : pathᵥ go₀ moves = pathᵥ go₁ (morphᵥ f go₀ moves)

.

def path_transformed {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (l : List (Fin b₀)) : List.Vector α l.length.succ

.

Equations

• path_transformed f go₀ go₁ l = ⟨↑(path go₁ (morph f go₀ l)), ⋯⟩

def path_transformedᵥ {l : ℕ} {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (v : List.Vector (Fin b₀) l) : List.Vector α l.succ

.

Equations

• path_transformedᵥ f go₀ go₁ v = pathᵥ go₁ (morphᵥ f go₀ v)

theorem transform_of_embed {α : Type} [Zero α] {b₀ b₁ : ℕ} (f : Fin b₀ → α → Fin b₁) (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (l : List (Fin b₀)) (h_embed : is_embedding go₀ go₁ f) : path_transformed f go₀ go₁ l = path go₀ l

def pts_tot_bound {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) (q : ℕ) : Prop

.

Equations

• pts_tot_bound go ph q = ∀ (moves : List.Vector β l), (Function.Injective fun (k : Fin (↑(path go ↑moves)).length) => (↑(path go ↑moves)).get k) → pts_tot' go ph ⟨↑(path go ↑moves), ⋯⟩ ≤ q

def pts_tot_bound_rev {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) (q : ℕ) : Prop

This version of pts_tot_bound is correct even for the asymmetric 3-move version of rect:

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instDecidablePredNatPts_tot_bound {l : ℕ} {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] {ph : List.Vector Bool l.succ} (go : β → α → α) : DecidablePred (pts_tot_bound go ph)

.

Equations

• instDecidablePredNatPts_tot_bound go = id (id inferInstance)

@[implicit_reducible]

instance instDecidablePredNatPts_tot_bound_1 {l : ℕ} {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] {ph : List.Vector Bool l.succ} (go : β → α → α) : DecidablePred fun (n : ℕ) => pts_tot_bound go ph n

.

Equations

• instDecidablePredNatPts_tot_bound_1 go = id (id inferInstance)

@[implicit_reducible]

instance instDecidablePredNatPts_tot_bound_rev {l : ℕ} {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {ph : List.Vector Bool l.succ} : DecidablePred (pts_tot_bound_rev go ph)

.

Equations

• instDecidablePredNatPts_tot_bound_rev go = id (id inferInstance)

@[implicit_reducible]

instance instDecidablePredNatPts_tot_bound_rev_1 {l : ℕ} {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {ph : List.Vector Bool l.succ} : DecidablePred fun (n : ℕ) => pts_tot_bound_rev go ph n

.

Equations

• instDecidablePredNatPts_tot_bound_rev_1 go = id (id inferInstance)

theorem pts_tot_bound_rev_exists {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) : ∃ (q : ℕ), pts_tot_bound_rev go ph q

.

theorem pts_tot_bound_exists {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) : ∃ (q : ℕ), pts_tot_bound go ph q

.

def HP {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

HP is the HP protein folding model "objective function" or "value function":

Equations

• HP go ph = Nat.find ⋯

def HP_rev {α : Type} [Zero α] [DecidableEq α] {β : Type} [Fintype β] (go : β → α → α) {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

For nonsymmetric "nearby" relations we must use this version.

Equations

• HP_rev go ph = Nat.find ⋯

def P_tri' {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

.

Equations

• P_tri' ph = HP tri ph

def P_rect' {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

.

Equations

• P_rect' ph = HP rect ph

def P_rect₃' {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

.

Equations

• P_rect₃' ph = HP_rev rect₃ ph

def P_hex' {l : ℕ} (ph : List.Vector Bool l.succ) : ℕ

.

Equations

• P_hex' ph = HP hex ph

theorem List.Vector_inj_of_list_inj {t : Type} {n : ℕ} {v : Vector t n} (h : Function.Injective fun (k : Fin (↑v).length) => (↑v).get k) : Function.Injective fun (k : Fin n) => v.get k

.

theorem list_inj_of_List.Vector_inj {t : Type} {n : ℕ} {v : List.Vector t n} (h : Function.Injective fun (k : Fin n) => v.get k) : Function.Injective fun (k : Fin (↑v).length) => (↑v).get k

.

theorem P_tri_lin_bound {l : ℕ} (ph : List.Vector Bool l.succ) : P_tri' ph ≤ l.succ * 3

.

theorem P_hex_lin_bound {l : ℕ} (ph : List.Vector Bool l.succ) : P_hex' ph ≤ l.succ * 6

.

theorem P_rect_lin_bound {l : ℕ} (ph : List.Vector Bool l.succ) : P_rect' ph ≤ l.succ * 4

.

theorem value_bound_of_embeds_strongly {α : Type} [Zero α] [DecidableEq α] {b₀ b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : go₀ ≼ go₁) {l : ℕ} (ph : List.Vector Bool l.succ) : HP go₀ ph ≤ HP go₁ ph

.

theorem embeds_strongly_tri_quad : tri ≼ rect

.

theorem embeds_strongly_quad_hex : rect ≼ hex

.

theorem HP_quad_bounds_tri {l : ℕ} (ph : List.Vector Bool l.succ) : HP tri ph ≤ HP rect ph

.

theorem HP_hex_bounds_quad {l : ℕ} (ph : List.Vector Bool l.succ) : HP rect ph ≤ HP hex ph

.