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
morf
{l : ℕ}
{b₀ : ℕ}
{b₁ : ℕ}
(f : Fin b₀ → Fin b₁)
(v : Mathlib.Vector (Fin b₀) l)
:
Mathlib.Vector (Fin b₁) l
.
Equations
- morf f v = Mathlib.Vector.map f v
Instances For
theorem
pt_loc_of_embeds
{α : Type}
[DecidableEq α]
{b₀ : ℕ}
{b₁ : ℕ}
{go₀ : Fin b₀ → α → α}
{go₁ : Fin b₁ → α → α}
(h_embed : embeds_in go₀ go₁)
{l : ℕ}
(fold : Mathlib.Vector α l)
(a : Fin l)
(b : Fin l)
(phobic : Mathlib.Vector Bool l)
(htri : 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 : Mathlib.Vector Bool l)
(fold : Mathlib.Vector α l)
:
.
def
pts_tot'
{α : Type}
{β : Type}
[Fintype β]
(go : β → α → α)
[DecidableEq α]
{l : ℕ}
(ph : Mathlib.Vector Bool l)
(fold : Mathlib.Vector α l)
:
.
Instances For
def
points_tot
{α : Type}
{β : Type}
[DecidableEq α]
[Fintype β]
(go : β → α → α)
{l : ℕ}
(ph : Mathlib.Vector Bool l)
(fold : Mathlib.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 = (Finset.filter (fun (ik : Fin l × Fin l) => pt_loc go fold ik.1 ik.2 ph = true) Finset.univ).card
Instances For
In order to use the handshaking lemma from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/DegreeSum.html#SimpleGraph.sum_degrees_eq_twice_card_edges Bonds: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Dart.html#SimpleGraph.Dart we may introduce this: note that we form a graph on the amino acids rather than on the ambient space.
Equations
Instances For
def
ProteinGraph₀
{α : Type}
{β : Type}
[Fintype β]
(go : β → α → α)
[DecidableEq α]
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(fold : Mathlib.Vector α l.succ)
:
SimpleGraph (Fin l.succ)
.
Equations
Instances For
theorem
pts_tot'_eq_points_tot
{α : Type}
{β : Type}
[Fintype β]
(go : β → α → α)
[DecidableEq α]
{l : ℕ}
(ph : Mathlib.Vector Bool l)
(fold : Mathlib.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 : Mathlib.Vector Bool l)
(fold : Mathlib.Vector α l)
:
.
def
pts_at_improved
{α : Type}
{β : Type}
[Fintype β]
(go : β → α → α)
[DecidableEq α]
{l : ℕ}
(k : Fin l)
(ph : Mathlib.Vector Bool l)
(fold : Mathlib.Vector α l)
:
.
Equations
- pts_at_improved go k ph fold = (Finset.filter (fun (i : Fin (↑k).pred) => pt_loc go fold (Fin_trans_pred i) k ph = true) Finset.univ).card
Instances For
theorem
pts_at_eq_pts_at'_improved
{α : Type}
{β : Type}
[Fintype β]
(go : β → α → α)
[DecidableEq α]
{l : ℕ}
(k : Fin l)
(ph : Mathlib.Vector Bool l)
(fold : Mathlib.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 : Mathlib.Vector Bool l)
(fold : Mathlib.Vector α l)
(i : Fin l)
:
can make this i.pred I think
theorem
pts_earned_bound_loc'_improved
{α : Type}
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(fold : Mathlib.Vector α l.succ)
:
.
theorem
when_zero
{α : Type}
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(fold : Mathlib.Vector α l.succ)
:
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_at_len
{α : Type}
(base : α)
{β : Type}
(go : β → α → α)
{l : ℕ}
(moves : Mathlib.Vector β l)
:
.
def
pathᵥ_at
{l : ℕ}
{α : Type}
(base : α)
{β : Type}
(go : β → α → α)
(moves : Mathlib.Vector β l)
:
Mathlib.Vector α l.succ
.
Instances For
def
pt_dir
{α : Type}
[Zero α]
{β : Type}
(go : β → α → α)
{l : ℕ}
(j : Fin l.succ)
(moves : Mathlib.Vector β l)
(ph : Mathlib.Vector Bool l.succ)
:
.
Equations
Instances For
theorem
unique_loc
{α : Type}
[Zero α]
{β : Type}
{go : β → α → α}
{l : ℕ}
{j : Fin l.succ}
{moves : Mathlib.Vector β l}
{ph : Mathlib.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₀ : Fin l.succ)
(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 : Mathlib.Vector β l)
(ph : Mathlib.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 : Mathlib.Vector β l}
{ph : Mathlib.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)
:
.
theorem
left_injective_of_embeds_in_strongly
{α : Type}
{b : ℕ}
{go₀ : Fin b → α → α}
{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 : Mathlib.Vector (Fin 4) l)
(ph : Mathlib.Vector Bool l.succ)
(path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ rect moves).get k)
:
location, direction
theorem
unique_loc_dir_hex
{l : ℕ}
(j : Fin l.succ)
(moves : Mathlib.Vector (Fin 6) l)
(ph : Mathlib.Vector Bool l.succ)
(path_inj : Function.Injective fun (k : Fin l.succ) => (pathᵥ hex moves).get k)
:
.
instance
instDecidablePt_dirFinOfDecidableEq
{α : Type}
[Zero α]
[DecidableEq α]
{b : ℕ}
{go : Fin b → α → α}
{l : ℕ}
(j : Fin l.succ)
(ph : Mathlib.Vector Bool l.succ)
(moves : Mathlib.Vector (Fin b) l)
(a : Fin b)
(i : Fin l.succ)
:
This trivial instance is nonetheless needed.
theorem
pts_at'_dir
{α : Type}
[Zero α]
[DecidableEq α]
{b : ℕ}
{go : Fin b → α → α}
{l : ℕ}
(j : Fin l.succ)
(ph : Mathlib.Vector Bool l.succ)
(moves : Mathlib.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)
:
.
theorem
pts_earned_bound_dir'
{α : Type}
[Zero α]
[DecidableEq α]
{b : ℕ}
{go : Fin b → α → α}
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(moves : Mathlib.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)
:
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
.
.
Equations
- instDecidableLeft_injectiveFinOfNatNatG = id inferInstance
.
Equations
- instDecidableRight_injectiveFinOfNatNatG = id inferInstance
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 : Mathlib.Vector Bool l.succ)
(moves : Mathlib.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)
:
this is anyway obsolete since Handshake lemma gives another /2 factor
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]
:
.
.
def
path_transformedᵥ
{l : ℕ}
{α : Type}
[Zero α]
{b₀ : ℕ}
{b₁ : ℕ}
(f : Fin b₀ → α → Fin b₁)
(go₀ : Fin b₀ → α → α)
(go₁ : Fin b₁ → α → α)
(v : Mathlib.Vector (Fin b₀) l)
:
Mathlib.Vector α l.succ
.
Equations
- path_transformedᵥ f go₀ go₁ v = pathᵥ go₁ (morphᵥ f go₀ v)
Instances For
def
pts_tot_bound
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(q : ℕ)
:
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
pts_tot_bound_rev
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{l : ℕ}
(ph : Mathlib.Vector Bool l.succ)
(q : ℕ)
:
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.
Instances For
instance
instDecidablePredNatPts_tot_bound
{l : ℕ}
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
{ph : Mathlib.Vector Bool l.succ}
(go : β → α → α)
:
DecidablePred (pts_tot_bound go ph)
.
Equations
- instDecidablePredNatPts_tot_bound go = id (id inferInstance)
instance
instDecidablePredNatPts_tot_bound_1
{l : ℕ}
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
{ph : Mathlib.Vector Bool l.succ}
(go : β → α → α)
:
DecidablePred fun (n : ℕ) => pts_tot_bound go ph n
.
Equations
- instDecidablePredNatPts_tot_bound_1 go = id (id inferInstance)
instance
instDecidablePredNatPts_tot_bound_rev
{l : ℕ}
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{ph : Mathlib.Vector Bool l.succ}
:
DecidablePred (pts_tot_bound_rev go ph)
.
Equations
- instDecidablePredNatPts_tot_bound_rev go = id (id inferInstance)
instance
instDecidablePredNatPts_tot_bound_rev_1
{l : ℕ}
{α : Type}
[Zero α]
[DecidableEq α]
{β : Type}
[Fintype β]
(go : β → α → α)
{ph : Mathlib.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 : Mathlib.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 : Mathlib.Vector Bool l.succ)
:
∃ (q : ℕ), pts_tot_bound go ph q
.
theorem
Vector_inj_of_list_inj
{t : Type}
{n : ℕ}
{v : Mathlib.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_Vector_inj
{t : Type}
{n : ℕ}
{v : Mathlib.Vector t n}
(h : Function.Injective fun (k : Fin n) => v.get k)
:
Function.Injective fun (k : Fin (↑v).length) => (↑v).get k
.